Forward to backward conversion and vice versa

Stream: lean4

[Sid]

Hi,

Are there any algorithms to convert Lean forward reasoning proofs to backward and vice versa?

Thanks

[Edward van de Meent]

could you give an example of what that would look like/what the use would be? because in the type theory of lean, proofs of the same statement are equal, and once a theorem compiles, as far as i know the compiler throws away the actual value...

[Ruben Van de Velde]

Not quite - see the #print command

[Ruben Van de Velde]

But the output is a proof term, which (if it's simple enough) you could present as forward or backward tactic scripts. Still, it depends on what you're actually trying to do

[Edward van de Meent]

in that case, you'd be looking at some sort of delaborator?

[Sid]

Edward van de Meent said:

could you give an example of what that would look like/what the use would be? because in the type theory of lean, proofs of the same statement are equal, and once a theorem compiles, as far as i know the compiler throws away the actual value...

So my goal was to see if I could generate additional data for ML theorem proving in Lean by having the same Lean proof be in a variety of different versions (forward tactics mostly or backward tactics mostly -- to the extent possible -- for example I don't think a proof by contradiction or induction which afaik are backward tactics can always be converted automatically to a forward direct proof) where the Lean proofs are taken from mathlib or other github repos.

[Sid]

Ruben Van de Velde said:

But the output is a proof term, which (if it's simple enough) you could present as forward or backward tactic scripts. Still, it depends on what you're actually trying to do

I see. What do you mean by "simple enough"? Is there a function that would take the proof term and convert whatever can be converted to forward style and the rest to backward style for example?

[Sid]

Edward van de Meent said:

in that case, you'd be looking at some sort of delaborator?

I'm not familiar with a delaborator. Assuming you're referring to this (https://leanprover-community.github.io/mathlib4_docs/Lean/PrettyPrinter/Delaborator/Basic.html), it seems like it does conversion from print to syntax but I think a conversion of terms to tactics would require more than that?

[Edward van de Meent]

from my shallow understanding of the lean metalanguage abilities, a delaborator is a program that turns a term into some kind of string/syntax, which includes (i'm assuming) tactic mode. this could allow you to turn a proof term into a sequence of tactics. i don't know how practical this would be though.