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.