Tactics reference

Tactics operate on the current proof state: a list of hypotheses, a list of eigenvariables, and a goal. Most tactics finish with a period. Several accept optional annotations described at the end of this page.

General tactics

intros

intros.
intros <HYP> ... <HYP>.

Introduces the leading universal quantifiers and implications of the goal. Each universally quantified variable becomes an eigenvariable and each implication premise becomes a hypothesis.

The optional names give the new hypotheses. The anonymous name _ lets Abella choose:

intros H1 H2.

induction

induction on <NUM> ... <NUM>.

Performs induction on the hypotheses selected by the numeric arguments. The numbers count implications in the goal, starting at one. The selected hypotheses must be inductively defined.

With one argument, the tactic creates a single inductive hypothesis. With several arguments, it performs mutual induction and creates one hypothesis per argument:

induction on 1.
induction on 1 1.

The induction produces the * and @ size annotations described in Inductive restrictions.

coinduction

coinduction.

Applies co-induction to a goal whose head is a co-inductively defined predicate. It adds a co-inductive hypothesis annotated with + and marks the goal with #.

coinduction.
unfold.

case

case <HYP>.
case <HYP> (keep).

Performs case analysis on a hypothesis and, by default, removes it. The keep annotation, written (keep) after the hypothesis, retains it in every generated subgoal.

Case analysis is the main way to analyze a specification-level judgment. The number and shape of the subgoals follow the clauses that could have produced the judgment. See Provability in the reasoning logic.

search

search.
search <NUM>.
search with <WITNESS>.

Searches for a proof of the current goal. The numeric argument overrides the default depth, which is 5 or the value set by Set search_depth.

When the goal is a specification-level judgment, search corresponds to the executable semantics of the specification. When the goal is atomic, search looks in the hypotheses and in the definition clauses.

A witness can be supplied to guide the search:

search with split (apply H1, *).

The witness grammar is:

w ::= true
    | apply <HYP>
    | left w
    | right w
    | split (w, w)
    | intros [<HYP>, ...] w
    | forall [<VAR>, ...] w
    | exists [<VAR> = <TERM>, ...] w
    | unfold (<HYP>, <NUM>, w, ...)
    | *
    | =
    | (w)

* is a wildcard witness and = selects reflexivity. Witnesses are printed after each successful search when Set witnesses on is in effect.

apply

apply <HYP>.
apply <HYP> to <HYP> ... <HYP>.
apply <HYP> to <HYP> ... <HYP> with <VAR> = <TERM>, ... .
apply <HYP> with <VAR> = <TERM>, ... .
apply <DEPTH> <HYP> to ... .

Applies a hypothesis of the form

forall A1 ... Ai, nabla z1 ... zj, H1 -> ... -> Hk -> G

to argument hypotheses matching H1, ..., Hk. The result, an instance of G, is added as a new hypothesis.

A previously proved theorem may be used in place of the first hypothesis, which is how lemmas are applied.

The with clause instantiates quantified variables. An argument may be replaced by _ to use apply with unknowns: Abella guesses the missing hypothesis and tries to prove it with search. A leading number bounds the depth of that search. Instantiating a forall-quantified variable avoids capture: bound variables in the lemma are renamed when necessary.

apply IH to H3 H5.
apply IH to _ H4 H5.
apply even_odd_nat.
apply my_lemma to H1 with X = n1.

Omitting the to clause simply adds the instantiated hypothesis. This is useful for introducing a lemma or for extracting one conjunct of a mutually inductive theorem.

backchain

backchain <HYP>.
backchain <HYP> with <VAR> = <TERM>, ... .
backchain <DEPTH> <HYP>.

The dual of apply. It matches the conclusion of the hypothesis against the current goal and replaces the goal with the hypothesis's premises. It then runs search on each generated subgoal, so trivial premises disappear immediately.

backchain step_det.

A with clause instantiates quantified variables before matching. A leading number bounds the search depth for the generated subgoals.

assert

assert <FORMULA>.
assert <DEPTH> <FORMULA>.

Changes the current goal to the asserted formula. Once the formula is proved, the original goal returns with the formula added as a hypothesis. If search can prove the formula immediately, it is discharged automatically.

The tactic is useful when the search strategy needs guidance:

assert ctx (of n1 T :: L).

The optional leading number bounds the automatic search.

split

split.
split*.

Splits a conjunctive goal into one subgoal per conjunct. split* also adds the earlier conjuncts as hypotheses in the later subgoals.

split.

left and right

left.
right.

Select the left or right disjunct of a goal G1 \/ G2.

witness and exists

witness <TERM>.
witness <VAR> = <TERM>, ... .
exists <TERM>.
exists <VAR> = <TERM>, ... .

Instantiates the leading existential quantifier with the given term. The named form can supply several witnesses at once:

exists Q' = q0.
witness (abs R).

witness and exists are synonyms.

unfold

unfold.
unfold <CLAUSE-SELECTOR>.
unfold (all).
unfold <CLAUSE-SELECTOR> (all).

Replaces a defined predicate in the goal by its clauses. Without a selector, the first matching definition is unfolded. A numeric selector picks the definition by position; a name selector picks it by predicate name.

(all) unfolds every matching clause rather than only the first, which produces one subgoal per clause.

unfold.
unfold sim.
unfold (all).

Computation and forward chaining

compute

compute <HYP> ... <HYP>.
compute *<HYP> ... .
compute <NUM> <HYP> ... .
compute (all).
compute (*all).

Evaluates the named hypotheses asynchronously. Computation repeatedly unfolds definitions and case-analyzes hypotheses, stopping when a suspension guard applies, when no further progress is possible, or when the gas limit is exhausted. The optional number is the gas limit; the default is 1000.

