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