PyPantograph

https://github.com/stanford-centaur/pypantograph
Admin
PyPantograph is a machine-to-machine interaction system for Lean 4 designed to train and evaluate...
Tokens:12,789
Snippets:139
Trust Score:7.6
License:Apache-2.0
Update:5 months ago
Show doc for...
Tokens:
Raw
### Build Example Project

Source: https://github.com/stanford-centaur/pypantograph/blob/main/examples/README.md

Builds the example project to generate compiled .olean files. Ensure you are in the 'Example' directory before running.

```sh
pushd Example
lake build
popd
```

--------------------------------

### Install Dependencies with uv

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/setup.md

After cloning, navigate to the repository and use 'uv sync' to install project dependencies.

```sh
cd <repo-path>
uv sync
```

--------------------------------

### Run Sketch Loading Example

Source: https://github.com/stanford-centaur/pypantograph/blob/main/examples/README.md

Executes the Python script 'sketch.py' from the project root to demonstrate loading a sketch.

```sh
poetry run examples/sketch.py
```

--------------------------------

### Starting a Goal and Applying Tactics

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

Initiate a Lean goal state using `goal_start_async` and then apply tactics sequentially using `goal_tactic_async`.

```python
state = await server.goal_start_async("forall (p : Prop), p -> And p (Or p p)")
state = await server.goal_tactic_async(state, "intro p h")
state = await server.goal_tactic_async(state, "apply And.intro")
print(state)
```

--------------------------------

### Install Pantograph Wheel

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/setup.md

Example of how to specify a Pantograph wheel file in a pyproject.toml file.

```toml
pantograph = { file = "path/to/wheel/dist/pantograph-0.3.0-cp312-cp312-manylinux_2_40_x86_64.whl" }
```

--------------------------------

### Starting a Proof Goal

Source: https://context7.com/stanford-centaur/pypantograph/llms.txt

Initiate a new proof goal using `goal_start` with a target expression. This sets up the context for applying tactics.

```APIDOC
## Starting a Proof Goal

The `goal_start` method creates a new goal state from a target expression. This initializes a proof context where tactics can be applied to prove the given proposition.

### Request Example
```python
from pantograph import Server

server = Server(imports=['Init'])

# Start a proof for a simple proposition
state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
print(f"State ID: {state0.state_id}")  # Output: State ID: 0
print(f"Number of goals: {len(state0.goals)}")  # Output: Number of goals: 1
print(state0)
# Output:
# ⊢ ∀ (p q : Prop), p ∨ q → q ∨ p

# Start a proof for a natural number property
state = server.goal_start("forall (n m: Nat), n + m = m + n")
print(state.goals[0].target)  # Output: ∀ (n m : Nat), n + m = m + n
```
```

--------------------------------

### Run Aesop Tactic Example

Source: https://github.com/stanford-centaur/pypantograph/blob/main/examples/README.md

Executes the Python script 'aesop.py' from the project root to demonstrate the usage of the 'aesop' tactic.

```sh
poetry run examples/aesop.py
```

--------------------------------

### Start a New Proof Goal

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

Initiates a new proof by calling `Server.goal_start` with a logical expression. This creates the initial goal state.

```python
server = await Server.create()
state0 = await server.goal_start_async("forall (p q: Prop), Or p q -> Or q p")
```

--------------------------------

### Start a Proof Goal

Source: https://context7.com/stanford-centaur/pypantograph/llms.txt

Use the `goal_start` method to create a new goal state from a target expression, initializing a proof context for tactic application.

```python
from pantograph import Server

server = Server(imports=['Init'])

# Start a proof for a simple proposition
state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
print(f"State ID: {state0.state_id}")  # Output: State ID: 0
print(f"Number of goals: {len(state0.goals)}")  # Output: Number of goals: 1
print(state0)
# Output:
# ⊢ ∀ (p q : Prop), p ∨ q → q ∨ p
```

```python
from pantograph import Server

server = Server(imports=['Init'])

# Start a proof for a natural number property
state = server.goal_start("forall (n m: Nat), n + m = m + n")
print(state.goals[0].target)  # Output: ∀ (n m : Nat), n + m = m + n
```

--------------------------------

### Build PyPantograph Documentation

Source: https://github.com/stanford-centaur/pypantograph/blob/main/README.md

Builds the project documentation using jupyter-book. This command requires uv and jupyter-book to be installed.

```sh
uv run --group dev jupyter-book build doc
```

--------------------------------

### Execute Pantograph Search

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/agent-search.ipynb

Initializes the Pantograph server and a custom agent, then starts the proof search for a given goal state. Set `verbose=True` for detailed search logs.

```python
server = Server()
agent = DumbAgent()
goal_state = server.goal_start("∀ (p q: Prop), Or p q -> Or q p")
agent.search(server=server, goal_state=goal_state, verbose=False)
```

--------------------------------

### Search Result Example

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/agent-search.ipynb

An example of the output from the `agent.search` method, indicating search performance and success.