A Suspend command declares the guards used by computation. The member predicate has a built-in guard on its list argument.

Define $nat : nat -> prop by
  $nat z ;
  $nat (s X) := $nat X.

Suspend $nat X.

Theorem ten : forall X, $nat (s^10 X) -> $nat X.
intros. compute H1. search.

compute *H1. removes H1 after computing it. compute (all) tries every hypothesis, and compute (*all) also removes the computed hypotheses. The tactic may produce subgoals; computation continues on each branch.

fchain

[hint:] fchain [<DEPTH>] <LEMMA> ... <LEMMA>.

Forward-chains the listed lemmas against the hypotheses in scope. The lemmas are tried from left to right, and their immediate consequences are added as hypotheses. The optional depth bounds the number of iterations and defaults to the number of lemmas. The tactic is branching: it may produce subgoals.

Type p, q, r tm -> prop.

Axiom p_q : forall X, p X -> q X.
Axiom q_r : forall X, q X -> r X.

Theorem chain : forall X, p X -> r X.
intros. fchain p_q q_r. search.

Specification logic tactics

These tactics exploit properties of the specification logic that are not available for arbitrary reasoning-level predicates.

inst

inst <HYP> with <NOMINAL> = <TERM>, ... .

Given a hypothesis of the form {... n ...} where n is a nominal constant, produces the hypothesis with n replaced by the given term. This implements the meta-level substitution property of the specification logic.

inst H8 with n1 = N.

The hypothesis must be a specification-level judgment, and each left-hand side must be a nominal constant in its support.

cut

cut <HYP> with <HYP>.
cut <HYP>.
cut (<TERM>) from <HYP> with <HYP>.

Given hypotheses {L1, A |- C} and {L2 |- A}, creates {L1, L2 |- C}. This is the meta-level cut property of the specification logic.

Without a with argument, search finds a suitable second hypothesis. The from form names an explicit term to cut from the context, which is useful when the hypothesis is normalized or when its goal formula is not the one to remove.

cut H9 with H6.
cut H9.
cut (of N U) from H9 with H6.

monotone

monotone <HYP> with <TERM>.

Given a hypothesis {L |- C} and a term K, adds {K |- C} as a hypothesis and creates a subgoal with the obligation

forall X, member X L -> member X K.

This is the meta-level monotonicity property of specification contexts. Abella often applies monotonicity automatically during unification, so explicit uses of this tactic are rare.

Proof state manipulation

undo

undo.

Undoes the previous tactic. It may be repeated. The tactic is available only in interactive mode; in batch mode it is an error. Use #back at the top level for the corresponding interactive command.

skip

skip.

Accepts the current subgoal without proof. The result is logically unsound but is useful while developing a proof. Abella records that the proof used skip and reports it in interactive and batch mode.

abort

abort.

Gives up on the current theorem and returns to the top level without recording the theorem.

clear

clear.
clear <HYP> ... <HYP>.
clear -> <HYP> ... <HYP>.

Without arguments, clear removes duplicate predicate hypotheses, keeping the earliest occurrence. Hypotheses that are not atomic predicates are left unchanged.

With arguments, the first form removes the named hypotheses. The second form removes them and returns the named variables and hypotheses to the goal as universally quantified implications.

For example, given

Variables: X Y
H1 : X = Y
============================
 Y = X

the tactic clear -> H1 Y. produces

Variables: X
============================
 forall Y, X = Y -> Y = X

A variable that is still needed cannot be cleared, and neither can a hypothesis that a remaining goal depends on.

abbrev and unabbrev

abbrev <HYP> ... <HYP> "<TEXT>".
unabbrev <HYP> ... <HYP>.

abbrev replaces the display of the named hypotheses with the given text. unabbrev restores the original display. The underlying hypotheses are not changed.

abbrev H1 H2 "typing facts".
unabbrev H1 H2.

rename

rename <OLD> to <NEW>.

Renames a hypothesis or an eigenvariable. The old name must exist and the new name must be unused.

rename H3 to H_typing.
rename X to Y.

permute

permute (<NOMINAL> ... <NOMINAL>).
permute (<NOMINAL> ... <NOMINAL>) <HYP>.

Permutes the named nominal constants in the goal, or in the given hypothesis. The arguments must form a permutation. This is useful for aligning the names in a goal with the names expected by a lemma.

permute (n1 n2).
permute (n1 n2) H3.

Tactic arguments and annotations

Naming generated hypotheses

Most tactics accept an optional name: prefix that names the hypothesis they generate:

IH: induction on 1.
H_typing: assert {of N U}.

This is useful when a proof refers to the generated hypothesis later and the automatic name would be fragile. The prefix is accepted by induction, coinduction, apply, cut, inst, case, assert, and monotone.

Removing or keeping hypotheses

apply, backchain, cut, and monotone accept a * before a hypothesis argument to remove that hypothesis after use. case accepts (keep) to avoid removing its hypothesis.

apply IH to *H3 H5.
case H1 (keep).

Depth arguments

search, apply, backchain, and assert accept a leading number that bounds search. For apply and backchain, the bound applies to the search for generated premises. For assert, it applies to the automatic attempt to prove the asserted formula.

search 10.
apply 2 IH to H1.
assert 3 (member X L).

all

all is not a standalone tactic. It appears as the argument (all) of unfold, where it selects every matching clause, and of compute, where it selects every hypothesis.

by, as, from, on, to, with

These words are part of the syntax of other commands and tactics rather than tactics themselves:

• by separates the declarations from the clauses in Define and CoDefine;
• as introduces names in Split;
• from supplies an explicit context formula in cut;
• on introduces the hypothesis numbers in induction;
• to introduces the argument hypotheses in apply;
• with introduces instantiations in apply, backchain, cut, inst, monotone, search, and the Import command.