Istari

Tactics

Istari tactics have the type tactic; they operate on the current goal, generating zero or more subgoals.

Combinators

Hypotheses

Many tactics take a hypothesis or a list of hypotheses as an argument. Hypotheses are given by the grammar:

Hypothesis ::= [name]
               [number]
               # [number]
               \ ... antiquoted name ... \
               # \ ... antiquoted number ... \

Hypothesis numbers count backward from the end of the context, starting with 0. The # to indicate a number is optional for literal numbers, but it is required for antiquoted numbers.

In IML hypotheses are given by the datatype:

datatype hypothesis = NAME of symbol | NUMBER of int

which appears in the Hyp structure.

Introduction tactics

Hypothesis tactics

Equality tactics

Substitution

The substitution tactics above first attempt to use a substitution rule that does not allow the substitution variable (i.e., the variable being substituted for) to appear in the conclusion. If that fails, they use a more general rule that allows it. The former rule is preferable, because it does not generate a proof obligation that the conclusion is well-formed. However, in unusual circumstances this can result in a surprising behavior: if the conclusion mentions an evar that might or might not depend on the substitution variable, that possible dependency is pruned out. More predictable behavior can be obtained using substCautious, which will always prune out any possible dependency in the conclusion.

Type equality and subtyping tactics

Destruction

Destruction and other tactics use intro patterns, defined by the datatype:

datatype ipattern =
   Wild
 | Ident of Symbol.symbol option
 | And of ipattern list
 | Or of ipattern list

Wild discards the term being matched. Ident creates a hypothesis for the term being matched, using the indicated name (if SOME) or inventing a new name (if NONE). And breaks a conjunctive term into component parts, matching a pattern against each of them. Or case-analyses a disjunctive term, generating a subgoal for each case, and matching a pattern against the disjunct in each case.

The syntax for intro patterns is:

PatternAtom ::= 0                                  (Or [])
                _                                  (Wild)
                ?                                  (Ident NONE)
                [name]                             (Ident (SOME name))
                (Pattern)
                [PatternAtom ... PatternAtom]      (And [p1, ..., pn])
                {PatternArm | ... | PatternArm}    (Or [p1, ..., pn])

PatternArm  ::= PatternAtom ... PatternAtom        (And [p1, ..., pn])

PatternSeq  ::= PatternAtom
                PatternAtom PatternSeq             (And [p1, p2])

Pattern     ::= PatternSeq
                PatternSeq | Pattern               (Or [p1, p2])
                [epsilon]                          (And [])
                [epsilon] | Pattern                (Or [And [], p])

For example:

Syntax Parses to:
p1 p2 p3 And [p1, And [p2, p3]]
[p1 p2 p3] And [p1, p2, p3]
p1 p2 p3 | p4 | p5 Or [And [p1, And [p2, p3]], Or [p4, p5]]
{p1 p2 p3 | p4 | p5} Or [And [p1, p2, p3], And [p4], And [p5]]

The effect of the pattern match depends on the type being matched:

The destruction tactics are:

Chaining

Generalization

Induction

Typechecking

Autotactic

Arithmetic

Omega understands the following constants in arithmetic expressions:

Other expressions are uninterpreted and taken as additional variables.

In propositions Omega understands:

Other propositions are treated as void in positive positions, and as unit in negative positions.

Note that quantified propositions are not understood. For example, forall x . x <= x in a positive position (such as the conclusion) is treated as void. Consequently it fails with an empty counterexample, which may be surprising.

Terms must be identical to be taken as the same uninterpreted variable. This can be surprising, particularly with terms that mention evars. For example, the terms `length nat L and `length E1 L are taken as two different terms – even though they display the same way – which will very likely cause Omega to fail. To lessen the likelihood of this, omega (but not omegaRaw) runs the inference tactic first to attempt to resolve evars. Nevertheless, it is possible for evars to leak through inference.

Some forms require Omega to search multiple possibilities. This includes prod in a positive position, sum or arrow in a negative position, and any function that is defined by cases (e.g., minus, pred, min, max, or integer_to_nat). Each appearance of such a form doubles the effective size of the constraint, which will affect performance. However, multiple occurrences of the same expression will not double the size multiple times.

Miscellaneous tactics

Rewriting, reordering, and case analysis are documented on their own pages.

The tactic monad

The tactic type is a special case of the tactic monad type 'a tacticm, which is like an ordinary tactic except it passes a value of type 'a to each subgoal. Ordinary tactics are then defined:

type tactic = Message.label tacticm

The label contains information that is attached to the subgoal when it is displayed for the user. Most tactics leave it empty.

Most of the tactic combinators actually have more general types than given above, using the tactic monad:

fail        : string -> 'a tacticm
cut         : 'a tacticm -> 'a tacticm
lift        : (unit -> 'a tacticm) -> 'a tacticm
done        : 'a tacticm
andthen     : 'a tacticm -> 'b tacticm -> 'b tacticm
andthenl    : 'a tacticm -> 'b tacticm list -> 'b tacticm
andthenlPad : 'a tacticm -> 'b tacticm list -> 'b tacticm -> 'b tacticm
andthenOn   : int -> 'a tacticm -> 'a tacticm -> 'a tacticm
first       : 'a tacticm list -> 'a tacticm
orthen      : 'a tacticm -> (unit -> 'a tacticm) -> 'a tacticm
ifthen      : 'a tacticm -> 'b tacticm -> 'b tacticm -> 'b tacticm

Several of the combinators also have monadic versions that serve as the monad’s unit and various flavors of bind:

idtacM       : 'a -> 'a tacticm
andthenM     : 'a tacticm -> ('a -> 'b tacticm) -> 'b tacticm
andthenlM    : 'a tacticm -> ('a -> 'b tacticm) list -> 'b tacticm
andthenlPadM : 'a tacticm -> ('a -> 'b tacticm) list -> ('a -> 'b tacticm) -> 'b tacticm
andthenOnM   : int -> 'a tacticm -> ('a -> 'a tacticm) -> 'a tacticm
ifthenM      : 'a tacticm -> ('a -> 'b tacticm) -> 'b tacticm -> 'b tacticm

The monadic operations andthenM and andthenlM have the infix operators >>= and >>>= as synonyms.

The most general flavor of bind is:

andthenFoldM :
   'a tacticm 
   -> ('a -> 'b -> 'c tacticm * 'b)
   -> ('b -> string option)
   -> 'b
   -> 'c tacticm

The tactic andthenFoldM tac1 tacfn finish x first runs tac1. It then folds tacfn left-to-right over the subgoals. Each invocation is passed (1) the monadic argument of type 'a that was passed to that subgoal, and (2) a current value of type 'b; and returns a 'c tacticm (which is used on that subgoal) and a new value of type 'b that will be used with the next subgoal. The initial 'b value is x. Suppose the final 'b value is y. Then finish y is evaluated and if the result is SOME msg, the entire tactic fails using error message msg.

Exceptions

Exceptions tend to work clumsily with continuation-passing style. The tryf function mediates the interface between them:

exception Tactic.Tryf of string
Tactic.tryf : (unit -> 'a) -> ('a -> 'b tacticm) -> 'b tacticm

The tactic tryf f tac will call f () to obtain x : 'a, and then execute tac x. But if f () raises Tryf msg, the combinator calls fail msg instead.

Low-level tactics

These tactics are primarily used to implement other tactics:

This site is open source. Improve this page.