This repository contains work-in-progress of a Lean4 tactic to prove equalities, powered by E-Graphs and the egg project.
To use this tactic you will need a recent version of Lean4, ideally a nightly (see here for installation instructions.
You will also need an installation of Rust to compile the egg integration.
To build this, just run the following in the json-egg directory:
cargo build --release
Just open the EggTactic/Test.lean file in your favorite editor that supports Lean4 and you should be able to use the rawEgg tactic to prove your equalities. We have not yet packaged this to use directly in your own project.
This project is work in progress and is not yet ready for everyday use. Don't worry however, you won't be able to prove anything incorrect with this. In the worst case, the tactic will fail when it shouldn't.