Drafting

Pantograph supports drafting (technically the sketch step) from Draft-Sketch-Prove. Pantograph’s drafting feature is more powerful. At any place in the proof, you can replace an expression with sorry, and the sorry will become a goal. Any type errors will also become goals. In order to detect whether type errors have occurred, the user can look at the messages from each compilation unit.

At this point we must introduce the idea of compilation units. Each Lean definition, theorem, constant, etc., is a compilation unit. When Pantograph extracts data from Lean source code, it sections the data into these compilation units.

For example, consider this sketch produced by a language model prover:

theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := by
   intros n m
   induction n with
   | zero =>
     have h_base: 0 + m = m := sorry
     have h_symm: m + 0 = m := sorry
     sorry
   | succ n ih =>
     have h_inductive: n + m = m + n := sorry
     have h_pull_succ_out_from_right: m + Nat.succ n = Nat.succ (m + n) := sorry
     have h_flip_n_plus_m: Nat.succ (n + m) = Nat.succ (m + n) := sorry
     have h_pull_succ_out_from_left: Nat.succ n + m = Nat.succ (n + m) := sorry
     sorry

There are some sorrys that we want to solve automatically with hammer tactics. We can do this by drafting. Feeding this into the drafting feature produces one goal state (corresponding to the one compilation unit) containing as many goals as the draft has sorrys:

from pantograph import Server

sketch = """
theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := by
   -- Consider some n and m in Nats.
   intros n m
   -- Perform induction on n.
   induction n with
   | zero =>
     -- Base case: When n = 0, we need to show 0 + m = m + 0.
     -- We have the fact 0 + m = m by the definition of addition.
     have h_base: 0 + m = m := sorry
     -- We also have the fact m + 0 = m by the definition of addition.
     have h_symm: m + 0 = m := sorry
     -- Combine facts to close goal
     sorry
   | succ n ih =>
     -- Inductive step: Assume n + m = m + n, we need to show succ n + m = m + succ n.
     -- By the inductive hypothesis, we have n + m = m + n.
     have h_inductive: n + m = m + n := sorry
     -- 1. Note we start with: Nat.succ n + m = m + Nat.succ n, so, pull the succ out from m + Nat.succ n on the right side from the addition using addition facts Nat.add_succ.
     have h_pull_succ_out_from_right: m + Nat.succ n = Nat.succ (m + n) := sorry
     -- 2. then to flip m + S n to something like S (n + m) we need to use the IH.
     have h_flip_n_plus_m: Nat.succ (n + m) = Nat.succ (m + n) := sorry
     -- 3. Now the n & m are on the correct sides Nat.succ n + m = Nat.succ (n + m), so let's use the def of addition to pull out the succ from the addition on the left using Nat.succ_add.
     have h_pull_succ_out_from_left: Nat.succ n + m = Nat.succ (n + m) := sorry
     -- Combine facts to close goal
     sorry
"""

server = Server()
unit, = server.load_sorry(sketch)
print(unit.goal_state)

m : Nat
⊢ 0 + m = m
m : Nat
h_base : 0 + m = m
⊢ m + 0 = m
m : Nat
h_base : 0 + m = m
h_symm : m + 0 = m
⊢ 0 + m = m + 0
m : Nat
n : Nat
ih : n + m = m + n
⊢ n + m = m + n
m : Nat
n : Nat
ih : n + m = m + n
h_inductive : n + m = m + n
⊢ m + n.succ = (m + n).succ
m : Nat
n : Nat
ih : n + m = m + n
h_inductive : n + m = m + n
h_pull_succ_out_from_right : m + n.succ = (m + n).succ
⊢ (n + m).succ = (m + n).succ
m : Nat
n : Nat
ih : n + m = m + n
h_inductive : n + m = m + n
h_pull_succ_out_from_right : m + n.succ = (m + n).succ
h_flip_n_plus_m : (n + m).succ = (m + n).succ
⊢ n.succ + m = (n + m).succ
m : Nat
n : Nat
ih : n + m = m + n
h_inductive : n + m = m + n
h_pull_succ_out_from_right : m + n.succ = (m + n).succ
h_flip_n_plus_m : (n + m).succ = (m + n).succ
h_pull_succ_out_from_left : n.succ + m = (n + m).succ
⊢ n + 1 + m = m + (n + 1)

For an in-depth example, see experiments/dsp.