This repository contains a (work-in-progress) equality saturation tactic for Lean based on egg. The tactic is useful for automated equational reasoning. Checkout the Lean/Egg/Tests
directory for examples.
This tactic requires Rust and its package manager Cargo. They are easily installed following the official guide.
To use egg
in your Lean project, add the following line to your lakefile.lean
:
require egg from git "https://github.com/marcusrossel/lean-egg" @ "main"
Then, add import Egg
to the files that require egg
.
The syntax of egg
is very similar to that of simp
or rw
:
example : 0 = 0 := by
egg
example (a b c : Nat) (h₁ : a = b) (h₂ : b = c) : a = c := by
egg [h₁, h₂]
open List in
example (as bs : List α) : reverse (as ++ bs) = (reverse bs) ++ (reverse as) := by
induction as generalizing bs with
| nil => egg [reverse_nil, append_nil, append]
| cons a as ih => egg [ih, append_assoc, reverse_cons, append]
But you can use it to solve some equations which simp
cannot:
variable (a b c d : Int)
example : ((a * b) - (2 * c)) * d - (a * b) = (d - 1) * (a * b) - (2 * c * d) := by
egg [Int.sub_mul, Int.sub_sub, Int.add_comm, Int.mul_comm, Int.one_mul]
Sometimes, egg
needs a little help with finding the correct sequence of rewrites.
You can help out by providing guide terms which nudge egg
in the right direction:
-- From Lean/Egg/Tests/Groups.lean
example [Group G] (a : G) : a⁻¹⁻¹ = a := by
egg [/- group axioms -/] using a⁻¹ * a
And if you want to prove your goal based on an equivalent hypothesis, you can use the from
syntax:
example (h : p ∧ q ∧ r) : r ∧ r ∧ q ∧ p ∧ q ∧ r ∧ p := by
egg [and_comm, and_assoc, and_self] from h
For conditional rewriting, hypotheses can be provided after the rewrites:
example {p q r : Prop} (h₁ : p) (h₂ : p ↔ q) (h₃ : q → (p ↔ r)) : p ↔ r := by
egg [h₂, h₃; h₁]
Note that rewrites are also applied to hypotheses.
- Guided Equality Saturation introduces the original prototype of the
egg
tactic. - Bridging Syntax and Semantics of Lean Expressions in E-Graphs contains a high-level description of how the tactic handles binders and definitional equality.