## calcify - an explanation tactic for Lean

The `calcify`

tactic in this repository will take a proof as generated by
tactics like `simp`

and `rw`

, and shows an equivalent proof by small-step
equational reasoning using `calc`

:

```
example (n : Nat) : 0 + n = 0 + (n * 1) := by
calcify rw [Nat.mul_one, Nat.zero_add]
/-
Try this: calc
0 + n
_ = n := (Nat.zero_add n)
_ = 0 + n := (Eq.symm (Nat.zero_add n))
_ = 0 + n * 1 := congrArg (fun _a => 0 + _a) (Eq.symm (Nat.mul_one n))
-/
```

For more examples, see `Calcify/Basic.lean`

.

It is mostly an experiment and of prototype quality, but maybe you'll enjoy it.

### Usage

This isn’t well tested, but if you are on a new enough version of lean (a
nightly release most likely, or 0.4.7 once it is there), you should be able to
add this repository as a lake dependency and then `import Calcify`

.

### Implementation

The tactic first rewrites the proof term, pushing congruences into `Eq.trans`

,
so that the proof term becomes a list of `Eq.trans`

applications. It is using a
hand-rolled simplification routine because Lean’s `simp`

does not work on proof
terms (as usually they do not matter due to proof irrelvance).

Then that proof term is turned into a `calc`

proof.

### Contact

This was created by Joachim Breitner. Feel free to report issues, create PRs with test cases and more features, or reach out on Zulip.