```text
Result:
SearchResult(n_goals_root=1, duration=0.7717759609222412, success=True, steps=16)
```

--------------------------------

### Add PyPantograph as a Project Dependency

Source: https://github.com/stanford-centaur/pypantograph/blob/main/README.md

Installs PyPantograph as a dependency for your project using uv. Ensure uv is installed and configured.

```sh
uv add git+https://github.com/stanford-centaur/PyPantograph
uv sync
```

--------------------------------

### Custom Proof Search Agent Implementation

Source: https://context7.com/stanford-centaur/pypantograph/llms.txt

Shows how to implement a custom proof search agent by extending the Agent class. This example defines a simple agent with a fixed sequence of tactics.

```python
from pantograph import Server
from pantograph.search import Agent, SearchResult, SearchState, DumbAgent
from pantograph.expr import GoalState, Tactic, Site
from typing import Optional

# Implement a custom proof search agent
class MyAgent(Agent):
    def __init__(self):
        self.tactics = ["intro", "assumption", "rfl", "simp"]
        self.tactic_idx = {}

    def next_tactic(self, state: GoalState, goal_id: int) -> Optional[Tactic]:
        key = (state.state_id, goal_id)
        idx = self.tactic_idx.get(key, 0)
        if idx >= len(self.tactics):
            return None
        self.tactic_idx[key] = idx + 1
        return self.tactics[idx]

    def guidance(self, state: GoalState) -> list[float]:
        return [0.0 for _ in state.goals]

    def reset(self):
        self.tactic_idx.clear()

# Run proof search
server = Server(imports=['Init'])
state0 = server.goal_start("forall (p: Prop), p -> p")

agent = DumbAgent()
result = agent.search(
    server=server,
    goal_state=state0,
    max_steps=100,
    max_trials_per_goal=5,
    verbose=True
)

print(f"Success: {result.success}")
print(f"Steps: {result.steps}")
print(f"Duration: {result.duration:.2f}s")
# Output:
# Success: True
# Steps: 2
# Duration: 0.05s
```

--------------------------------

### Asynchronous Server Initialization and Goal Loading in Jupyter

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/setup.md

Use the asynchronous version of Server.create() and load_sorry_async for running Pantograph in Jupyter environments. This example demonstrates loading a 'sorry' proof and printing its goal state.

```python
server = await Server.create()
unit, = await server.load_sorry_async(sketch)
print(unit.goal_state)
```

--------------------------------

### Using Tactic Modes in Pantograph

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

Demonstrates starting a goal and then applying tactics, including switching to TacticMode.CALC for incremental feedback. Ensure TacticMode is imported.

```python
state = await server.goal_start_async("∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b")

state = await server.goal_tactic_async(state, "intro a b h")
state = await server.goal_tactic_async(state, TacticMode.CALC)
state = await server.goal_tactic_async(state, "1 + a + 1 = a + 1 + 1")
state
```

--------------------------------

### Execute PyPantograph Unit Tests

Source: https://github.com/stanford-centaur/pypantograph/blob/main/README.md

Runs the unit tests for PyPantograph using pytest. This command requires uv and pytest to be installed.

```sh
uv run pytest
```

--------------------------------

### Implement a Brute-Force Search Agent

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/agent-search.ipynb

A basic agent that iterates through predefined tactics for goals based on their structure. Use this as a starting point for custom search strategies.

```python
class DumbAgent(Agent):

    def __init__(self):
        super().__init__()

        self.goal_tactic_id_map = collections.defaultdict(lambda : 0)
        self.intros = [
            "intro",
        ]
        self.tactics = [
            "intro h",
            "cases h",
            "apply Or.inl",
            "apply Or.inr",
        ]
        self.no_space_tactics = [
            "assumption",
        ]

    def next_tactic(
            self,
            state: GoalState,
            goal_id: int,
    ) -> Optional[Tactic]:
        key = (state.state_id, goal_id)
        i = self.goal_tactic_id_map[key]

        target = state.goals[goal_id].target
        if target.startswith('∀'):
            tactics = self.intros
        elif ' ' in target:
            tactics = self.tactics
        else:
            tactics = self.no_space_tactics

        if i >= len(tactics):
            return None

        self.goal_tactic_id_map[key] = i + 1
        return tactics[i]
```

--------------------------------

### Applying Tactic Draft in Python

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

Use `TacticDraft` to apply a sequence of tactics to a Lean goal state obtained from a sketch. This example demonstrates applying tactics to solve base and inductive cases.

```python
step = """
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 =>
     sorry
"""
from pantograph.expr import TacticDraft
tactic = TacticDraft(step)
state1 = await server.goal_tactic_async(unit.goal_state, tactic)
print(state1)
```

--------------------------------

### Loading Sorry from Sketch in Python

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

Load a Lean sketch containing 'sorry' using Pantograph's `load_sorry_async` function in Python. This method is not compatible with 'example' declarations.

```python
sketch = """
theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := sorry
"""
unit, = await server.load_sorry_async(sketch)
print(unit.goal_state)
```

