Marcus Rossel: Egg: An Equality Saturation Tactic in Lean

Stream: Lean Together 2025

[Andrés Goens]

discussion thread

[Andrés Goens]

(link to the tactic https://github.com/marcusrossel/lean-egg)

[Andrés Goens]

and just to mention one thing that was asked, there is already an egg? variant that uses calc (through calcify), but sometimes the explantions frome egg become very long

[Marcus Rossel]

Slides

[Tristan Figueroa-Reid]

I'm a little curious about the bundling the backend issue: what problems occurred when trying to build and bundle egg?

[Vlad Tsyrklevich]

Yes, would it just be possible to ship static binaries for the main platforms to avoid the rust dependency?

[Vlad Tsyrklevich]

Also, given that you've said egg is slow, how many low-hanging performance gains do you imagine there are? Either by large efforts like eliminating the Lean -> Rust -> Lean translation steps or anything else. I'm just curious if it has to be slow because of equality saturations intrinsic perf characteristics or if it could imaginably be fast.

[Marcus Rossel]

Tristan Figueroa-Reid said:

I'm a little curious about the bundling the backend issue: what problems occurred when trying to build and bundle egg?

Right now, when you lake build a project which depends on egg it will call the Rust's build tool cargo to build the required Rust code. So if you don't have cargo installed, this will fail.

[Marcus Rossel]

Vlad Tsyrklevich said:

Yes, would it just be possible to ship static binaries for the main platforms to avoid the rust dependency?

That would be my hope. I don't think Lake supports such a feature at the moment though.

[Marcus Rossel]

Vlad Tsyrklevich said:

Also, given that you've said egg is slow, how many low-hanging performance gains do you imagine there are? Either by large efforts like eliminating the Lean -> Rust -> Lean translation steps or anything else. I'm just curious if it has to be slow because of equality saturations intrinsic perf characteristics or if it could imaginably be fast.

There are definitely many low-hanging performance gains, because so far we've largely disregarded optimizing for performance. However, these performance gains are mainly to be found in the preprocessing and proof reconstruction steps (in Lean), which usually aren't the bottleneck. When a proof takes multiple seconds to complete, this usually means that the equality saturation step in the egg backend took that long. And since the egg library is already extremely performant, we could only hope to improve performance there by being smarter about which rewrites we generate/select, and keeping the data we pass into the e-graph as small as possible.

That said, equality saturation tends to have the property that it either completes relatively quickly, or never manages to prove a goal at all (cf. this paper). That's why we set the default time limit for equality saturation at 3 seconds, so I guess it's arguable whether that's "fast".

[Kim Morrison]

@Marcus Rossel, https://github.com/marcusrossel/lean-egg doesn't seem to have a Lake testDriver set up (i.e. so I can run lake test).

Would you mind either setting that up, or adding instructions to the README on how to run the test suite?

[Kim Morrison]

Is there an existing discussion topic for egg? I'm looking for some help getting it going and don't want to clog up this discussion.

[Kim Morrison]

In the meantime, I'm stuck at the linked error trace when trying to open Lean/Egg/Tests/Math/Math/Group.lean in VSCode.

[Kim Morrison]

Running rustc -vV at the command line looks sensible:

% rustc -vV
rustc 1.84.0 (9fc6b4312 2025-01-07) (Homebrew)
binary: rustc
commit-hash: 9fc6b43126469e3858e2fe86cafb4f0fd5068869
commit-date: 2025-01-07
host: aarch64-apple-darwin
release: 1.84.0
LLVM version: 19.1.6

but copy pasting the other command line from the error trace to the command line gives:

% cargo rustc --release -- -C relocation-model=pic
error: could not find `Cargo.toml` in `/Users/kim/projects/lean/lean-egg` or any parent directory

[Pietro Monticone]

:video_camera: Video recording: https://youtu.be/Nnxp92NGB9c

[Johan Commelin]

If the calc-blocks produced by egg? become quite long, would it make sense to produce rw proofs instead? (And leave it to the user to decide whether to calcify?)

[Johan Commelin]

It's really cool to see that egg now works on the Lie theory problems (-;

[Vlad Tsyrklevich]

I think there's also a more general question about how to handle unwieldy re-constructed proofs from hammers. If the reconstructed proofs don't easily take the form of a short re-write but are a ~2 kilobyte term, how should that be handled? I could imagine that if these hammers come into common use that perhaps it would be valuable to have a system where egg?, duper?, smt? etc can automatically offer to save long expressions in something like a Generated/ directory to keep the human-readable code clean, and just reference that expression. But I'm far from an expert on Lean/mathlib, would love to hear what others think

[Andrés Goens]

Kim Morrison said:

Marcus Rossel, https://github.com/marcusrossel/lean-egg doesn't seem to have a Lake testDriver set up (i.e. so I can run lake test).

Would you mind either setting that up, or adding instructions to the README on how to run the test suite?

I'll let @Marcus Rossel answer the rest of that, but as a quick note in the meantime, you can run the test suite by calling ./Lean/Egg/Tests/run_tests.sh --egg (AFIU not everything runs right now because of some refactoring)

[Andrés Goens]

Kim Morrison said:

In the meantime, I'm stuck at the linked error trace when trying to open Lean/Egg/Tests/Math/Math/Group.lean in VSCode.

oh, yeah that looks like an unfortunate problem with the way the tests are set up, because we don't want to depend on mathlib, tests that use mathlib are in a second repository in Lean/Egg/Tests/Math, the ones that are on Lean/Egg/Tests should "just work" by opening vs code in your setup (that has a rust installation). I think @Marcus Rossel mentioned something was broken with this two-repo setup, but I'm not up to date there so we'll have to wait for him on that one

[Marcus Rossel]

Kim Morrison said:

Marcus Rossel, https://github.com/marcusrossel/lean-egg doesn't seem to have a Lake testDriver set up (i.e. so I can run lake test).

Would you mind either setting that up, or adding instructions to the README on how to run the test suite?

Sure, we'll set up lake test integration soon. For now (as Andrés mentioned), you can run tests by calling ./Lean/Egg/Tests/run_tests.sh --egg. And as of the latest commit (204b228) all test should pass again (:check: = good, :yellow_circle: = known problem, :cross_mark: = actual error).

[Marcus Rossel]

Kim Morrison said:

In the meantime, I'm stuck at the linked error trace when trying to open Lean/Egg/Tests/Math/Math/Group.lean in VSCode.

As for this, Andrés again pretty much summed it up. We have a separate Lake project in Lean/Egg/Test/Math for tests which should depend on mathlib. So if you want to build those files you'll have to lake build from that directory. Or if you want to look at the code in an editor, open that directory instead of the root lean-egg directory. We don't have a test script for mathlib-based tests yet, but there aren't many test cases, so you should be able to just browse them.

Also, if you pull a new version of the repo and want a clean clean rebuild, I recommend first going into Egg/Rust and doing a cargo clean and then doing a lake clean in the top-level lean-egg directory. Is there a way to hook into lake clean to make it do the cargo clean?

[Marcus Rossel]

Johan Commelin said:

If the calc-blocks produced by egg? become quite long, would it make sense to produce rw proofs instead? (And leave it to the user to decide whether to calcify?)

I think having a rw-based egg? is definitely a desirable goal when somebody finds time to work on that. I just don't know how hard it is to turn an egg explanation into a sequence of rws. In general we can't just use rw with the given lemma and rewrite direction. We would sometimes also have to determine at which occurrence (as in docs#Lean.Meta.Occurrences) to rw. And other times we would have to explicitly specify some of the arguments to the lemma. And even then, unfortunately this doesn't fix the problem of long explanations because 600 explanation steps would simply turn into ~600 rws.

[Marcus Rossel]

Vlad Tsyrklevich said:

I think there's also a more general question about how to handle unwieldy re-constructed proofs from hammers.

I'm guessing other ITPs (Isabelle :eyes:) must have faced similar issues which we could take inspiration from.

[Andrés Goens]

Marcus Rossel said:

Vlad Tsyrklevich said:

I think there's also a more general question about how to handle unwieldy re-constructed proofs from hammers.

I'm guessing other ITPs (Isabelle :eyes:) must have faced similar issues which we could take inspiration from.

Isabelle's a bit different because Isabelle doesn't have proof terms in the same way that Lean has (there is no equivalent to the oleans), they have a more "purist" view of the LCF architecture wherin they just have an API to deduce things in the core language and so Isabelle just saves proofs in the memory of the kernel, having been checked, and not as an ellaborated term that could be independently checked (cf. this blog post by Larry Paulson)

[Joachim Breitner]

Marcus Rossel said:

In general we can't just use rw with the given lemma and rewrite direction. We would sometimes also have to determine at which occurrence (as in docs#Lean.Meta.Occurrences) to rw. And other times we would have to explicitly specify some of the arguments to the lemma.

I imagine that the calcify infrastructure (simplifying the proof terms into a sequence of transitive steps) can be used here; if each step turns out to be an congArg , then one can maybe construct the necessary occurrence count for the rw. At least as a 80% heuristic.

[Marcus Rossel]

Joachim Breitner said:

if each step turns out to be an congArg , then one can maybe construct the necessary occurrence count for the rw. At least as a 80% heuristic.

IIRC there was also some Lean project which allowed you to insert rws by clicking on the relevant terms in the info view. I think they had to address the same problem.

[Joachim Breitner]

Instead of using rw with occ, maybe using conv => enter [1,2,3,4] is another alternative for a more concise form, and certainly simpler and more robust to create.

[Siddhartha Gadgil]

This is really useful stuff. In LeanAide I have a hack for this by passing rw [blah] in both directions as tactics to Aesop. I look forward to using lean-egg instead.

[Marcus Rossel]

Siddhartha Gadgil said:

This is really useful stuff. In LeanAide I have a hack for this by passing rw [blah] in both directions as tactics to Aesop. I look forward to using lean-egg instead.

Could you point me to where you're currently implementing the bidirectional rw?

[Siddhartha Gadgil]

Marcus Rossel said:

Siddhartha Gadgil said:

This is really useful stuff. In LeanAide I have a hack for this by passing rw [blah] in both directions as tactics to Aesop. I look forward to using lean-egg instead.

Could you point me to where you're currently implementing the bidirectional rw?

It is in https://github.com/siddhartha-gadgil/LeanAide/blob/main/LeanAide/AesopSyntax.lean which in turn is called by https://github.com/siddhartha-gadgil/LeanAide/blob/main/LeanAide/AutoTactic.lean (very hacky at present)