Code for turning goal state strings into theorem statements

Stream: Machine Learning for Theorem Proving

[Kyle Miller]

I thought I'd share some Python code I wrote today that parses pretty printed goal strings and creates a theorem statement from it. This is really wrong to do — much better would be to create the theorem statement by metaprogramming from within Lean and pretty print it! — but I'm sure people here have been in situations where you only have pretty printed goal states available.

https://gist.github.com/kmill/5991f18449fed6be4eb6d661fdd73742

This is only lightly tested, and I'm sure there are unhandled edge cases. Feel free to share your own code here, or make improvements to mine.

Example:

ex4 = """
V✝ : Type u_1
G✝ : SimpleGraph V✝
inst✝³ : Fintype V✝
inst✝² : DecidableRel G✝.Adj
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u w v : V
q : G.Walk u v
v✝ : V
hv : G.Adj v v✝
p : G.Walk v✝ w
h_nontrivial : (q.append (Walk.cons hv p)).length > 0
h : (Walk.cons hv p).length > 0
⊢ G.degree v ≥ 1
"""
print(goal_to_theorem("my_thm4", ex4))

outputs

theorem my_thm4 (V_2 : Type u_1) (G_2 : SimpleGraph V_2) [Fintype V_2] [DecidableRel G_2.Adj]
    (V : Type u_1) (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj]
    (u w v : V) (q : G.Walk u v) (v_2 : V) (hv : G.Adj v v_2) (p : G.Walk v_2 w)
    (h_nontrivial : (q.append (Walk.cons hv p)).length > 0)
    (h : (Walk.cons hv p).length > 0) :
    G.degree v ≥ 1 :=
  sorry

[Kyle Miller]

Hmm, I just realized the logic I wrote to try to split a local let decl on the correct := is incorrect (I assumed let/have would start with a space, but they could start with a ( or other bracket too). It's a really unlikely situation that there's a let expression in the type of a variable though, and I'll fix it once it actually causes issue.