--------------------------------

### Initialize Pantograph Server

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/setup.md

Create an instance of the Pantograph Server for basic theorem proving tasks.

```python
from pantograph import Server
server = Server()
```

--------------------------------

### Initialize Server with Lean Project Path

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/setup.md

Provide the path to your Lean repository when initializing the server to use external Lean dependencies.

```python
server = Server(project_path="./path-to-lean-repo/")
```

--------------------------------

### Loading Tactics from External Projects

Source: https://context7.com/stanford-centaur/pypantograph/llms.txt

Shows how to configure PyPantograph to use tactics from external Lean projects, such as Mathlib. The server automatically discovers the Lean path.

```python
from pathlib import Path
from pantograph import Server

# Point to a Lean project with dependencies
project_path = Path('./examples/Example').resolve()

# Server automatically discovers LEAN_PATH
server = Server(
    imports=['Example'],
    project_path=str(project_path),
    timeout=120
)

# Use tactics from the imported project (e.g., Aesop)
state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
state1 = server.goal_tactic(state0, tactic="aesop")
print(f"Solved by aesop: {state1.is_solved}")  # True
```

```python
# Load header with specific imports
server2 = Server(imports=[])
server2.load_header("import Init\nopen Nat")

state0 = server2.goal_start("forall (n : Nat), n + 1 = n.succ")
state1 = server2.goal_tactic(state0, "intro")
state2 = server2.goal_tactic(state1, "apply add_one")
print(f"Proof complete: {state2.is_solved}")  # True
```

--------------------------------

### Initialize PyPantograph Server

Source: https://context7.com/stanford-centaur/pypantograph/llms.txt

Initialize the Server class with default or custom imports, project paths, and configuration options. The server manages a Lean 4 REPL subprocess.

```python
from pantograph import Server

# Basic server with default Init import
server = Server(imports=['Init'])
```

```python
from pantograph import Server
from pathlib import Path
project_path = Path('./my_lean_project').resolve()
server = Server(
    imports=['MyProject'],
    project_path=str(project_path),
    timeout=120,
    options={"automaticMode": True}
)
```

```python
import asyncio

async def create_async_server():
    server = await Server.create(
        imports=['Init'],
        project_path=None,
        timeout=60
    )
    return server
```

```python
from pantograph import Server

# Context manager usage
with Server(imports=['Init']) as server:
    t = server.expr_type("forall (n: Nat), n + 0 = n")
    print(t)  # Output: Prop
```

--------------------------------

### Build PyPantograph Wheels

Source: https://github.com/stanford-centaur/pypantograph/blob/main/README.md

Builds wheel packages for PyPantograph from the source code after cloning the repository. Navigate to the repository directory before executing.

```sh
cd <repo-path>
uv build
```

--------------------------------

### Serve PyPantograph Documentation

Source: https://github.com/stanford-centaur/pypantograph/blob/main/README.md

Serves the built PyPantograph documentation locally using Python's http.server. The documentation files are located in doc/_build/html.

```sh
python3 -m http.server -d doc/_build/html
```

--------------------------------

### Save and Load Goal State

Source: https://context7.com/stanford-centaur/pypantograph/llms.txt

Demonstrates how to save a Lean goal state to a file and then load it back. Ensure the temporary directory is handled correctly.

```python
import tempfile

# Create a goal state
state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")

# Save the goal state
with tempfile.TemporaryDirectory() as td:
    path = f"{td}/goal-state.pickle"
    server.goal_save(state0, path)

    # Load the goal state
    state0b = server.goal_load(path)
    print(state0b.goals[0].target)
    # Output: ∀ (p q : Prop), p ∨ q → q ∨ p
```

--------------------------------

### Server Initialization

Source: https://context7.com/stanford-centaur/pypantograph/llms.txt

Initialize the Pantograph Server to interact with a Lean 4 REPL subprocess. Supports custom imports, project paths, and asynchronous creation.

```APIDOC
## Server Initialization

The `Server` class is the main interface for interacting with Pantograph. It manages a Lean 4 REPL subprocess and provides both synchronous and asynchronous methods for proof manipulation. The server can be initialized with custom imports, project paths, and configuration options.

### Request Example
```python
from pantograph import Server

# Basic server with default Init import
server = Server(imports=['Init'])

# Server with custom project dependencies
from pathlib import Path
project_path = Path('./my_lean_project').resolve()
server = Server(
    imports=['MyProject'],
    project_path=str(project_path),
    timeout=120,
    options={"automaticMode": True}
)

# Async server creation
import asyncio

async def create_async_server():
    server = await Server.create(
        imports=['Init'],
        project_path=None,
        timeout=60
    )
    return server

# Context manager usage
with Server(imports=['Init']) as server:
    t = server.expr_type("forall (n: Nat), n + 0 = n")
    print(t)  # Output: Prop
```
```

--------------------------------

### Import Pantograph Server and Expression Utilities

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

