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

ruleand_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:

valand_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`.

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:

typetactic = tactic_arg -> tactic_value

The following operations are defined on values of type `tactic_arg`.

valgoal : tactic_arg -> termvalmsequent : tactic_arg -> msequentvalnth_hyp : tactic_arg -> int -> string * termvalnth_concl : tactic_arg -> int -> termvalcache : tactic_arg -> cachevallabel : 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 acutrule

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

valget_term : tactic_arg -> string -> termvalget_term_list : tactic_arg -> string -> term listvalget_type : tactic_arg -> string -> termvalget_int : tactic_arg -> string -> intvalget_bool : tactic_arg -> string -> boolvalget_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:

valsetLabelT : string -> tacticvalwithTermT : string -> term -> tactic -> tacticvalwithTermListT : string -> term list -> tactic -> tacticvalwithTypeT : string -> term -> tactic -> tacticvalwithBoolT : string -> bool -> tactic -> tacticvalwithIntT : string -> int -> tactic -> tacticvalwithSubstT : 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.

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

topvalidT : tactictopvalfailT : tactic

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

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 & 'Band'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`):

topvalnthAssumT : 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] }BYD 0Subgoal 1:Assums:sameGoal: sequent { 'H >- 'A type }BYnthAssumT 2 Subgoal 2: Assums:sameGoal: sequent { 'H; a: 'A >- 'B['a] }BYnthAssumT 1

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:

topvalprefix_orelseT : tactic -> tactic -> tactictopvalprefix_orthenT : tactic -> tactic -> tactictopvalprefix_thenT : tactic -> tactic -> tactictopvalprefix_thenLT : tactic -> tactic list -> tacticvalprefix_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 [tac`*1*`;
...; tac`*n*`])` is applied, `tac` must
produce *n* subgoals. Then `tac`*i* 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.

There are several tactics for conditional application and looping.

valifT : (tactic_arg -> bool) -> tactic -> tactic -> tacticvalifThenT : (term -> bool) -> tactic -> tacticvalwhileT : (term -> bool) -> tactic -> tacticvaluntilT : (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.

topvalprogressT : tactic -> tactictopvalrepeatT : tactic -> tactictopvalrepeatForT : 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.