Zulip Chat Archive

Stream: Is there code for X?

Topic: calcify tactic?


Joachim Breitner (Sep 17 2023 at 15:47):

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 (Sep 17 2023 at 15:50):

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

Joachim Breitner (Sep 17 2023 at 15:51):

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 (Sep 17 2023 at 15:54):

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 :-)


Last updated: Dec 20 2023 at 11:08 UTC