From 850fd89e377d14570d8ec54eb29e33e7ae8a93fc Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 3 Oct 2024 01:32:43 -0700
Subject: [PATCH] fix: `sorry` extraction from sketch

---
 examples/README.md |  5 +++++
 examples/sketch.py | 36 ++++++++++++++++++++++++++++++++++++
 src                |  2 +-
 3 files changed, 42 insertions(+), 1 deletion(-)
 create mode 100644 examples/sketch.py

diff --git a/examples/README.md b/examples/README.md
index 41e702e..37e099f 100644
--- a/examples/README.md
+++ b/examples/README.md
@@ -18,6 +18,7 @@ This would generate compiled `.olean` files. Then run one of the examples from t
 project root:
 ``` sh
 poetry run examples/aesop.py
+poetry run examples/sketch.py
 poetry run examples/data.py
 ```
 
@@ -26,3 +27,7 @@ build`! Moreover, the version of the Lean used in the example folder (including
 dependencies in `lakefile.lean` and `lean-toolchain`) **must match exactly**
 with the version in `src/`!
 
+* `aesop.py`: Example of how to use the `aesop` tactic
+* `data.py`: Example of loading training data
+* `sketch.py`: Example of loading a sketch
+
diff --git a/examples/sketch.py b/examples/sketch.py
new file mode 100644
index 0000000..0f9bb74
--- /dev/null
+++ b/examples/sketch.py
@@ -0,0 +1,36 @@
+#!/usr/bin/env python3
+
+from pantograph.server 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
+"""
+
+if __name__ == '__main__':
+    server = Server()
+    state0, = server.load_sorry(sketch)
+    print(state0)
diff --git a/src b/src
index bec84f8..143cd28 160000
--- a/src
+++ b/src
@@ -1 +1 @@
-Subproject commit bec84f857bd4f80064213fa5646bef4699191290
+Subproject commit 143cd289bbc4ea93f0889cf05737c3b6f90a51df