6.2.901.900
3.1 Tactics
As Coq has shown, tactics have proven useful for doing complex proofs. In Cur, tactics are not built-in or provided by the language. However, any user can use meta-programming to add tactics to Cur. A tactic system ships in the standard library, written entirely in user-land code.
3.1.1 Proof State and Defining Tactics
| (require cur/stdlib/tactics/base) | package: cur |
Defines a new tactic, at phase 1. A tactic is a Racket function from
proof state to proof state that runs at phase 1. A tactic takes any
number of arguments, plus the proof state. The proof state must be the final argument of
the tactic.
Examples: | |||||||
|
Returns #t if p is a proof, and #f otherwise.
A proof is either a Cur term as a syntax object, or a procedure expecting a proof to plug
into the holes of the existing partial proof.
Returns #t is the proof p has no holes, i.e., is a syntax object, and #f
otherwise.
Returns an empty partial proof, i.e., the identity function.
struct
(struct proof-state (env goals current-goal proof theorem) #:extra-constructor-name make-proof-state) env : dict? goals : dict? current-goal : natural-number/c proof : (or/c syntax? procedure?) theorem : syntax?
The environment env is a map of assumptions local to the theorem from symbols (names) to the
type of the assumption as a syntax object.
The list of goals goals is a map from natural numbers to goals, types as syntax objects.
The current goal current-goal is a natural number indexing into goals, representing
the goal currently in focus.
The proof is the proof of the theorem so far. The proof is either a
syntax object if complete, or a procedure which expects a proof to replace the current holes in the
proof.
The theorem is the original statement of the theorem to be proved.
Returns a proof-state? initialized with an empty environment, the list of goals initialized with
prop, the current-goal set to 0, an empty proof via (new-proof), and the
theorem set to prop.
Returns #t is the proof of the proof-state? ps is a
complete-proof?, and #f otherwise.
Returns the ith goal from the proof state ps.
Returns the goal using the index from
(proof-state-current-goal ps).
Returns the type of the assumption name in the local
environment of ps.
Returns the name of the assumption of type type from the local
environment of ps, or #f is no
assumption with type exists.
procedure
ps : proof-state? name : (or/c symbol? identifier?) type : syntax?
Returns a proof state with the local environment of
ps updated to include the assumption name of type
type.
Returns a proof state with the current goal in the goals list of
ps changed to goal.
Returns a proof state with the current holes of the proof filled with
pf.
procedure
ps : proof-state? ctxt : procedure?
Updates the proof in ps by playing the current proof inside the
holes of ctxt.
Pretty-prints ps to the current-output-port.
Returns the tactic defined with name name. Only works when the
tactic is defined and a theorem has been defined but not proved.
Defines a new theorem.
Proves the theorem previously defined with define-theorem. Currently, this proof is not
saved anywhere, only checked against the most recent theorem defined via define-theorem.
Note that the proof state is implicitly given to each call by proof and should not appear as an explicit argument.
Examples: | |||||
|
TODO: Examples, better documentation (e.g. don’t say "returns a proof state"; the signature says so)
3.1.2 Standard Tactics
The tactic system includes several standard tactics.
| (require cur/stdlib/tactics/standard) | package: cur |
Matches when the current goal has the form (forall (id : type-expr) body-expr), introducing
the assumption id : type-expr into the local environment of ps.
Matches with the current goal has a type that matches an assumption in the local environment of
ps. Completes the goal.
Attempts to prove the current goal by doing the obvious thing.
Resets ps to its state when the proof began. Clears the proof and goals, reinitializing the
goals to the original theorem.
Prints ps, returning it unmodified.
Removes the assumption x from the local environment of ps.
3.1.3 Interactive Tactic
In Cur, interactivity is just a user-defined tactic.
Starts a REPL that prints ps, reads a tactic (as proof would), evaluates the
tactic, and repeats. To quit, use (quit).
3.1.4 SarTactic (Sarcastic Tactics)
| (require cur/stdlib/tactics/sartactic) | package: cur |
The SarTactic library provides amusing wrappers around the standard tactics. This library exists mostly for the author’s own amusement, and to ensure the extensibility of the tactic system.
It defines the same tactics as cur/stdlib/tactics/standard, but each tactics will insult the user, and will only work some of the time.