166 lines
6.0 KiB
Plaintext
166 lines
6.0 KiB
Plaintext
{
|
|
"cells": [
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "aecc5260-56ad-4734-8917-3a4d92910309",
|
|
"metadata": {},
|
|
"source": [
|
|
"# Drafting\n",
|
|
"\n",
|
|
"Pantograph supports drafting (technically the sketch step) from\n",
|
|
"[Draft-Sketch-Prove](https://github.com/wellecks/ntptutorial/tree/main/partII_dsp).\n",
|
|
"Pantograph's drafting feature is more powerful. At any place in the proof, you\n",
|
|
"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.\n",
|
|
"\n",
|
|
"At this point we must introduce the idea of compilation units. Each Lean\n",
|
|
"definition, theorem, constant, etc., is a *compilation unit*. When Pantograph\n",
|
|
"extracts data from Lean source code, it sections the data into these compilation\n",
|
|
"units.\n",
|
|
"\n",
|
|
"For example, consider this sketch produced by a language model prover:\n",
|
|
"```lean\n",
|
|
"theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := by\n",
|
|
" intros n m\n",
|
|
" induction n with\n",
|
|
" | zero =>\n",
|
|
" have h_base: 0 + m = m := sorry\n",
|
|
" have h_symm: m + 0 = m := sorry\n",
|
|
" sorry\n",
|
|
" | succ n ih =>\n",
|
|
" have h_inductive: n + m = m + n := sorry\n",
|
|
" have h_pull_succ_out_from_right: m + Nat.succ n = Nat.succ (m + n) := sorry\n",
|
|
" have h_flip_n_plus_m: Nat.succ (n + m) = Nat.succ (m + n) := sorry\n",
|
|
" have h_pull_succ_out_from_left: Nat.succ n + m = Nat.succ (n + m) := sorry\n",
|
|
" sorry\n",
|
|
"```\n",
|
|
"There are some `sorry`s 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 `sorry`s:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 1,
|
|
"id": "52bd153d-235c-47fa-917e-415d444867a5",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"m : Nat\n",
|
|
"⊢ 0 + m = m\n",
|
|
"m : Nat\n",
|
|
"h_base : 0 + m = m\n",
|
|
"⊢ m + 0 = m\n",
|
|
"m : Nat\n",
|
|
"h_base : 0 + m = m\n",
|
|
"h_symm : m + 0 = m\n",
|
|
"⊢ 0 + m = m + 0\n",
|
|
"m : Nat\n",
|
|
"n : Nat\n",
|
|
"ih : n + m = m + n\n",
|
|
"⊢ n + m = m + n\n",
|
|
"m : Nat\n",
|
|
"n : Nat\n",
|
|
"ih : n + m = m + n\n",
|
|
"h_inductive : n + m = m + n\n",
|
|
"⊢ m + n.succ = (m + n).succ\n",
|
|
"m : Nat\n",
|
|
"n : Nat\n",
|
|
"ih : n + m = m + n\n",
|
|
"h_inductive : n + m = m + n\n",
|
|
"h_pull_succ_out_from_right : m + n.succ = (m + n).succ\n",
|
|
"⊢ (n + m).succ = (m + n).succ\n",
|
|
"m : Nat\n",
|
|
"n : Nat\n",
|
|
"ih : n + m = m + n\n",
|
|
"h_inductive : n + m = m + n\n",
|
|
"h_pull_succ_out_from_right : m + n.succ = (m + n).succ\n",
|
|
"h_flip_n_plus_m : (n + m).succ = (m + n).succ\n",
|
|
"⊢ n.succ + m = (n + m).succ\n",
|
|
"m : Nat\n",
|
|
"n : Nat\n",
|
|
"ih : n + m = m + n\n",
|
|
"h_inductive : n + m = m + n\n",
|
|
"h_pull_succ_out_from_right : m + n.succ = (m + n).succ\n",
|
|
"h_flip_n_plus_m : (n + m).succ = (m + n).succ\n",
|
|
"h_pull_succ_out_from_left : n.succ + m = (n + m).succ\n",
|
|
"⊢ n + 1 + m = m + (n + 1)\n"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"from pantograph import Server\n",
|
|
"\n",
|
|
"sketch = \"\"\"\n",
|
|
"theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := by\n",
|
|
" -- Consider some n and m in Nats.\n",
|
|
" intros n m\n",
|
|
" -- Perform induction on n.\n",
|
|
" induction n with\n",
|
|
" | zero =>\n",
|
|
" -- Base case: When n = 0, we need to show 0 + m = m + 0.\n",
|
|
" -- We have the fact 0 + m = m by the definition of addition.\n",
|
|
" have h_base: 0 + m = m := sorry\n",
|
|
" -- We also have the fact m + 0 = m by the definition of addition.\n",
|
|
" have h_symm: m + 0 = m := sorry\n",
|
|
" -- Combine facts to close goal\n",
|
|
" sorry\n",
|
|
" | succ n ih =>\n",
|
|
" -- Inductive step: Assume n + m = m + n, we need to show succ n + m = m + succ n.\n",
|
|
" -- By the inductive hypothesis, we have n + m = m + n.\n",
|
|
" have h_inductive: n + m = m + n := sorry\n",
|
|
" -- 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.\n",
|
|
" have h_pull_succ_out_from_right: m + Nat.succ n = Nat.succ (m + n) := sorry\n",
|
|
" -- 2. then to flip m + S n to something like S (n + m) we need to use the IH.\n",
|
|
" have h_flip_n_plus_m: Nat.succ (n + m) = Nat.succ (m + n) := sorry\n",
|
|
" -- 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.\n",
|
|
" have h_pull_succ_out_from_left: Nat.succ n + m = Nat.succ (n + m) := sorry\n",
|
|
" -- Combine facts to close goal\n",
|
|
" sorry\n",
|
|
"\"\"\"\n",
|
|
"\n",
|
|
"server = Server()\n",
|
|
"unit, = server.load_sorry(sketch)\n",
|
|
"print(unit.goal_state)"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "0d4dda56-7b7f-4c4c-b59d-af6f857d7788",
|
|
"metadata": {},
|
|
"source": [
|
|
"For an in-depth example, see `experiments/dsp`."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "eaf8e506-a6d1-4e9a-ad7a-f7bbb82e01c6",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
}
|
|
],
|
|
"metadata": {
|
|
"kernelspec": {
|
|
"display_name": "Python 3 (ipykernel)",
|
|
"language": "python",
|
|
"name": "python3"
|
|
},
|
|
"language_info": {
|
|
"codemirror_mode": {
|
|
"name": "ipython",
|
|
"version": 3
|
|
},
|
|
"file_extension": ".py",
|
|
"mimetype": "text/x-python",
|
|
"name": "python",
|
|
"nbconvert_exporter": "python",
|
|
"pygments_lexer": "ipython3",
|
|
"version": "3.12.7"
|
|
}
|
|
},
|
|
"nbformat": 4,
|
|
"nbformat_minor": 5
|
|
}
|