Import necessary classes from the pantograph library to interact with the server and define tactics.

```python
from pantograph import Server
from pantograph.expr import Site, TacticHave, TacticExpr, TacticMode
```

--------------------------------

### Python Output for Goal and Tactic Application

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

The output shows the intermediate goal states after applying 'intro' and 'apply And.intro' tactics.

```text
left
p : Prop
h : p
⊢ p
right
p : Prop
h : p
⊢ p ∨ p
```

--------------------------------

### Execute Tactics with Intermediate Steps

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

Demonstrates executing tactics that involve intermediate steps like `have` and `cases`. The `?_` placeholder indicates a goal to be solved later.

```python
state2 = await server.goal_tactic_async(state0, "intro p q h\nhave random : 1 + 1 = 2 := ?_\ncases h")
print(state2)
```

--------------------------------

### Build Lean Repository with Lake

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/setup.md

Execute 'lake build' within your Lean repository to build all files. This is necessary after any file modifications.

```sh
lake build
```

--------------------------------

### Python Output for Site-Specific Tactic Application

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

The output shows the goal states after applying tactics with specific `goal_id`s, demonstrating the effect of `auto_resume`.

```text
right.h
p : Prop
h : p
⊢ p
left
p : Prop
h : p
⊢ p
```

--------------------------------

### Extract Tactic Invocations from Lean File

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/frontend.ipynb

Initializes the Pantograph server and extracts tactic invocation data from a specified Lean file. Requires the project path and the Lean file name.

```python
project_path = Path(os.getcwd()).parent.resolve() / 'examples/Example'
print(f"$PWD: {project_path}")
server = await Server.create(imports=['Example'], project_path=project_path)
units = await server.tactic_invocations_async(project_path / "Example.lean")
```

--------------------------------

### Using TacticDraft for Proof Sketches

Source: https://context7.com/stanford-centaur/pypantograph/llms.txt

Use TacticDraft to apply proof sketches to Lean goals. This is useful for generating initial proof structures or exploring proof steps.

```python
sketch = """by
  have h1 : Or p p := sorry
  sorry"""
state1b = server.goal_tactic(state0, tactic=TacticDraft(sketch))
print(f"Goals from sketch: {len(state1b.goals)}")
```

```lean
theorem add_comm_sketch : forall n m : Nat, n + m = m + n := sorry

```

```lean
sketch = """
by
  intros n m
  induction n with
  | zero =>
    sorry
  | succ n ih =>
    have h_inductive: n + m = m + n := sorry
    sorry
"""

```

```python
server2 = Server(imports=['Init'])
unit, = server2.load_sorry(root)
print(unit.goal_state)
state1 = server2.goal_tactic(unit.goal_state, tactic=TacticDraft(sketch))
print(f"Remaining sorries: {len(state1.goals)}")
```

--------------------------------

### Check File Conformance (Successful)

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/frontend.ipynb

Compares two Lean code snippets (`src` and `dst`) to check if the destination conforms to the source. A successful check results in an empty `CheckTrackResult` with no failures.

```python
src = """
def f : Nat -> Nat := sorry
theorem property (n : Nat) : f n = n + 1 := sorry
"""
dst = """
def f (x : Nat) := x + 1
theorem property (n : Nat) : f n = n + 1 := rfl
"""
await server.check_track_async(src, dst)
```

--------------------------------

### Load and Prove Theorems with Sorry

Source: https://context7.com/stanford-centaur/pypantograph/llms.txt

Use `load_sorry` to parse Lean code with `sorry` placeholders and extract goal states for training data extraction and proof sketching. Then, use `goal_tactic` to complete the proof.

```python
from pantograph import Server
from pantograph.expr import TacticDraft

server = Server(imports=['Init'])

# Load a theorem with sorry
units = server.load_sorry("theorem mystery (p: Prop) : p -> p := sorry")
unit = units[0]
state0 = unit.goal_state
print(state0)
# Output:
# p : Prop
# ⊢ p → p
```

```python
from pantograph import Server
from pantograph.expr import TacticDraft

server = Server(imports=['Init'])

# Load a theorem with sorry
units = server.load_sorry("theorem mystery (p: Prop) : p -> p := sorry")
unit = units[0]
state0 = unit.goal_state

# Complete the proof
state1 = server.goal_tactic(state0, tactic="intro h")
state2 = server.goal_tactic(state1, tactic="exact h")
print(f"Proof complete: {state2.is_solved}")  # Output: Proof complete: True
```

--------------------------------

### Using Conv and Calc Modes

Source: https://context7.com/stanford-centaur/pypantograph/llms.txt

Demonstrates PyPantograph's support for Lean's conversion (conv) and calculation (calc) proof modes. Manual control is enabled by disabling automatic mode.

