26138a5362
This PR implements equality propagation in the new commutative ring procedure in `grind`. The idea is to propagate implied equalities back to the `grind` core module that does congruence closure. In the following example, the equalities: `x^2*y = 1` and `x*y^2 - y = 0` imply that `y*x` is equal to `y*x*y`, which implies by congruence that `f (y*x) = f (y*x*y)`. ```lean example [CommRing α] (x y : α) (f : α → Nat) : x^2*y = 1 → x*y^2 - y = 0 → f (y*x) = f (y*x*y) := by grind +ring ``` |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||