15 E-Graphs
For proving implications, we used another technique called equality saturation [ 10 ] with the lean-egg tactic, to automatically construct proofs.
A similar approach is being pursued in the MagmaEgg tool as well, which is a standalone program that only supports magma equalities, while the lean-egg tactic supports any Lean expression.
15.1 lean-egg
15.1.1 Methodology
The basic methodology of equality saturation is based on E-Graphs, a data structure that can store equivalence classes of terms efficiently. We used the lean-egg tactic (https://github.com/marcusrossel/lean-egg), based on equality saturation as a tactic, which (re)constructs a proof from the E-graph [ 6 ] in Lean. This means that we do not have to trust either the egg tool nor the tactic: if something goes wrong, Lean will not accept the constructed proof. In fact, we found issues with the proof reconstruction from the examples in this project.
The lean-egg tactic works for equational reasoning, i.e. proving equalities as consequences of other equalities (potentially universally quantified), which is exactly what we need to prove implications of laws in Magmas. In many cases, we have laws of the form \(x = y\), where neither set of variables in the left- and right-hand-side of the law is a subset of each other. In this case the laws cannot be used as rewrite rules: it’s not clear what it would be rewritten to, since there are unknowns on both sides of the equation. For these cases we used a simple heuristic, where we instantiate the variables with terms found in the (proof) context, as those are likely to be important for proving the equality.
15.1.2 Results
Out of the possible implications between the \(34\) equations considered in Chapter 2, this method found an additional 86 implications that were not found before. Some of these seem to be missing in the computation of the transitive closure of implications of the equalities (an investigation is in progress), but some of these are genuinely new theorems, and the lean-egg tactic finds good proofs of these (these can be rewritten using calc style with a different tactic, calcify: https://github.com/nomeata/lean-calcify). An example of this is the following proof, found by lean-egg:
Definition 2.9 is equivalent to Definition 2.11.
It was also able to (re)prove Theorem 5.5, albeit with a manually-provided hint (guide, in the sense of [ 6 ] ).
15.2 MagmaEgg
This is a simple but apparently at least somewhat effective Rust theorem prover based on egg e-graph library written for this project.
It proved \(5574\) of the \(24283\) implications in the “only_strongest.txt” file at the time.
The code was originally based on the magma_search pull request, but has been pretty much completely rewritten.
Currently search just uses the egg library in a basic fashion, except that in case there are extra variables not present in the LHS, it has code to instantiate them with all subexpressions of the original goal.
Exporting the proofs to Lean has turned out to be harder than finding the proofs, but a good solution has been implemented (modulo some issues in egg that require to sometimes turn off explanation optimization since it sometimes triggers stack overflows and assert failures) that directly produces proof terms using let/have and Eq.refl, Eq.symm, Eq.trans, Magma.op, a congruence lemma for Magma.op and variables and the hypothesis. I define one letter aliases for them to reduce verbosity.
Possible future work:
Figure out which implications are important to prove and try it on them
Replace the fork-based code with self-execution so that it works on Windows and is less of na hack
Fork egg and fix the buggy and slow length optimization of explanations
Maybe write Lean code directly instead of writing explanation sexps and converting to Lean code in a second run
Fix the generation of extra variable values so it doesn’t take too much time in pathological cases (i.e. goals with 4-6 variables)
Determine whether it actually has some advantages compared to Vampire and lean-egg
Support searching for multiple goal equations at once
Write a custom elaborator for Lean to speed up elaboration
If the Lean kernel turns out to be too slow for some large necessary proofs and thus the custom elaborator is not enough, write a custom verified typechecker
Support having extra rewrite rules, such as other implications that have been found implied by the hypothesis, or simple equalities found by the egraph search itself
Run it with massive computing resources if deemed useful and someone offers those, once it’s a bit more mature