## Equality Saturation Tactic for Lean

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.

### Setup

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`

.

### Basic Usage

The syntax of `egg`

is very similar to that of `simp`

or `rw`

:

```
import Egg
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:

```
import Egg
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
import Egg
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:

```
import Egg
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:

```
import Egg
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.

### Related Work

- 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.