Goals and Tactics

Goals and Tactics#

Executing tactics in Pantograph is simple. To start a proof, call the Server.goal_start function and supply an expression.

from pantograph import Server
from pantograph.expr import TacticHave, TacticCalc, TacticExpr

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)

⊢ forall (p q: Prop), Or p q -> Or q p

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.

state1 = server.goal_tactic(state0, goal_id=0, tactic="intro a")
print(state1)

a : Prop
⊢ ∀ (q : Prop), a ∨ q → q ∨ a

Executing a tactic produces a new goal state. If this goal state has no goals, the proof is complete. You can recover the usual form of a goal with str()

str(state1.goals[0])

'a : Prop\n⊢ ∀ (q : Prop), a ∨ q → q ∨ a'

Error Handling and GC#

When a tactic fails, it throws an exception:

try:
    state2 = server.goal_tactic(state1, goal_id=0, tactic="assumption")
    print("Should not reach this")
except Exception as e:
    print(e)

["tactic 'assumption' failed\na : Prop\n⊢ ∀ (q : Prop), a ∨ q → q ∨ a"]

A state with no goals is considered solved

state0 = server.goal_start("forall (p : Prop), p -> p")
state1 = server.goal_tactic(state0, goal_id=0, tactic="intro")
state2 = server.goal_tactic(state1, goal_id=0, tactic="intro h")
state3 = server.goal_tactic(state2, goal_id=0, tactic="exact h")
state3

GoalState(state_id=5, goals=[], _sentinel=[0, 1])

Execute server.gc() once in a while to delete unused goals.

server.gc()

Special Tactics#

Lean has special provisions for some tactics. This includes have, let, calc. To execute one of these tactics, create a TacticHave, TacticLet, TacticCalc instance and feed it into server.goal_tactic.

Technically speaking have and let are not tactics in Lean, so their execution requires special attention.

state0 = server.goal_start("1 + 1 = 2")
state1 = server.goal_tactic(state0, goal_id=0, tactic=TacticHave(branch="2 = 1 + 1", binder_name="h"))
print(state1)

⊢ 2 = 1 + 1
h : 2 = 1 + 1
⊢ 1 + 1 = 2

The TacticExpr “tactic” parses an expression and assigns it to the current goal. This leverages Lean’s type unification system and is as expressive as Lean expressions. Many proofs in Mathlib4 are written in a mixture of expression and tactic forms.

state0 = server.goal_start("forall (p : Prop), p -> p")
state1 = server.goal_tactic(state0, goal_id=0, tactic="intro p")
state2 = server.goal_tactic(state1, goal_id=0, tactic=TacticExpr("fun h => h"))
print(state2)

To execute the conv tactic, use server.goal_conv_begin to enter conv mode on one goal, and use server.goal_conv_end to exit from conv mode. Pantograph will provide interactive feedback upon every tactic executed in conv mode.

Contents