calcify tactic?

Stream: Is there code for X?

[Joachim Breitner]

I really like calc proofs, they are pretty, easy to understand and easier to maintain (as you know what step broke when you change something). But they are sometimes a bit tedious to write out.

Do we have a tactic that works a bit like show_term, but produces a nice sequence of calc steps?
(I could imagine a tactic that mangles the proof term to right-associate all trans rules, distributes cong into trans, and finally writes out the top-level sequence of trans steps a explicit calc steps.)
If not, who would find it useful?

[Eric Wieser]

What do you mean by "distributes cong into trans"?

[Joachim Breitner]

something like congr_arg f (Eq.trans h1 h2) = Eq.trans (congr_arg f h1) (congr_arg f h2).
Or in prose: A proof that takes two rewriting steps under some expression can be turned into a proof that takes two top-level rewriting steps, each under some expression.

[Joachim Breitner]

Of course, things can become arbitrary complicated when the relation isn’t equality, or when there are dependent motives, I expect… but I could imagine it would work well with rewriting simp or rw calls to more explicit forms.
Very much anti-golfing, of course :-)