421 lines
11 KiB
Plaintext
421 lines
11 KiB
Plaintext
{
|
||
"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.\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": 2,
|
||
"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": 3,
|
||
"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": 6,
|
||
"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": 6,
|
||
"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": 8,
|
||
"id": "bfbd5512-fcb0-428d-8131-4da4005e743c",
|
||
"metadata": {},
|
||
"outputs": [
|
||
{
|
||
"data": {
|
||
"text/plain": [
|
||
"GoalState(state_id=2, goals=[Goal(variables=[Variable(t='Prop', v=None, name='p✝')], target='p✝ → p✝', name=None, is_conversion=False)], _sentinel=[1])"
|
||
]
|
||
},
|
||
"execution_count": 8,
|
||
"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": 9,
|
||
"id": "2d18d6dc-7936-4bb6-b47d-f781dd8ddacd",
|
||
"metadata": {},
|
||
"outputs": [
|
||
{
|
||
"data": {
|
||
"text/plain": [
|
||
"'p✝ : Prop\\n⊢ p✝ → p✝'"
|
||
]
|
||
},
|
||
"execution_count": 9,
|
||
"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": 12,
|
||
"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": 15,
|
||
"id": "9d18045a-9734-415c-8f40-7aadb6cb18f4",
|
||
"metadata": {},
|
||
"outputs": [
|
||
{
|
||
"data": {
|
||
"text/plain": [
|
||
"GoalState(state_id=7, goals=[], _sentinel=[1, 3, 4, 5])"
|
||
]
|
||
},
|
||
"execution_count": 15,
|
||
"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": 16,
|
||
"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": 19,
|
||
"id": "ecf5d9d3-e53e-4f67-969e-d38e3d97c65e",
|
||
"metadata": {},
|
||
"outputs": [
|
||
{
|
||
"name": "stdout",
|
||
"output_type": "stream",
|
||
"text": [
|
||
"$PWD: /Users/aniva/Projects/atp/PyPantograph/examples/Example\n",
|
||
"$LEAN_PATH: b'././.lake/packages/std/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/build/lib:/Users/aniva/.elan/toolchains/leanprover--lean4---v4.8.0-rc1/lib/lean\\n'\n"
|
||
]
|
||
}
|
||
],
|
||
"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",
|
||
"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)"
|
||
]
|
||
},
|
||
{
|
||
"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": 20,
|
||
"id": "bf485778-baa9-4c1c-80fa-960f9cf9bc8a",
|
||
"metadata": {},
|
||
"outputs": [
|
||
{
|
||
"data": {
|
||
"text/plain": [
|
||
"True"
|
||
]
|
||
},
|
||
"execution_count": 20,
|
||
"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 project module via `Server.compile_unit`."
|
||
]
|
||
},
|
||
{
|
||
"cell_type": "code",
|
||
"execution_count": 21,
|
||
"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",
|
||
"==== #2 ====\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.compile_unit(\"Example\")\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": "cb5bbbcc-01dc-4a35-81ba-e155cedb9a91",
|
||
"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.4"
|
||
}
|
||
},
|
||
"nbformat": 4,
|
||
"nbformat_minor": 5
|
||
}
|