```python
from pantograph import Server
from pantograph.expr import TacticMode, Site

# Disable automatic mode for manual control
server = Server(options={"automaticMode": False})

state0 = server.goal_start("forall (a b: Nat), (b = 2) -> 1 + a + 1 = a + b")
state1 = server.goal_tactic(state0, "intro a b h")

# Enter calc mode
state1b = server.goal_tactic(state1, TacticMode.CALC)

# Provide calc step
state2 = server.goal_tactic(state1b, "1 + a + 1 = a + 1 + 1")
print(f"Calc goals: {len(state2.goals)}")  # 2 goals

# Enter conv mode on first goal
state_c1 = server.goal_tactic(state2, TacticMode.CONV)
state_c2 = server.goal_tactic(state_c1, "rhs")
state_c3 = server.goal_tactic(state_c2, "rw [Nat.add.comm]")

# Exit conv mode back to tactic mode
state_c4 = server.goal_tactic(state_c3, TacticMode.TACTIC)
state_c5 = server.goal_tactic(state_c4, "rfl")
print(f"Conv goal solved: {state_c5.is_solved}")  # True

# Continue with remaining calc goal
state3 = server.goal_tactic(state2, "_ = a + 2", site=Site(1))
state4 = server.goal_tactic(state3, "rw [Nat.add.assoc]")
print(f"All goals solved: {state4.is_solved}")  # True
```

--------------------------------

### Load Definitions into Server Environment

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/frontend.ipynb

Adds a new Lean definition to the server's global environment using `server.load_definitions_async`. This allows subsequent operations to recognize the new definition.

```python
code = """
def mystery : Nat -> Nat := fun x => x + 1
"""
await server.load_definitions_async(code)
await server.env_inspect_async("mystery")
```

--------------------------------

### Clone Repository with Submodules

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/setup.md

Use this command to clone the repository and its submodules.

```sh
git clone --recurse-submodules <repo-path>
```

--------------------------------

### Goal State Persistence

Source: https://context7.com/stanford-centaur/pypantograph/llms.txt

Save and load Lean goal states to disk using PyPantograph's persistence features. This enables checkpointing during proof searches and sharing proof states.

```python
from pantograph import Server
import tempfile

server = Server(imports=['Init'])
```

--------------------------------

### Python Output for Loading Sorry

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

The output shows the goal state derived from a Lean sketch loaded via `load_sorry_async`.

```text
⊢ ∀ (n m : Nat), n + m = m + n
```

--------------------------------

### Execute Multiple Tactics Sequentially

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

Runs a sequence of tactics in a single call to `Server.goal_tactic_async`. Use `?_` to mark goals for later solving.

```python
state2 = await server.goal_tactic_async(state0, "intro p q\nintro h\ncases h")
print(state2)
```

--------------------------------

### Execute Lean Tactics

Source: https://context7.com/stanford-centaur/pypantograph/llms.txt

Apply tactics to a goal state using `goal_tactic`. Tactics can be simple strings or specialized objects like `TacticHave`, `TacticLet`, `TacticExpr`, and `TacticDraft`. Use `Site` to target specific goals.

```python
from pantograph import Server
from pantograph.expr import TacticHave, TacticLet, TacticDraft, Site

server = Server(imports=['Init'])

# Simple tactic execution
state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
state1 = server.goal_tactic(state0, tactic="intro a b h")
print(state1)
# Output:
# a : Prop
# b : Prop
# h : a ∨ b
# ⊢ b ∨ a
```

```python
from pantograph import Server
from pantograph.expr import TacticHave, TacticLet, TacticDraft, Site

server = Server(imports=['Init'])

# Simple tactic execution
state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
state1 = server.goal_tactic(state0, tactic="intro a b h")

state2 = server.goal_tactic(state1, tactic="cases h")
print(f"Goals after cases: {len(state2.goals)}")  # Output: 2
```

```python
from pantograph import Server
from pantograph.expr import TacticHave, TacticLet, TacticDraft, Site

server = Server(imports=['Init'])

# Simple tactic execution
state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
state1 = server.goal_tactic(state0, tactic="intro a b h")
state2 = server.goal_tactic(state1, tactic="cases h")

# Apply tactic to specific goal using Site
state3 = server.goal_tactic(state2, tactic="apply Or.inl", site=Site(goal_id=1))
state4 = server.goal_tactic(state3, tactic="assumption")
print(f"Remaining goals: {len(state4.goals)}")  # Output: 1
```

```python
from pantograph import Server
from pantograph.expr import TacticHave, TacticLet, TacticDraft, Site

server2 = Server(imports=['Init'])
state0 = server2.goal_start("1 + 1 = 2")
state1 = server2.goal_tactic(state0, tactic=TacticHave(branch="2 = 1 + 1", binder_name="h"))
print(f"Goals: {len(state1.goals)}")  # Output: 2
print(state1.goals[0].target)  # Output: 2 = 1 + 1
print(state1.goals[1].target)  # Output: 1 + 1 = 2
```

```python
from pantograph import Server
from pantograph.expr import TacticHave, TacticLet, TacticDraft, Site

server2 = Server(imports=['Init'])
state0 = server2.goal_start("1 + 1 = 2")
state1 = server2.goal_tactic(state0, tactic=TacticLet(branch="2 = 1 + 1", binder_name="h"))
# Creates goals with let-bound variable
```

