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.