Tactic style to term style

Stream: lean4

[Sid]

Hi,

Is there a way to automatically convert a tactic style lean proof into a term style lean proof? I noticed that if I print even a tactic style proof, Lean shows the term style version so I'm wondering if there's a way to convert without printing and parsing.

Thanks

[Adam Topaz]

You can use show_term.

[Edward van de Meent]

or even by?

[Adam Topaz]

example (p q : Prop) (h : p → q) (hp : p) : q := show_term by
  apply h
  assumption

[Edward van de Meent]

corresponding for by?:

example (p q : Prop) (h : p → q) (hp : p) : q := by?
  apply h
  assumption

[Sid]

As a followup to this, is there a way to convert term style back to tactic style in an automated way?

[Julian Berman]

exact <yourterm> is (the simplest) tactic which gets you back into term mode. I assume you don't mean that though? You mean whether there's a way to take some complicated term and "decompile" it into some more readable tactics? AFAIK there isn't anything automated to do so.

[Sid]

Julian Berman said:

exact <yourterm> is (the simplest) tactic which gets you back into term mode. I assume you don't mean that though? You mean whether there's a way to take some complicated term and "decompile" it into some more readable tactics? AFAIK there isn't anything automated to do so.

Yes the latter is what I meant. I'm guessing it's possible in theory tho and there's just not an implementation or are there theoretical obstacles as well?

Also is there a reference on how the Lean compilation from tactics -> proof terms works?

[Julian Berman]

(Completely speculating) I think having such a thing is generally not considered very interesting, because proofs which involve complicated terms are often that way because they've been "golfed" -- which is (meant to be) an indication that the proof isn't interesting / doesn't contain much mathematical value. It's of course possible for that to be wrong, but yeah as a general rule I think most of the Mathlib proofs that are inscrutable in this way are the way they are precisely because they're not really intended for a human to read them anymore.

[Julian Berman]

The theoretical obstacle would I think be similar to other "humanization" cases -- there probably are multiple ways to decompile what you have, including the most direct one being what I mentioned, i.e. defining decompile(term) to literally be exact term -- so what constitutes a "good" output is going to be somewhat subjective and probably not unique

[Sid]

Sid said:

As a followup to this, is there a way to convert term style back to tactic style?

I see. What if a reference tactic style proof is available? My motivation here is basically to convert Lean proofs that use backward tactics into ones that use forward tactics. It doesn't seem like there's a way to do this directly in an automatic way (https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Forward.20to.20backward.20conversion.20and.20vice.20versa) so I was thinking perhaps there might be if I go through proof terms. The motivation is to generate additional training data for ML models

[Kyle Miller]

I've had it in the back of my mind to write a "tactify" program decompile terms into tactics.

[Kyle Miller]

Sid said:

Also is there a reference on how the Lean compilation from tactics -> proof terms works?

Not really, though you can always read the source code for any given tactic. They themselves are the programs that create proof terms.

[Kim Morrison]

Kyle Miller said:

I've had it in the back of my mind to write a "tactify" program decompile terms into tactics.

I tried this once, even had a branch somewhere, but ... Kyle would do a better job. :-)