--------------------------------

### Complete a Proof

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

Shows a sequence of tactics that lead to a solved state (no goals remaining). A state with no goals is considered complete.

```python
state0 = await server.goal_start_async("forall (p : Prop), p -> p")
state1 = await server.goal_tactic_async(state0, "intro")
state2 = await server.goal_tactic_async(state1, "intro h")
state3 = await server.goal_tactic_async(state2, "exact h")
state3
```

--------------------------------

### Companion Generation with Load Sorry

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

Generate coupled search targets by loading a sketch with a definition and a property using `load_sorry_async` with `ignore_values=True`. This is suitable for flat dependency structures.

```python
sketch = """
def f : Nat -> Nat := sorry
theorem property (n : Nat) : f n = n + 1 := sorry
"""
target, = await server.load_sorry_async(sketch, ignore_values=True)
print(target.goal_state)
```

--------------------------------

### Inspect Tactic Invocations in Second Compilation Unit

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/frontend.ipynb

Iterates through the tactic invocations of the second compilation unit, printing the 'before' state, the tactic executed (including used constants), and the 'after' state. This demonstrates detailed step-by-step execution analysis.

```python
for i in units[1].invocations:
    print(f"[Before]\n{i.before}")
    print(f"[Tactic]\n{i.tactic} (using {i.used_constants})")
    print(f"[After]\n{i.after}")
```

--------------------------------

### Applying Tactic with Auto-Resume Disabled

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

Apply a tactic to a specific goal using `goal_tactic_async` with `auto_resume=False` in the `Site` argument. This will dormant other goals.

```python
state1 = await server.goal_tactic_async(state, "exact h", site=Site(goal_id=0, auto_resume=False))
print(state1)
```

--------------------------------

### Import Pantograph Server Components

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/frontend.ipynb

Imports necessary components from the pantograph.server library for server-side operations.

```python
import os
from pathlib import Path
from pantograph.server import Server
```

--------------------------------

### Loading and Proving Theorems with Sorry

Source: https://context7.com/stanford-centaur/pypantograph/llms.txt

Use `load_sorry` to parse Lean code with `sorry` placeholders and extract goal states for proof sketching and data extraction.

```APIDOC
## Loading and Proving Theorems with Sorry

The `load_sorry` method parses Lean code containing `sorry` placeholders and extracts goal states for each sorry. This is essential for training data extraction and proof sketching workflows.

### Request Example
```python
from pantograph import Server
from pantograph.expr import TacticDraft

server = Server(imports=['Init'])

# Load a theorem with sorry
units = server.load_sorry("theorem mystery (p: Prop) : p -> p := sorry")
unit = units[0]
state0 = unit.goal_state
print(state0)
# Output:
# p : Prop
# ⊢ p → p

# Complete the proof
state1 = server.goal_tactic(state0, tactic="intro h")
state2 = server.goal_tactic(state1, tactic="exact h")
print(f"Proof complete: {state2.is_solved}")  # Output: Proof complete: True
```
```

--------------------------------

### Apply a Tactic to a Goal State

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

Executes a specified tactic on a given goal state using `Server.goal_tactic`. Most Lean tactics can be provided as strings.

```python
state1 = await server.goal_tactic_async(state0, "intro a")
print(state1)
```

--------------------------------

### Python Output for Tactic Draft Application

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

The output displays the evolving goal states after applying tactics defined in a `TacticDraft`.

```text
n : Nat
m : Nat
⊢ 0 + m = m
n : Nat
m : Nat
h_base : 0 + m = m
⊢ m + 0 = m
n : Nat
m : Nat
h_base : 0 + m = m
h_symm : m + 0 = m
⊢ 0 + m = m + 0
n✝ : Nat
m : Nat
n : Nat
ih : n + m = m + n
⊢ n + 1 + m = m + (n + 1)
```

--------------------------------

### Import Pantograph Search Components

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/agent-search.ipynb

Imports necessary modules for implementing a custom search agent in Pantograph.

```python
from typing import Optional
import collections
from pantograph import Server
from pantograph.search import Agent
from pantograph.expr import GoalState, Tactic
```

--------------------------------

### Display Current Goal State

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

Prints the current goal state to the console. This is useful for inspecting the proof progress.

```python
print(state0)
```

--------------------------------

### Inspect Tactic Invocations in First Compilation Unit

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/frontend.ipynb

Iterates through the tactic invocations of the first compilation unit, printing the 'before' state, the tactic executed (including used constants), and the 'after' state.

```python
for i in units[0].invocations:
    print(f"[Before]\n{i.before}")
    print(f"[Tactic]\n{i.tactic} (using {i.used_constants})")
    print(f"[After]\n{i.after}")
```

--------------------------------

### Drafting with Sorry in Lean

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

Use this Lean code to draft a proof by replacing expressions with 'sorry', which then become goals to be solved.

