automatically turn tactic proof into calc proof?

Stream: new members

[Chris M]

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.

[Scott Morrison]

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.

[Scott Morrison]

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

[Chris M]

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.

[Scott Morrison]

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

[Scott Morrison]

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

[Chris M]

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.

[Jannis Limperg]

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.

[Scott Morrison]

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.