doc: Add comprehensive documentation
fix: Typo in `Server.tactic_invocations`
This commit is contained in:
parent
75221cca0b
commit
7a2278cb70
GPG Key ID:
4D9B1C8D10EA4C50
|
|
@ -5,7 +5,8 @@ parts:
|
|||
chapters:
|
||||
- file: setup
|
||||
- file: goal
|
||||
- file: proof_search
|
||||
- file: agent-search
|
||||
- file: data
|
||||
- file: drafting
|
||||
- caption: API Documentation
|
||||
chapters:
|
||||
|
|
|
|||
|
|
@ -0,0 +1,155 @@
|
|||
{
|
||||
"cells": [
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "ec3abb52-d7cd-471f-b3b7-2d9681c79360",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"# Search\n",
|
||||
"\n",
|
||||
"Pantograph supports basic proof search. In this case, Pantograph treats goals as nodes on an and-or tree. The user supplies an agent which should provide two functions:\n",
|
||||
"\n",
|
||||
"1. *Tactic*: Which tactic should be used on a goal?\n",
|
||||
"2. *Guidance*: What is the search priority on a goal?\n",
|
||||
"\n",
|
||||
"The user agent should inherit from `pantograph.search.Agent`. Here is a brute force agent example:"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 1,
|
||||
"id": "959458f5-02e4-4f73-ae28-16a756aebed9",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"from typing import Optional\n",
|
||||
"import collections\n",
|
||||
"from pantograph import Server\n",
|
||||
"from pantograph.search import Agent\n",
|
||||
"from pantograph.expr import GoalState, Tactic"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 2,
|
||||
"id": "8b402602-3ae5-43e4-9a62-2fa9e2c039fa",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"class DumbAgent(Agent):\n",
|
||||
"\n",
|
||||
" def __init__(self):\n",
|
||||
" super().__init__()\n",
|
||||
"\n",
|
||||
" self.goal_tactic_id_map = collections.defaultdict(lambda : 0)\n",
|
||||
" self.intros = [\n",
|
||||
" \"intro\",\n",
|
||||
" ]\n",
|
||||
" self.tactics = [\n",
|
||||
" \"intro h\",\n",
|
||||
" \"cases h\",\n",
|
||||
" \"apply Or.inl\",\n",
|
||||
" \"apply Or.inr\",\n",
|
||||
" ]\n",
|
||||
" self.no_space_tactics = [\n",
|
||||
" \"assumption\",\n",
|
||||
" ]\n",
|
||||
"\n",
|
||||
" def next_tactic(\n",
|
||||
" self,\n",
|
||||
" state: GoalState,\n",
|
||||
" goal_id: int,\n",
|
||||
" ) -> Optional[Tactic]:\n",
|
||||
" key = (state.state_id, goal_id)\n",
|
||||
" i = self.goal_tactic_id_map[key]\n",
|
||||
"\n",
|
||||
" target = state.goals[goal_id].target\n",
|
||||
" if target.startswith('∀'):\n",
|
||||
" tactics = self.intros\n",
|
||||
" elif ' ' in target:\n",
|
||||
" tactics = self.tactics\n",
|
||||
" else:\n",
|
||||
" tactics = self.no_space_tactics\n",
|
||||
"\n",
|
||||
" if i >= len(tactics):\n",
|
||||
" return None\n",
|
||||
"\n",
|
||||
" self.goal_tactic_id_map[key] = i + 1\n",
|
||||
" return tactics[i]"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "665db9d0-5fff-4b26-9cea-32d06a6e1e04",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Execute the search with `agent.search`."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 3,
|
||||
"id": "1c7961d1-b1fa-498c-ab75-16feb784ca2c",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"data": {
|
||||
"text/plain": [
|
||||
"SearchResult(n_goals_root=1, duration=0.7717759609222412, success=True, steps=16)"
|
||||
]
|
||||
},
|
||||
"execution_count": 3,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"server = Server()\n",
|
||||
"agent = DumbAgent()\n",
|
||||
"goal_state = server.goal_start(\"∀ (p q: Prop), Or p q -> Or q p\")\n",
|
||||
"agent.search(server=server, goal_state=goal_state, verbose=False)"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "141e0116-cbb6-4957-aaea-2a1100f80ece",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"## Automatic and Manual Modes\n",
|
||||
"\n",
|
||||
"The agent chooses one goal and executes a tactic on this goal. What happens to the other goals that are not chosen? By default, the server runs in automatic mode. In automatic mode, all other goals are automatically inherited by a child state, so a user agent could declare a proof finished when there are no more goals remaining in the current goal state.\n",
|
||||
"\n",
|
||||
"Some users may wish to handle sibling goals manually. For example, Aesop's treatment of metavariable coupling is not automatic. To do this, pass the flag `options={ \"automaticMode\" : False }` to the `Server` constructor."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"id": "2090e538-d196-4923-937c-b83fedf1d9a2",
|
||||
"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.6"
|
||||
}
|
||||
},
|
||||
"nbformat": 4,
|
||||
"nbformat_minor": 5
|
||||
}
|
||||
|
|
@ -0,0 +1,167 @@
|
|||
{
|
||||
"cells": [
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "fe7a3037-5c49-4097-9a5d-575b958cc7f8",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"# Data Extraction"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 1,
|
||||
"id": "fc68ad1d-e64c-48b7-9461-50d872d30473",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"import os\n",
|
||||
"from pathlib import Path\n",
|
||||
"from pantograph.server import Server"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "fd13c644-d731-4f81-964e-584bbd43e51c",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"## Tactic Invocation\n",
|
||||
"\n",
|
||||
"Pantograph can extract tactic invocation data from a Lean file. A **tactic\n",
|
||||
"invocation** is a tuple containing the before and after goal states, and the\n",
|
||||
"tactic which converts the \"before\" state to the \"after\" state.\n",
|
||||
"\n",
|
||||
"To extract tactic invocation data, use `server.tactic_invocations(file_name)`\n",
|
||||
"and supply the file name of the input Lean file."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 2,
|
||||
"id": "a0a2a661-e357-4b80-92d1-4172670ab061",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"$PWD: /home/aniva/Projects/atp/PyPantograph/examples/Example\n",
|
||||
"==== #0 ====\n",
|
||||
"/-- Ensure that Aesop is running -/\n",
|
||||
"example : α → α :=\n",
|
||||
" by aesop\n",
|
||||
"\n",
|
||||
"\n",
|
||||
"==== #1 ====\n",
|
||||
"example : ∀ (p q: Prop), p ∨ q → q ∨ p := by\n",
|
||||
" intro p q h\n",
|
||||
" -- Here are some comments\n",
|
||||
" cases h\n",
|
||||
" . apply Or.inr\n",
|
||||
" assumption\n",
|
||||
" . apply Or.inl\n",
|
||||
" assumption\n",
|
||||
"\n",
|
||||
"==== Invocations ====\n",
|
||||
"α : Sort ?u.7\n",
|
||||
"⊢ α → α\n",
|
||||
"aesop\n",
|
||||
"\n",
|
||||
"\n",
|
||||
"⊢ ∀ (p q : Prop), p ∨ q → q ∨ p\n",
|
||||
"intro p q h\n",
|
||||
"p q : Prop\n",
|
||||
"h : p ∨ q\n",
|
||||
"⊢ q ∨ p\n",
|
||||
"\n",
|
||||
"p q : Prop\n",
|
||||
"h : p ∨ q\n",
|
||||
"⊢ q ∨ p\n",
|
||||
"cases h\n",
|
||||
"case inl\n",
|
||||
"p q : Prop\n",
|
||||
"h✝ : p\n",
|
||||
"⊢ q ∨ p\n",
|
||||
"case inr p q : Prop h✝ : q ⊢ q ∨ p\n",
|
||||
"\n",
|
||||
"case inl\n",
|
||||
"p q : Prop\n",
|
||||
"h✝ : p\n",
|
||||
"⊢ q ∨ p\n",
|
||||
"apply Or.inr\n",
|
||||
"case inl.h\n",
|
||||
"p q : Prop\n",
|
||||
"h✝ : p\n",
|
||||
"⊢ p\n",
|
||||
"\n",
|
||||
"case inl.h\n",
|
||||
"p q : Prop\n",
|
||||
"h✝ : p\n",
|
||||
"⊢ p\n",
|
||||
"assumption\n",
|
||||
"\n",
|
||||
"\n",
|
||||
"case inr\n",
|
||||
"p q : Prop\n",
|
||||
"h✝ : q\n",
|
||||
"⊢ q ∨ p\n",
|
||||
"apply Or.inl\n",
|
||||
"case inr.h\n",
|
||||
"p q : Prop\n",
|
||||
"h✝ : q\n",
|
||||
"⊢ q\n",
|
||||
"\n",
|
||||
"case inr.h\n",
|
||||
"p q : Prop\n",
|
||||
"h✝ : q\n",
|
||||
"⊢ q\n",
|
||||
"assumption\n",
|
||||
"\n",
|
||||
"\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"project_path = Path(os.getcwd()).parent.resolve() / 'examples/Example'\n",
|
||||
"print(f\"$PWD: {project_path}\")\n",
|
||||
"server = Server(imports=['Example'], project_path=project_path)\n",
|
||||
"units, invocations = server.tactic_invocations(project_path / \"Example.lean\")\n",
|
||||
"for i, u in enumerate(units):\n",
|
||||
" print(f\"==== #{i} ====\")\n",
|
||||
" print(u)\n",
|
||||
"print(\"==== Invocations ====\")\n",
|
||||
"for i in invocations:\n",
|
||||
" print(f\"{i.before}\\n{i.tactic}\\n{i.after}\\n\")"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"id": "51f5398b-5416-4dc1-81cd-6d2514758232",
|
||||
"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.6"
|
||||
}
|
||||
},
|
||||
"nbformat": 4,
|
||||
"nbformat_minor": 5
|
||||
}
|
||||
|
|
@ -0,0 +1,165 @@
|
|||
{
|
||||
"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.\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",
|
||||
"state0, = server.load_sorry(sketch)\n",
|
||||
"print(state0)"
|
||||
]
|
||||
},
|
||||
{
|
||||
"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.6"
|
||||
}
|
||||
},
|
||||
"nbformat": 4,
|
||||
"nbformat_minor": 5
|
||||
}
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
# Drafting
|
||||
|
||||
Pantograph supports drafting from
|
||||
[Draft-Sketch-Prove](https://github.com/wellecks/ntptutorial/tree/main/partII_dsp).
|
||||
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.
|
||||
|
||||
For an in-depth example, see `experiments/dsp`.
|
||||
|
||||
|
|
@ -0,0 +1,315 @@
|
|||
{
|
||||
"cells": [
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "c5106980-4850-4bea-a333-5a1b2e4d1dc5",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"# Goals and Tactics\n",
|
||||
"\n",
|
||||
"Executing tactics in Pantograph is simple. To start a proof, call the\n",
|
||||
"`Server.goal_start` function and supply an expression."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 1,
|
||||
"id": "3257de2b-41ca-4cfe-b66c-1ef4781c98b0",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"from pantograph import Server\n",
|
||||
"from pantograph.expr import TacticHave, TacticCalc, TacticExpr"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 2,
|
||||
"id": "6783d478-d8c7-4c4e-a56e-8170384297ef",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"server = Server()\n",
|
||||
"state0 = server.goal_start(\"forall (p q: Prop), Or p q -> Or q p\")"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "bfe5a9df-33c2-4538-a9ce-fc0e02c92ff2",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"This creates a *goal state*, which consists of a finite number of goals. In this\n",
|
||||
"case since it is the beginning of a state, it has only one goal."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 3,
|
||||
"id": "eefc9094-9574-4f92-9aa2-c39beb85389b",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"\n",
|
||||
"⊢ forall (p q: Prop), Or p q -> Or q p\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"print(state0)"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "26dbe212-e09e-42dd-ab15-65ee2fba6234",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"To execute a tactic on a goal state, use `Server.goal_tactic`. This function\n",
|
||||
"takes a goal id and a tactic. Most Lean tactics are strings."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 4,
|
||||
"id": "c907dbb6-4d6a-4aa7-b173-60220165ba9e",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"a : Prop\n",
|
||||
"⊢ ∀ (q : Prop), a ∨ q → q ∨ a\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"state1 = server.goal_tactic(state0, goal_id=0, tactic=\"intro a\")\n",
|
||||
"print(state1)"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "9978fdcf-a12b-4f22-9551-5e04c262e5e0",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Executing a tactic produces a new goal state. If this goal state has no goals,\n",
|
||||
"the proof is complete. You can recover the usual form of a goal with `str()`"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 5,
|
||||
"id": "16595c5e-2285-49d5-8340-397ad1e6c9e7",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"data": {
|
||||
"text/plain": [
|
||||
"'a : Prop\\n⊢ ∀ (q : Prop), a ∨ q → q ∨ a'"
|
||||
]
|
||||
},
|
||||
"execution_count": 5,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"str(state1.goals[0])"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "67f2a75d-6851-4393-bac9-a091400f1906",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"## Error Handling and GC\n",
|
||||
"\n",
|
||||
"When a tactic fails, it throws an exception:"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 6,
|
||||
"id": "c9784ba2-3810-4f80-a6c4-33d5eef3003e",
|
||||
"metadata": {
|
||||
"scrolled": true
|
||||
},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"[\"tactic 'assumption' failed\\na : Prop\\n⊢ ∀ (q : Prop), a ∨ q → q ∨ a\"]\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"try:\n",
|
||||
" state2 = server.goal_tactic(state1, goal_id=0, tactic=\"assumption\")\n",
|
||||
" print(\"Should not reach this\")\n",
|
||||
"except Exception as e:\n",
|
||||
" print(e)"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "1ae60d9e-8656-4f26-b495-d04bced250fc",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"A state with no goals is considered solved"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 7,
|
||||
"id": "1cb96b19-d3bb-4533-abeb-a7dbc5bc8c3e",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"data": {
|
||||
"text/plain": [
|
||||
"GoalState(state_id=5, goals=[], _sentinel=[0, 1])"
|
||||
]
|
||||
},
|
||||
"execution_count": 7,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"state0 = server.goal_start(\"forall (p : Prop), p -> p\")\n",
|
||||
"state1 = server.goal_tactic(state0, goal_id=0, tactic=\"intro\")\n",
|
||||
"state2 = server.goal_tactic(state1, goal_id=0, tactic=\"intro h\")\n",
|
||||
"state3 = server.goal_tactic(state2, goal_id=0, tactic=\"exact h\")\n",
|
||||
"state3"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "a2945e71-e583-4ae0-9c0f-83035f0492f2",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Execute `server.gc()` once in a while to delete unused goals."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 8,
|
||||
"id": "d53624ff-c720-4847-98f7-28e109eb76e7",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"server.gc()"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "0b59e05e-7d8c-4fad-b8ca-375ea995ea5b",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"## Special Tactics\n",
|
||||
"\n",
|
||||
"Lean has special provisions for some tactics. This includes `have`, `let`,\n",
|
||||
"`calc`. To execute one of these tactics, create a `TacticHave`, `TacticLet`,\n",
|
||||
"`TacticCalc` instance and feed it into `server.goal_tactic`"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 9,
|
||||
"id": "526d620b-064f-4ec0-a7b2-6a1ef3c6f6e7",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"\n",
|
||||
"⊢ 2 = 1 + 1\n",
|
||||
"h : 2 = 1 + 1\n",
|
||||
"⊢ 1 + 1 = 2\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"state0 = server.goal_start(\"1 + 1 = 2\")\n",
|
||||
"state1 = server.goal_tactic(state0, goal_id=0, tactic=TacticHave(branch=\"2 = 1 + 1\", binder_name=\"h\"))\n",
|
||||
"print(state1)"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "c415d436-ed0d-475f-bf5e-b8dc63954c7e",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"The `TacticExpr` \"tactic\" parses an expression and assigns it to the current\n",
|
||||
"goal. This leverages Lean's type unification system and is as expressive as\n",
|
||||
"Lean expressions. Many proofs in Mathlib4 are written in a mixture of expression\n",
|
||||
"and tactic forms."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 10,
|
||||
"id": "e1f06441-4d77-45a7-a1c3-b800b96a8105",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"state0 = server.goal_start(\"forall (p : Prop), p -> p\")\n",
|
||||
"state1 = server.goal_tactic(state0, goal_id=0, tactic=\"intro p\")\n",
|
||||
"state2 = server.goal_tactic(state1, goal_id=0, tactic=TacticExpr(\"fun h => h\"))\n",
|
||||
"print(state2)"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "d6bcd026-507b-4b1c-8dee-006df53636b0",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"To execute the `conv` tactic, use `server.goal_conv_begin` to enter conv mode on\n",
|
||||
"one goal, and use `server.goal_conv_end` to exit from conv mode. Pantograph will\n",
|
||||
"provide interactive feedback upon every tactic executed in `conv` mode."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"id": "2b0b27c6-0c69-4255-aed1-c0713c227ccc",
|
||||
"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.6"
|
||||
}
|
||||
},
|
||||
"nbformat": 4,
|
||||
"nbformat_minor": 5
|
||||
}
|
||||
26
docs/goal.md
26
docs/goal.md
|
|
@ -1,26 +0,0 @@
|
|||
# Goals and Tactics
|
||||
|
||||
Executing tactics in Pantograph is very simple. To start a proof, call the
|
||||
`Server.goal_start` function and supply an expression.
|
||||
|
||||
```python
|
||||
from pantograph import Server
|
||||
|
||||
server = Server()
|
||||
state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
|
||||
```
|
||||
|
||||
This creates a *goal state*, which consists of a finite number of goals. In this
|
||||
case since it is the beginning of a state, it has only one goal. `print(state0)` gives
|
||||
|
||||
```
|
||||
GoalState(state_id=0, goals=[Goal(variables=[], target='forall (p : Prop), p -> p', name=None, is_conversion=False)], _sentinel=[])
|
||||
```
|
||||
|
||||
To execute a tactic on a goal state, use `Server.goal_tactic`. This function
|
||||
takes a goal id and a tactic. Most Lean tactics are strings.
|
||||
|
||||
```python
|
||||
state1 = server.goal_tactic(state0, goal_id=0, tactic="intro a")
|
||||
```
|
||||
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
# Intro
|
||||
# Introduction
|
||||
|
||||
This is Pantograph, an machine-to-machine interaction interface for Lean 4.
|
||||
Its main purpose is to train and evaluate theorem proving agents. The main
|
||||
|
|
|
|||
|
|
@ -1,14 +0,0 @@
|
|||
# Proof Search
|
||||
|
||||
Inherit from the `pantograph.search.Agent` class to create your own search agent.
|
||||
```python
|
||||
from pantograph.search import Agent
|
||||
|
||||
class UnnamedAgent(Agent):
|
||||
|
||||
def next_tactic(self, state, goal_id):
|
||||
pass
|
||||
def guidance(self, state):
|
||||
pass
|
||||
```
|
||||
|
||||
|
|
@ -22,7 +22,26 @@ server = Server()
|
|||
|
||||
## Lean Dependencies
|
||||
|
||||
The server created from `Server()` is sufficient for basic theorem proving tasks
|
||||
reliant on Lean's `Init` library. Some users may find this insufficient and want
|
||||
to use non-builtin libraries such as Aesop or Mathlib4.
|
||||
|
||||
To use external Lean dependencies such as
|
||||
[Mathlib4](https://github.com/leanprover-community/mathlib4), Pantograph relies
|
||||
on an existing Lean repository. Instructions for creating this repository can be
|
||||
found [here](https://docs.lean-lang.org/lean4/doc/setup.html#lake).
|
||||
|
||||
After creating this initial Lean repository, execute in the repository
|
||||
```sh
|
||||
lake build
|
||||
```
|
||||
|
||||
to build all files from the repository. This step is necessary after any file in
|
||||
the repository is modified.
|
||||
|
||||
Then, feed the repository's path to the server
|
||||
```python
|
||||
server = Server(project_path="./path-to-lean-repo/")
|
||||
```
|
||||
|
||||
For a complete example, see `examples/`.
|
||||
|
|
|
|||
|
|
@ -239,14 +239,9 @@
|
|||
"source": [
|
||||
"import subprocess, os\n",
|
||||
"from pathlib import Path\n",
|
||||
"def get_project_and_lean_path():\n",
|
||||
" cwd = Path(os.getcwd()).resolve() / 'Example'\n",
|
||||
" p = subprocess.check_output(['lake', 'env', 'printenv', 'LEAN_PATH'], cwd=cwd)\n",
|
||||
" return cwd, p\n",
|
||||
"project_path, lean_path = get_project_and_lean_path()\n",
|
||||
"project_path = Path(os.getcwd()).resolve() / 'Example'\n",
|
||||
"print(f\"$PWD: {project_path}\")\n",
|
||||
"print(f\"$LEAN_PATH: {lean_path}\")\n",
|
||||
"server = Server(imports=['Example'], project_path=project_path, lean_path=lean_path)"
|
||||
"server = Server(imports=['Example'], project_path=project_path)"
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -445,7 +440,7 @@
|
|||
"name": "python",
|
||||
"nbconvert_exporter": "python",
|
||||
"pygments_lexer": "ipython3",
|
||||
"version": "3.12.4"
|
||||
"version": "3.12.6"
|
||||
}
|
||||
},
|
||||
"nbformat": 4,
|
||||
|
|
|
|||
|
|
@ -24,12 +24,28 @@ def _get_proc_cwd():
|
|||
def _get_proc_path():
|
||||
return _get_proc_cwd() / "pantograph-repl"
|
||||
|
||||
class TacticFailure(Exception):
|
||||
pass
|
||||
class ServerError(Exception):
|
||||
pass
|
||||
def get_lean_path(project_path):
|
||||
"""
|
||||
Extracts the `LEAN_PATH` variable from a project path.
|
||||
"""
|
||||
import subprocess
|
||||
p = subprocess.check_output(
|
||||
['lake', 'env', 'printenv', 'LEAN_PATH'],
|
||||
cwd=project_path,
|
||||
)
|
||||
return p
|
||||
|
||||
DEFAULT_CORE_OPTIONS=["maxHeartbeats=0", "maxRecDepth=100000"]
|
||||
class TacticFailure(Exception):
|
||||
"""
|
||||
Indicates a tactic failed to execute
|
||||
"""
|
||||
class ServerError(Exception):
|
||||
"""
|
||||
Indicates a logical error in the server.
|
||||
"""
|
||||
|
||||
|
||||
DEFAULT_CORE_OPTIONS = ["maxHeartbeats=0", "maxRecDepth=100000"]
|
||||
|
||||
|
||||
class Server:
|
||||
|
|
@ -54,6 +70,8 @@ class Server:
|
|||
self.timeout = timeout
|
||||
self.imports = imports
|
||||
self.project_path = project_path if project_path else _get_proc_cwd()
|
||||
if project_path and not lean_path:
|
||||
lean_path = get_lean_path(project_path)
|
||||
self.lean_path = lean_path
|
||||
self.maxread = maxread
|
||||
self.proc_path = _get_proc_path()
|
||||
|
|
@ -68,6 +86,9 @@ class Server:
|
|||
self.to_remove_goal_states = []
|
||||
|
||||
def is_automatic(self):
|
||||
"""
|
||||
Check if the server is running in automatic mode
|
||||
"""
|
||||
return self.options.get("automaticMode", True)
|
||||
|
||||
def restart(self):
|
||||
|
|
@ -185,6 +206,9 @@ class Server:
|
|||
return GoalState.parse(result, self.to_remove_goal_states)
|
||||
|
||||
def goal_conv_begin(self, state: GoalState, goal_id: int) -> GoalState:
|
||||
"""
|
||||
Start conversion tactic mode on one goal
|
||||
"""
|
||||
result = self.run('goal.tactic', {"stateId": state.state_id, "goalId": goal_id, "conv": True})
|
||||
if "error" in result:
|
||||
raise ServerError(result["desc"])
|
||||
|
|
@ -195,6 +219,9 @@ class Server:
|
|||
return GoalState.parse(result, self.to_remove_goal_states)
|
||||
|
||||
def goal_conv_end(self, state: GoalState) -> GoalState:
|
||||
"""
|
||||
Exit conversion tactic mode on all goals
|
||||
"""
|
||||
result = self.run('goal.tactic', {"stateId": state.state_id, "goalId": 0, "conv": False})
|
||||
if "error" in result:
|
||||
raise ServerError(result["desc"])
|
||||
|
|
@ -219,7 +246,7 @@ class Server:
|
|||
with open(file_name, 'rb') as f:
|
||||
content = f.read()
|
||||
units = [
|
||||
content[unit["bounary"][0]:unit["boundary"][1]].decode('utf-8')
|
||||
content[unit["boundary"][0]:unit["boundary"][1]].decode('utf-8')
|
||||
for unit in result['units']
|
||||
]
|
||||
invocations = [
|
||||
|
|
|
|||
Loading…
Reference in New Issue