```lean
by
   intros n m
   induction n with
   | zero =>
     have h_base: 0 + m = m := sorry
     have h_symm: m + 0 = m := sorry
     sorry
   | succ n ih =>
     have h_inductive: n + m = m + n := sorry
     have h_pull_succ_out_from_right: m + Nat.succ n = Nat.succ (m + n) := sorry
     have h_flip_n_plus_m: Nat.succ (n + m) = Nat.succ (m + n) := sorry
     have h_pull_succ_out_from_left: Nat.succ n + m = Nat.succ (n + m) := sorry
     sorry
```

--------------------------------

### Check Compilation of Lean Code

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/frontend.ipynb

Uses `server.check_compile_async` to verify if a given string of Lean code compiles successfully. An empty list of messages indicates successful compilation.

```python
server = await Server.create()
code = """
example : 1 + 1 = 2 := by rfl
"""
await server.check_compile_async(code)
```

--------------------------------

### Applying Tactic to a Specific Goal

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

Apply a tactic to a specific goal by providing its `goal_id` in the `Site` argument to `goal_tactic_async`. Other goals remain active.

```python
state2 = await server.goal_tactic_async(state, "apply Or.inl", site=Site(goal_id=1))
print(state2)
```

--------------------------------

### Compiling and Verifying Lean Code

Source: https://context7.com/stanford-centaur/pypantograph/llms.txt

Verify the compilation of Lean code and retrieve compilation units with potential error messages using `check_compile`. This method is essential for validating code correctness.

```python
units = server.check_compile("example (p: Prop) : p -> p := id")
unit = units[0]
print(f"Messages: {unit.messages}")
```

```python
units = server.check_compile("example (p: Prop) : p -> p := 1")
unit = units[0]
print(unit.messages[0].data)
```

```python
units = server.check_compile(
    "import Lean\nexample (p: Prop) : p -> p := id",
    read_header=True
)
print(f"Compilation successful: {len(units[0].messages) == 0}")
```

```python
src = "def f : Nat -> Nat := sorry"
dst = "def f : Nat -> Nat := fun y => y + y"
result = server.check_track(src, dst)
print(f"Conforms to spec: {result.succeeded}")
```

--------------------------------

### Adding and Inspecting Environment Definitions

Source: https://context7.com/stanford-centaur/pypantograph/llms.txt

Modify the Lean environment by adding new definitions or inspecting existing ones, including their types and dependencies. Use `env_add` to define new terms and `env_inspect` to query them.

```python
server.env_add(
    name="mystery",
    levels=[],
    t="forall (n: Nat), Nat",
    v="fun (n: Nat) => n + 1",
    is_theorem=False,
)
```

```python
result = server.env_inspect(name="mystery")
print(result['type'])
```

```python
result = server.env_inspect(name="Nat.add", print_dependency=True)
```

```python
server.load_definitions("def foo: Nat -> Nat | 0 => 1 | n + 1 => foo n")
```

```python
definitions = server.env_catalog(module_prefix="Init", invert_filter=True)
print(definitions)
```

```python
head, tail = server.env_parse("intro x; apply a", category="tactic")
print(f"Head: {head}")
print(f"Tail: {tail}")
```

--------------------------------

### Handle Tactic Failures

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

Demonstrates error handling for tactic failures using a `try-except` block. Catches `TacticFailure` exceptions and prints error messages.

```python
from pantograph.message import TacticFailure
try:
    state2 = await server.goal_tactic_async(state1, "assumption")
    print("Should not reach this")
except TacticFailure as e:
    print(e)
    for msg in e.args[0]:
        print(msg)
```

--------------------------------

### Check File Conformance (Failure)

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/frontend.ipynb

Compares two Lean code snippets where the destination has been tampered with, causing a type clash in the 'property' theorem. The result indicates a 'Type clash' failure.

```python
src = """
def f : Nat -> Nat := sorry
theorem property (n : Nat) : f n = n + 1 := sorry
"""
# Tampering!
dst = """
def f (x : Nat) := x + 1
theorem property (n : Nat) : 0 = 0 := rfl
"""
await server.check_track_async(src, dst)
```

--------------------------------

### Execute Special 'Have' Tactic

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

Demonstrates using the special `TacticHave` tactic to introduce a new hypothesis. This requires creating a `TacticHave` instance.

```python
state0 = await server.goal_start_async("1 + 1 = 2")
state1 = await server.goal_tactic_async(state0, TacticHave(branch="2 = 1 + 1", binder_name="h"))
print(state1)
```

--------------------------------

### Access Goals within a State

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

Retrieves and prints the first goal from a goal state. This allows inspection of individual goals.

```python
print(state1.goals[0])
```

--------------------------------

### Garbage Collect Unused Goals

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

Frees up resources by calling `server.gc_async()` to delete goals that are no longer referenced.

```python
await server.gc_async()
```

--------------------------------

### Executing Tactics

Source: https://context7.com/stanford-centaur/pypantograph/llms.txt

