simp_to_steps

Stream: mathlib4

[Joachim Breitner]

I was just porting a simp_only line that didn’t do what it did in mathlib3. My (second) approach was to edit the lean3 proof and turn it into many simp_rw […] lines with just one lemma, and permutate and duplicate until it went through. Then that sequence of steps worked fine in lean4 (and some lemmas were not needed at all).

This made me wish for a variant of squeeze_simp that would not print one simp only […] line, but something like that: A step-by-step reproduction of the proof using simpler tactics (maybe simp_rw, or even simpler), possibly even in an equational reasoning style with all intermediate states included – useful when porting, and in (simple) cases may even be a nicer, more explicit form of the proof altogether. It is anti-golf, however :-)

[Eric Wieser]

Note that it's somewhat misleading to claim simp_rw is a simpler tactic, as it's actually implemented in terms of repeated simp only!

[Reid Barton]

I was also thinking about something like this the other day. A more declarative version of simp only in the middle of the proof could be suffices BLAH, { simpa }, where BLAH is whatever the goal is supposed to be after the simp only.

[Reid Barton]

And then you can simp only-ify the simpa inside for performance reasons, but you can also throw away and regenerate the lemma list without losing any information.