Pantograph/docs/goal.md

Goals and Tactics

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

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.

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