Apply tactics to a goal state using `goal_tactic`. Supports simple tactic strings and specialized tactic objects like `TacticHave`, `TacticLet`, and `TacticDraft`.

```APIDOC
## Executing Tactics

The `goal_tactic` method applies a tactic to a goal state and returns the resulting new goal state. Tactics can be simple strings or specialized tactic objects like `TacticHave`, `TacticLet`, `TacticExpr`, and `TacticDraft`.

### Request Example
```python
from pantograph import Server
from pantograph.expr import TacticHave, TacticLet, TacticDraft, Site

server = Server(imports=['Init'])

# Simple tactic execution
state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
state1 = server.goal_tactic(state0, tactic="intro a b h")
print(state1)
# Output:
# a : Prop
# b : Prop
# h : a ∨ b
# ⊢ b ∨ a

state2 = server.goal_tactic(state1, tactic="cases h")
print(f"Goals after cases: {len(state2.goals)}")  # Output: 2

# Apply tactic to specific goal using Site
state3 = server.goal_tactic(state2, tactic="apply Or.inl", site=Site(goal_id=1))
state4 = server.goal_tactic(state3, tactic="assumption")
print(f"Remaining goals: {len(state4.goals)}")  # Output: 1

# Using TacticHave to introduce a hypothesis
server2 = Server(imports=['Init'])
state0 = server2.goal_start("1 + 1 = 2")
state1 = server2.goal_tactic(state0, tactic=TacticHave(branch="2 = 1 + 1", binder_name="h"))
print(f"Goals: {len(state1.goals)}")  # Output: 2
print(state1.goals[0].target)  # Output: 2 = 1 + 1
print(state1.goals[1].target)  # Output: 1 + 1 = 2

# Using TacticLet for let bindings
state0 = server2.goal_start("1 + 1 = 2")
state1 = server2.goal_tactic(state0, tactic=TacticLet(branch="2 = 1 + 1", binder_name="h"))
# Creates goals with let-bound variable
```
```

--------------------------------

### Read and Print Lean Compilation Units

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/frontend.ipynb

Reads the content of a Lean file and iterates through the extracted compilation units, printing their boundaries and source text. This is useful for inspecting the structure of the Lean file as parsed by Pantograph.

```python
with open(project_path / "Example.lean", 'rb') as f:
    content = f.read()
    for i, unit in enumerate(units):
        print(f"#{i}: [{unit.i_begin},{unit.i_end}]")
        unit_text = content[unit.i_begin:unit.i_end].decode('utf-8')
        print(unit_text)
```

--------------------------------

### Extracting Tactic Invocations

Source: https://context7.com/stanford-centaur/pypantograph/llms.txt

Extract tactic invocation data, including before/after goal states and used constants, from Lean source files using `tactic_invocations`. This is useful for generating ML training data.

```python
# Extract tactic invocations from a file
# (Assumes file_path points to a valid .lean file)
# units = server.tactic_invocations(Path("./Example.lean"))
# for unit in units:
#     if unit.invocations:
#         for inv in unit.invocations:
#             print(f"Tactic: {inv.tactic}")
#             print(f"Before: {inv.before}")
#             print(f"After: {inv.after}")
#             print(f"Used constants: {inv.used_constants}")
```

--------------------------------

### Python Output for Companion Generation

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

The output shows the coupled search target generated by Pantograph, combining a definition with its properties.

```text
⊢ { f // ∀ (n : Nat), f n = n + 1 }
```

--------------------------------

### Execute Special 'TacticExpr' Tactic

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/goal.ipynb

Uses `TacticExpr` to parse and apply a Lean expression as a tactic. This is useful for proofs that can be expressed directly as functions.

```python
state0 = await server.goal_start_async("forall (p : Prop), p -> p")
state1 = await server.goal_tactic_async(state0, "intro p")
state2 = await server.goal_tactic_async(state1, TacticExpr("fun h => h"))
print(state2)
```

--------------------------------

### Pypantograph Expr Module Members

Source: https://github.com/stanford-centaur/pypantograph/blob/main/doc/api-expr.rst

Lists all members exported by the pantograph.expr module.

```APIDOC
## Module: pantograph.expr

### Description
This module contains expressions and tactics for the pypantograph library.

### Members
This module exports the following members:

- **Expr**: A data type representing an expression.
- **Tactic**: A data type representing a tactic.

### Data

- **pantograph.expr.Expr**: Represents an expression.
- **pantograph.expr.Tactic**: Represents a tactic.
```

--------------------------------

### Checking Types of Lean Expressions

Source: https://context7.com/stanford-centaur/pypantograph/llms.txt

Determine the type of any Lean expression using `expr_type`. This is useful for validating expressions and understanding their types in the Lean environment.

```python
t = server.expr_type("forall (n m: Nat), n + m = m + n")
print(t)
```

```python
t = server.expr_type("fun (n: Nat) => n + 1")
print(t)
```

```python
t = server.expr_type("List.map (fun x => x + 1)")
print(t)
```
Tokens:
Raw