doc: Update `load_sorry` documentation
This commit is contained in:
parent
56fc11f831
commit
2aa5fb2a3d
GPG Key ID:
4D9B1C8D10EA4C50
|
|
@ -10,7 +10,7 @@
|
||||||
"Pantograph supports drafting (technically the sketch step) from\n",
|
"Pantograph supports drafting (technically the sketch step) from\n",
|
||||||
"[Draft-Sketch-Prove](https://github.com/wellecks/ntptutorial/tree/main/partII_dsp).\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",
|
"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",
|
"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",
|
"\n",
|
||||||
"At this point we must introduce the idea of compilation units. Each Lean\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",
|
"definition, theorem, constant, etc., is a *compilation unit*. When Pantograph\n",
|
||||||
|
|
@ -120,8 +120,8 @@
|
||||||
"\"\"\"\n",
|
"\"\"\"\n",
|
||||||
"\n",
|
"\n",
|
||||||
"server = Server()\n",
|
"server = Server()\n",
|
||||||
"state0, = server.load_sorry(sketch)\n",
|
"unit, = server.load_sorry(sketch)\n",
|
||||||
"print(state0)"
|
"print(unit.goal_state)"
|
||||||
]
|
]
|
||||||
},
|
},
|
||||||
{
|
{
|
||||||
|
|
@ -157,7 +157,7 @@
|
||||||
"name": "python",
|
"name": "python",
|
||||||
"nbconvert_exporter": "python",
|
"nbconvert_exporter": "python",
|
||||||
"pygments_lexer": "ipython3",
|
"pygments_lexer": "ipython3",
|
||||||
"version": "3.12.6"
|
"version": "3.12.7"
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
"nbformat": 4,
|
"nbformat": 4,
|
||||||
|
|
|
||||||
|
|
@ -1,448 +0,0 @@
|
||||||
{
|
|
||||||
"cells": [
|
|
||||||
{
|
|
||||||
"cell_type": "markdown",
|
|
||||||
"id": "a1078f98-fcaf-4cda-8ad4-3cbab44f114b",
|
|
||||||
"metadata": {},
|
|
||||||
"source": [
|
|
||||||
"# Pantograph Example\n",
|
|
||||||
"\n",
|
|
||||||
"The only interface for interacting with Pantograph is the `Server` class. It can be used either standalone (with no Lean project specified) or in a Lean project in order to access the project's symbols (e.g. Mathlib).\n",
|
|
||||||
"\n",
|
|
||||||
"The server's `imports` argument must be specified as a list of Lean modules to import. With no import statements, there are no symbols available and no useful work can be done. By default, `imports` is `[\"Init\"]`."
|
|
||||||
]
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"cell_type": "code",
|
|
||||||
"execution_count": 1,
|
|
||||||
"id": "101f4591-ec31-4000-96a6-ac3fc3dd0fa2",
|
|
||||||
"metadata": {},
|
|
||||||
"outputs": [],
|
|
||||||
"source": [
|
|
||||||
"from pantograph import Server\n",
|
|
||||||
"\n",
|
|
||||||
"server = Server()"
|
|
||||||
]
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"cell_type": "markdown",
|
|
||||||
"id": "1fbdb837-740e-44ef-a7e9-c40f79584639",
|
|
||||||
"metadata": {},
|
|
||||||
"source": [
|
|
||||||
"We can initialize a proof by providing the target statement."
|
|
||||||
]
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"cell_type": "code",
|
|
||||||
"execution_count": 2,
|
|
||||||
"id": "4affc375-360b-40cf-8d22-4fdcc12dba0d",
|
|
||||||
"metadata": {},
|
|
||||||
"outputs": [],
|
|
||||||
"source": [
|
|
||||||
"state0 = server.goal_start(\"forall (p : Prop), p -> p\")"
|
|
||||||
]
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"cell_type": "markdown",
|
|
||||||
"id": "deb7994a-273f-4b52-be2d-e1086d4c1d55",
|
|
||||||
"metadata": {},
|
|
||||||
"source": [
|
|
||||||
"This invocation creates a *goal state*, which consists of a finite number of goals. "
|
|
||||||
]
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"cell_type": "code",
|
|
||||||
"execution_count": 3,
|
|
||||||
"id": "29f7ae15-7f69-4740-a6fa-71fbb1ccabd8",
|
|
||||||
"metadata": {},
|
|
||||||
"outputs": [
|
|
||||||
{
|
|
||||||
"data": {
|
|
||||||
"text/plain": [
|
|
||||||
"GoalState(state_id=0, goals=[Goal(variables=[], target='forall (p : Prop), p -> p', name=None, is_conversion=False)], _sentinel=[])"
|
|
||||||
]
|
|
||||||
},
|
|
||||||
"execution_count": 3,
|
|
||||||
"metadata": {},
|
|
||||||
"output_type": "execute_result"
|
|
||||||
}
|
|
||||||
],
|
|
||||||
"source": [
|
|
||||||
"state0"
|
|
||||||
]
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"cell_type": "markdown",
|
|
||||||
"id": "274f50da-85c1-445e-bf9f-cb716f66e36f",
|
|
||||||
"metadata": {},
|
|
||||||
"source": [
|
|
||||||
"Execute tactics on the goal state via `Server.goal_tactic`:"
|
|
||||||
]
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"cell_type": "code",
|
|
||||||
"execution_count": 4,
|
|
||||||
"id": "bfbd5512-fcb0-428d-8131-4da4005e743c",
|
|
||||||
"metadata": {},
|
|
||||||
"outputs": [
|
|
||||||
{
|
|
||||||
"data": {
|
|
||||||
"text/plain": [
|
|
||||||
"GoalState(state_id=1, goals=[Goal(variables=[Variable(t='Prop', v=None, name='p✝')], target='p✝ → p✝', name=None, is_conversion=False)], _sentinel=[])"
|
|
||||||
]
|
|
||||||
},
|
|
||||||
"execution_count": 4,
|
|
||||||
"metadata": {},
|
|
||||||
"output_type": "execute_result"
|
|
||||||
}
|
|
||||||
],
|
|
||||||
"source": [
|
|
||||||
"state1 = server.goal_tactic(state0, goal_id=0, tactic=\"intro\")\n",
|
|
||||||
"state1"
|
|
||||||
]
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"cell_type": "markdown",
|
|
||||||
"id": "1c1c5ab4-5518-40b0-8a2f-50e095a3702a",
|
|
||||||
"metadata": {},
|
|
||||||
"source": [
|
|
||||||
"Recover the usual string form of a goal by the `str` function:"
|
|
||||||
]
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"cell_type": "code",
|
|
||||||
"execution_count": 5,
|
|
||||||
"id": "2d18d6dc-7936-4bb6-b47d-f781dd8ddacd",
|
|
||||||
"metadata": {},
|
|
||||||
"outputs": [
|
|
||||||
{
|
|
||||||
"data": {
|
|
||||||
"text/plain": [
|
|
||||||
"'p✝ : Prop\\n⊢ p✝ → p✝'"
|
|
||||||
]
|
|
||||||
},
|
|
||||||
"execution_count": 5,
|
|
||||||
"metadata": {},
|
|
||||||
"output_type": "execute_result"
|
|
||||||
}
|
|
||||||
],
|
|
||||||
"source": [
|
|
||||||
"str(state1.goals[0])"
|
|
||||||
]
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"cell_type": "markdown",
|
|
||||||
"id": "fc560b88-0222-4e40-bff9-37ab70af075e",
|
|
||||||
"metadata": {},
|
|
||||||
"source": [
|
|
||||||
"When a tactic fails, it throws an exception:"
|
|
||||||
]
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"cell_type": "code",
|
|
||||||
"execution_count": 6,
|
|
||||||
"id": "a0fdd3b3-9b38-4602-84a3-89065822f6e8",
|
|
||||||
"metadata": {},
|
|
||||||
"outputs": [
|
|
||||||
{
|
|
||||||
"name": "stdout",
|
|
||||||
"output_type": "stream",
|
|
||||||
"text": [
|
|
||||||
"[\"tactic 'assumption' failed\\np✝ : Prop\\n⊢ p✝ → p✝\"]\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": "c801bbb4-9248-4f75-945b-1dd665bb08d1",
|
|
||||||
"metadata": {},
|
|
||||||
"source": [
|
|
||||||
"A state with no goals is considered solved"
|
|
||||||
]
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"cell_type": "code",
|
|
||||||
"execution_count": 7,
|
|
||||||
"id": "9d18045a-9734-415c-8f40-7aadb6cb18f4",
|
|
||||||
"metadata": {},
|
|
||||||
"outputs": [
|
|
||||||
{
|
|
||||||
"data": {
|
|
||||||
"text/plain": [
|
|
||||||
"GoalState(state_id=3, goals=[], _sentinel=[])"
|
|
||||||
]
|
|
||||||
},
|
|
||||||
"execution_count": 7,
|
|
||||||
"metadata": {},
|
|
||||||
"output_type": "execute_result"
|
|
||||||
}
|
|
||||||
],
|
|
||||||
"source": [
|
|
||||||
"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": "aa5a2800-cae3-48df-b746-d19a8d84eaf5",
|
|
||||||
"metadata": {},
|
|
||||||
"source": [
|
|
||||||
"Execute `Server.gc()` to clean up unused goals once in a while"
|
|
||||||
]
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"cell_type": "code",
|
|
||||||
"execution_count": 8,
|
|
||||||
"id": "ee98de99-3cfc-4449-8d62-00e8eaee03db",
|
|
||||||
"metadata": {},
|
|
||||||
"outputs": [],
|
|
||||||
"source": [
|
|
||||||
"server.gc()"
|
|
||||||
]
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"cell_type": "markdown",
|
|
||||||
"id": "78cfb9ac-c5ec-4901-97a5-4d19e6b8ecbb",
|
|
||||||
"metadata": {},
|
|
||||||
"source": [
|
|
||||||
"## Loading Projects\n",
|
|
||||||
"\n",
|
|
||||||
"Pantograph would not be useful if it could not load symbols from other projects. In `examples/Example` is a standard Lean 4 project, with its toolchain version precisely equal to the toolchain version of Pantograph. Executing `lake new PROJECT_NAME` or `lake init` in an empty folder initializes a project according to this specification. To use a project in Pantograph, compile the project by running `lake build` in its root directory. This sets up output folders and builds the binary Lean files.\n",
|
|
||||||
"\n",
|
|
||||||
"Load the example project by providing `project_path` and `lean_path` to `Server`:"
|
|
||||||
]
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"cell_type": "code",
|
|
||||||
"execution_count": 9,
|
|
||||||
"id": "ecf5d9d3-e53e-4f67-969e-d38e3d97c65e",
|
|
||||||
"metadata": {},
|
|
||||||
"outputs": [
|
|
||||||
{
|
|
||||||
"name": "stdout",
|
|
||||||
"output_type": "stream",
|
|
||||||
"text": [
|
|
||||||
"$PWD: /home/aniva/Projects/atp/PyPantograph/examples/Example\n",
|
|
||||||
"$LEAN_PATH: b'././.lake/packages/batteries/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/build/lib:/home/aniva/.elan/toolchains/leanprover--lean4---v4.12/lib/lean\\n'\n"
|
|
||||||
]
|
|
||||||
}
|
|
||||||
],
|
|
||||||
"source": [
|
|
||||||
"import subprocess, os\n",
|
|
||||||
"from pathlib import Path\n",
|
|
||||||
"project_path = Path(os.getcwd()).resolve() / 'Example'\n",
|
|
||||||
"print(f\"$PWD: {project_path}\")\n",
|
|
||||||
"server = Server(imports=['Example'], project_path=project_path)"
|
|
||||||
]
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"cell_type": "markdown",
|
|
||||||
"id": "67123741-3d23-4077-98ab-91110b4e39f1",
|
|
||||||
"metadata": {},
|
|
||||||
"source": [
|
|
||||||
"With the project loaded, all dependencies of the project, be it Mathlib or Aesop, are now available."
|
|
||||||
]
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"cell_type": "code",
|
|
||||||
"execution_count": 10,
|
|
||||||
"id": "bf485778-baa9-4c1c-80fa-960f9cf9bc8a",
|
|
||||||
"metadata": {},
|
|
||||||
"outputs": [
|
|
||||||
{
|
|
||||||
"data": {
|
|
||||||
"text/plain": [
|
|
||||||
"True"
|
|
||||||
]
|
|
||||||
},
|
|
||||||
"execution_count": 10,
|
|
||||||
"metadata": {},
|
|
||||||
"output_type": "execute_result"
|
|
||||||
}
|
|
||||||
],
|
|
||||||
"source": [
|
|
||||||
"state0 = server.goal_start(\"forall (p q: Prop), Or p q -> Or q p\")\n",
|
|
||||||
"state1 = server.goal_tactic(state0, goal_id=0, tactic=\"aesop\")\n",
|
|
||||||
"state1.is_solved"
|
|
||||||
]
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"cell_type": "markdown",
|
|
||||||
"id": "8c3f9d90-bacc-4cba-95a4-23cc31a58a4f",
|
|
||||||
"metadata": {},
|
|
||||||
"source": [
|
|
||||||
"## Reading Symbols\n",
|
|
||||||
"\n",
|
|
||||||
"Pantograph can also query proof states from a project by directly calling into Lean's compiler internals. Run the Lean compiler on a Lean file via `Server.tactic_invocations`. Feeding in the absolute path is preferred."
|
|
||||||
]
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"cell_type": "code",
|
|
||||||
"execution_count": 11,
|
|
||||||
"id": "8ff6007b-50df-4449-9a86-6d3eb0bc0caa",
|
|
||||||
"metadata": {},
|
|
||||||
"outputs": [
|
|
||||||
{
|
|
||||||
"name": "stdout",
|
|
||||||
"output_type": "stream",
|
|
||||||
"text": [
|
|
||||||
"==== #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": [
|
|
||||||
"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": "markdown",
|
|
||||||
"id": "8762b719-d13b-4714-84ff-48c44b18f364",
|
|
||||||
"metadata": {},
|
|
||||||
"source": [
|
|
||||||
"### Loading a theorem for the agent to prove\n",
|
|
||||||
"\n",
|
|
||||||
"For this to work, write `sorry` in the place where you would like your agent to do work, for example\n",
|
|
||||||
"```lean\n",
|
|
||||||
"example : (p q: Prop): Or p q -> Or q p := sorry\n",
|
|
||||||
"```\n",
|
|
||||||
"Then use the `Server.load_sorry`. As long as you only have one statement in `command`, it will give you exactly one goal state. A command with no `sorry`s results in no goal states.\n",
|
|
||||||
"\n",
|
|
||||||
"Note: Since a syntactically incorrect command will not generate `sorry`s, they will be sliently ignored by the frontend. Check if this is the case if the function returns no goals."
|
|
||||||
]
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"cell_type": "code",
|
|
||||||
"execution_count": 12,
|
|
||||||
"id": "3c515d2b-6910-499e-953b-bc69dc0e0a57",
|
|
||||||
"metadata": {},
|
|
||||||
"outputs": [
|
|
||||||
{
|
|
||||||
"name": "stdout",
|
|
||||||
"output_type": "stream",
|
|
||||||
"text": [
|
|
||||||
"GoalState(state_id=2, goals=[Goal(variables=[Variable(t='Prop', v=None, name='p'), Variable(t='Prop', v=None, name='q')], target='p ∨ q → q ∨ p', name=None, is_conversion=False)], _sentinel=[0])\n"
|
|
||||||
]
|
|
||||||
}
|
|
||||||
],
|
|
||||||
"source": [
|
|
||||||
"state0, = server.load_sorry(\"example (p q: Prop): Or p q -> Or q p := sorry\")\n",
|
|
||||||
"print(state0)"
|
|
||||||
]
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"cell_type": "code",
|
|
||||||
"execution_count": null,
|
|
||||||
"id": "50b90547-fcbf-419f-866e-a6ebcc925c5f",
|
|
||||||
"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
|
|
||||||
}
|
|
||||||
Loading…
Reference in New Issue