MetaPRL Tacticals

Each rule in a logic defines a tactic. For example, the following and-elimination rule defines a tactic called and_elim:

rule and_elim 'H 'J 'y 'z :
   sequent { 'H; y: 'A; z: 'B; 'J[('y, 'z)] >- C[('y, 'z)] } -->
   sequent { 'H; x: 'A & 'B; 'J['x] >- 'C['x] }

The and_elim tactic has the following ML type:

val and_elim : address -> address -> string -> string -> tactic

The extra arguments are for the parameters of the tactic: two arguments that defined the hypotheses matched by 'H and 'J, and two arguments for the variable names 'y and 'z.

Tactic arguments

The tactic type defined in the Tacticals module differs from the tactic type of the refiner. The Tacticals.tactic type includes an extra argument that represents information about the current goal, including the goal term, the state of the proof cache, and various annotations that are inherited in the proof tree. The tactic type is defined as:

type tactic = tactic_arg -> tactic_value

The following operations are defined on values of type tactic_arg.

val goal        : tactic_arg -> term
val msequent    : tactic_arg -> msequent
val nth_hyp     : tactic_arg -> int -> string * term
val nth_concl   : tactic_arg -> int -> term
val cache       : tactic_arg -> cache
val label       : tactic_arg -> string

These functions have the obvious definitions: the goal function produces the goal term of the argument, the cache function produces the proof cache, the nth_hyp, and nth_concl functions are provided for sequent calculi: they produces the sequent parts of the goal. The msequent function produces the goal, including derived rule assumptions (see the section on nthAssumT).

Proof tree nodes are labeled with annotations that describe properties of the node. Values of type tactic_arg also contain these annotations. One example is the label function, which produces a string describing the "type" of the argument. This values are typically used:

"main": the proof node is a normal node of the proof
"wf": the proof node is part of a well-formedness proof
"aux": the proof node is a "less-important" auxiliary part of a proof
"assertion": the proof node was introduced using a cut rule

There are additional proof node annotations defined by the following functions:

val get_term      : tactic_arg -> string -> term
val get_term_list : tactic_arg -> string -> term list
val get_type      : tactic_arg -> string -> term
val get_int       : tactic_arg -> string -> int
val get_bool      : tactic_arg -> string -> bool
val get_subst     : tactic_arg -> term_subst

Each attribute is associated with a string (the "name" of the attribute). Each get_<kind> function get the named attribute from the argument. There are also tactics to modify the attribute list during refinement:

val setLabelT : string -> tactic
val withTermT : string -> term -> tactic -> tactic
val withTermListT : string -> term list -> tactic -> tactic
val withTypeT : string -> term -> tactic -> tactic
val withBoolT : string -> bool -> tactic -> tactic
val withIntT : string -> int -> tactic -> tactic
val withSubstT : term_subst -> tactic -> tactic

Not all of the attributes can be modified: some are constant values that are initialized by the proof editor when a proof tree is constructed.

Simple tactics

There are several simple tactics. The topval declaration declares a value that is available to the MetaPRL toploop.

topval idT : tactic
topval failT : tactic

The idT tactic is the identity: given a goal T, the idT tactic produces the single subgoal T. The failT tactic always fails.

Assumption tactics

Proofs in MetaPRL are proofs of derived rules. There are two kinds of hypotheses in a derived rule. The subgoals of a derived rule are called assumptions, and the hypotheses of the sequent goal are called hypotheses. For instance, in the proof of the derived rule for and_elim, has one assumption:

sequent { 'H; y: 'A; z: 'B; 'J[('y, 'z)] >- 'C[('y, 'z)] }

and it has three initial hypotheses: the hypotheses of the goal sequent:

'H, x: 'A & 'B and 'J['x].

The tacticals module defines a tactic for a proof by assumption (the corresponding nthHyp tactic is not valid in all logics; the ITT version is in the module Itt_struct):

topval nthAssumT : int -> tactic

This tactic proves a goal only if it matches the assumption exactly (with possible alpha-renaming). For instance, the following proof is valid:

Assums:
1.  sequent { 'H; x: 'A >- 'B['x] }
2.  sequent { 'H >- 'A type }
Goal:
sequent { 'H >- all x: 'A. 'B['x] }
BY D 0

Subgoal 1:
   Assums: same
   Goal: sequent { 'H >- 'A type }
   BY nthAssumT 2

Subgoal 2:
   Assums: same
   Goal: sequent { 'H; a: 'A >- 'B['a] }
   BY nthAssumT 1

Tactic composition

There are several tactics for composition. Most of these tactics are defined as infix operators by the MetaPRL compiler. The prefix form for a tactic named tacT is named prefix_tacT. Here is a list of these tactics:

topval prefix_orelseT : tactic -> tactic -> tactic
topval prefix_orthenT : tactic -> tactic -> tactic
topval prefix_thenT : tactic -> tactic -> tactic
topval prefix_thenLT : tactic -> tactic list -> tactic
val prefix_thenFLT : tactic -> (tactic_arg list -> tactic_value list) -> tactic

The orelseT tactical is used for selection. The application of the tactic (tac1 orelseT tac2) first tries tac1. If the tactic succeeds, the subgoals are returned without applying tac2. Otherwise, if tac1 raises and exception, the exception is discarded and tac2 is applied instead.

The orthenT tactical has a similar behavior, but tac2 is always applied. An application of (tac1 orthenT tac2) first applies tac1. If tac1 fails, the result is discarded. The tac2 tactic is applied to the resulting subgoal.

The thenT tactical is used for tactic sequencing. An application of (tac1 thenT tac2) first applies tac1 to the goal, and then applies tac2 to all the subgoals. The sequence fails if either tac1 or tac2 fail.

The thenLT tactical also performs sequencing, but it allows different tactics to be applied to the subgoals generated by the first tactic. When (tac thenLT [tac1; ...; tacn]) is applied, tac must produce n subgoals. Then taci is applied to subgoal i. The tactic fails if any of the tactics fail, or the number of subgoals is not equal to the length of the tactic list.

The thenFLT tactical is similar to thenLT, but it allows the use of a function to compute the tactic list. The type tactic is defined as tactic_arg -> tactic_value; the thenFLT tactical performs the partial tactic application for the subgoal list.

Conditional tactics and looping

There are several tactics for conditional application and looping.

val ifT : (tactic_arg -> bool) -> tactic -> tactic -> tactic
val ifThenT : (term -> bool) -> tactic -> tactic
val whileT : (term -> bool) -> tactic -> tactic
val untilT : (term -> bool) -> tactic -> tactic

The ifT tactic takes a predicate on an argument. If the predicate holds, the first tactic is applied to the proof node, otherwise the second tactic is applied. The ifThenT tactic is similar, with the following equivalence:

ifThenT pred tac = ifT (function p -> pred (goal p)) tac idT.

The whileT and untilT tacticals perform the standard looping operations.

There are also tactics for constrained looping.

topval progressT : tactic -> tactic
topval repeatT : tactic -> tactic
topval repeatForT : int -> tactic -> tactic

The (progressT tac) tactic performs the same refinement as tac, except it fails if tac does not change the goal of the proof node. For instance (progress idT) always fails. The (repeatT tac) tactic applies tac recursively until a fixpoint is reached. The tactic (repeatForT i tac) repeats the application of tac exactly i times.