show step by step derivation from a tactic based proof?

Stream: new members

[Krishna Padmasola]

Hi friends, Sometimes it is difficult to understand the lemmas and theorems that were used to prove a hypothesis, even when one has a verified proof using tactics.

Does Lean have a proof tracing mechanism that can show the step by step derivation showing each of the lemmas/theorems involved in the chain of reasoning ? This can help demystify the tactic based proofs for the beginner to whom the tactic looks like a black(magic)box.

thanks for your help,
Krishna

[Luigi Massacci]

For some tactics (eg, ring) there's fairly detailed documentation as to what it's doing, while others implement classical algorithms (eg: linarith) you can look up. A not very helpful way to do what you want is to use show_term (or put a ? after the by) which will print the actual proof term that has been constructed, but it is rarely easy to parse for humans. Unfortunately this is more or less the best you can do as far as I know

[suhr]

You can use #print to see the proof term of your lemma. For example: #print Nat.mod_add_div.

This can help demystify the tactic based proofs for the beginner to whom the tactic looks like a black(magic)box.

The best way in my opinion is to avoid mystifying them in the first place. Teach terms first and then introduce tactics as an automatization.