Zulip Chat Archive

Stream: new members

Topic: automatically turn tactic proof into calc proof?


view this post on Zulip Chris M (Jun 29 2020 at 06:09):

Is it possible to automatically turn a tactic proof that only rewrites equations into a calc proof? It seems like this shouldn't be fundamentally hard.

view this post on Zulip Scott Morrison (Jun 29 2020 at 06:37):

Are you imagining a tactic that is only allowed to inspect the proof term (i.e. something like find_calc_proof { rw [...] }) or something that you run instead of rw, e.g. rw? [...]? The second option seems very doable.

view this post on Zulip Scott Morrison (Jun 29 2020 at 06:37):

You'd have the usual problem the round-tripping pp output is not 100% reliable. But it's often enough good.

view this post on Zulip Chris M (Jun 29 2020 at 06:38):

Sorry, to clarify, I'm not necessarily imagining a tactic at all. I'm imagining a program that takes as input a well-formed tactic proof, and outputs a well-formed calc proof. Since calc proofs are a little harder to write, but easier to read.

view this post on Zulip Scott Morrison (Jun 29 2020 at 06:39):

Oh --- better to write tactics. :-) You'll have to be talking to Lean anyway to generate the intermediate expressions.

view this post on Zulip Scott Morrison (Jun 29 2020 at 06:39):

The first option is doable as well, I'd guess --- rw produces pretty regularly shaped proof terms from which you can reconstruct what happened.

view this post on Zulip Chris M (Jun 29 2020 at 06:40):

Yes, I'm imagining writing a proof in tactic mode, and once the proof is finished, copy paste the proof into a "proof rewriting program" which then gives me the calc proof with all the intermediate steps clearly stated, so that others can read it more easily.

view this post on Zulip Jannis Limperg (Jun 29 2020 at 14:48):

I think this would be very hard in general. Tactics often don't care about producing intelligible terms, so a parser that tries to figure out what steps were taken would have to determine which parts of the term are relevant and which are incidental complexity. If you limit yourself to certain tactics (e.g. only chains of rw), it might be doable, but your parser will then be strongly coupled to the implementations of these tactics.

view this post on Zulip Scott Morrison (Jun 30 2020 at 03:45):

It will be much better to do this as a replacement/modifier for rw, so the scope is narrow. It should definitely be done as a tactic, not as some external program.


Last updated: May 13 2021 at 20:13 UTC