fix: `sorry` extraction from sketch

This commit is contained in:
Leni Aniva 2024-10-03 01:32:43 -07:00
parent 3221cfb45b
commit 850fd89e37
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
3 changed files with 42 additions and 1 deletions

View File

@ -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

36
examples/sketch.py Normal file
View File

@ -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)

2
src

@ -1 +1 @@
Subproject commit bec84f857bd4f80064213fa5646bef4699191290
Subproject commit 143cd289bbc4ea93f0889cf05737c3b6f90a51df