Some thoughts on tactics and proof readability / portability

Stream: new members

[ElCondor]

Hi!

As a newcomer to Lean I would like to share a thought I had (and which I suppose has already been discussed?).

With Lean, using some tactic like simp (or norm_num, ...) I can prove a lemma directly:

lemma a_more_or_less_complex_lemma: ... := by simp

From the proof-writer point of view, this is very nice (if the tactic succeeds) because I can move move on to my other goals.

From the proof-reader point of view, this is less nice because I might be interested to know the details of the proof of a_more_or_less_complex_lemma, especially if it's complex, and the way it is written doesn't make anything explicit.

Also, if I want to take this proof and port it to another proof system, there is no guarantee that there will be a similar strategy able to solve that lemma.
There even is no guarantee that this lemma will be portable from one version of Lean to another (well, there is no guarantee either if the steps are detailed but at least we have an idea what is going on).

How should that concern be addressed?
Also, when a tactic like simp in my example successfully proves a_more_or_less_complex_lemma, is there some easy way to turn this into an explicit proof? (the only way I found is to #print a_more_or_less_complex_lemma and see what it does but the presentation isn't really reader-friendly)

[Kyle Miller]

One thing you can do for a more-explicit proof is use simp?, which tells you exactly which lemmas simp used.

The simp tactic doesn't generate a particularly readable proof. It'd be neat if it could output a proof script using conv tactics and rw.

[Joachim Breitner]

Or even an explicit calc for when you really want a readable human like proof! (I dabbled in that direction once, but got stuck somewhere. Will maybe pick up the calcifier once I am more versed in metaprogramming and have some slack time)