Tactics

In this page, we use the following LF signature to parameterize proof developments on this page. These developments will display each tactic being used, usually through a toy theorem.

tactics.lf

nat : type.
z : nat.
s : {N:nat} nat.
 
plus : nat -> nat -> nat -> type.
plus-z : {N:nat} plus z N N.
plus-s : {N1:nat}{N2:nat}{N3:nat}
         {D: plus N1 N2 N3}
         plus (s N1) N2 (s N3).

search [<NUM>].

Search for a derivation of the current goal using matching with assumption formulas and decomposing judgments into subgoals using LF derivation rules. If a <NUM> is provided, assumption judgements are decomposed <NUM> times. If a <NUM> is not provided, the search_depth option is used. The search_depth can be changed with the Set command.

intros.

Introduces variables and assumptions from a goal formula until it no longer has top-level universal quantification, context quantification, or implications.

Specification "tactics.lf".
Schema C := ().
Theorem intro-example: ctx G:C, forall N1, { N1 : nat } => { s N1 : nat }.
intros.

split.

Creates subgoals for each sub formula, F1 and F2 if the current goal is a conjunction F1 /\ F2.

Theorem split_example : true /\ false.
split.

left.

Changes the goal to be the left side formula, F1 if the current goal is a disjunction, F1 \/ F2.

Theorem left_example : true \/ false.
left.

right.

Changes the goal to be the right side formula, F2 if the current goal is a disjunction, F1 \/ F2.

Theorem right_example : false \/ true.
right.

assert <FORMULA> [<NUM>].

Changes the proof state to one which has the given formula as a goal; once derivation of this goal is complete returns to the previous proof state with the given formula added as an assumption. Providing a <NUM> will decompose assumption judgements <NUM> times. If the asserted formula can be proven, it is added to the proof state immediately. This option defaults to search_depth when not provided and may be changed with the Set command.

Specification "tactics.lf".
 
Theorem plus_exist : forall N1 N2,
  {N1:nat} => {N2:nat} => exists N3 D, {D : plus N1 N2 N3}.
induction on 1. intros. case H1.
apply IH to H3 H2.
% Adelfa decomposes the {D: plus N N2 N3}* assumption
% to find this is derivable, adding it directly to the
% assumption set.
assert { N3 : nat }.
undo.
% We can tell adelfa to not perform any decomposition,
% to find this is derivable, adding it directly to the
% assumption set.
assert { N3 : nat} 0.

apply <NAME> to <HYP NAMES> [with <BINDINGS>].

Applies a hypothesis of the form ctx Gamma1:C1 ... Gammaj:Cj, forall X1 ... Xi, H1 => ... => Hk => F to argument hypotheses which match H1, ..., Hk. The result is an instantiation of F. Either or both of i and j may be zero. That is, there need not be universally quantified variables or context variables. The with clause allows specific instantiations of any of the variables X1 ... Xi and Gamma1 ... Gammaj.

Specification "tactics.lf".
 
Theorem plus-z-rhs : forall N,
  { N : nat } => exists D, { D : plus N z N }.
induction on 1. intros. case H1.
apply IH to H2. exists plus-s N1 z N1 D. search.
exists plus-z z. search.
 
Theorem plus-comm : forall N1 N2 N3 D1,
  { D1 : plus N1 N2 N3 } =>
  % what would be a lemma is listed here to display how one can apply
  % assumption formulas.
  (forall M1 M2 M3 P, { P : plus M1 M2 M3 }
    => exists P2, { P2 : plus M1 (s M2) (s M3) }) =>
  exists D2, { D2 : plus N2 N1 N3 }.
induction on 1. intros. case H1.
apply IH to H6 H2. apply H2 to H7. exists P2. search.
apply plus-z-rhs to H3. exists D. search.

induction on <NUM>.

Given a goal of the form ctx Gamma1:C1 Gamma2:C2 ..., forall X Y ..., H1 => H2 => ... => F the induction tactic allows you to induct on one of H1, H2, .... The hypothesis to be inducted on must be an atomic formula. The choice of induction is based on the number <NUM>. Applying the induction tactic results in an inductive hypothesis being added to the current set of hypotheses. Specifics on this inductive hypothesis and how it relates to the goal are given in the section Inductive Restrictions.

Adelfa supports nested induction through repeated calls to the induction tactic. See the Inductive Restrictions section for more details.

exists M.

Instantiates an existential goal with the given term, if it is of the correct arity type.

Specification "tactics.lf".
 
Theorem exist-example : exists N, { N : nat }.
exists z. search.

case <HYP NAME>[(keep)].

Performs case analysis on the given assumption formula. By default, the assumption is removed, use (keep) to retain it.

Specification "tactics.lf".
 
Theorem cases-example : forall N, {N : nat} => { s N : nat }.
intros. case H1.
% keep derivation which formed { N : nat }
undo. case H1 (keep).

weaken <HYP NAME> with A [<NUM>].

When the given assumption formula is of the form {G |- M : A}, and it can be verified that the LF type A must be well formed in the current context under G, then a new assumption is added in which the typing judgment is weakened to include the given type.

Specification "tactics.lf".
 
Theorem wk-example : forall N, { N : nat } => false.
intros. weaken H1 with nat.

strengthen <HYP NAME>.

If the given assumption formula is of the form {G, n:A1 |- M : A2} if n does not appear in M or A2 then a new assumption is added in which the typing judgment is strengthened to {G |- M : A2}.

ctxpermute <HYP NAME> to G.

If the given assumption is of the form {G' |- M : A}, and if the given context is a valid permutation of the context G' (i.e. does not violate dependencies), then a new assumption is added with the permuted context expression G.

permute <HYP NAME> with <PERM>.

Applies a permutation of nominal constants to the argument hypothesis. <PERM> must be a complete permutation. Mappings can be unidirectional n1 -> n2, n2 -> n or bidirectional n1 <-> n2. If the provided permutation is complete and limited to be within the relevant assumption’s restricted set, a new assumption is added with the permutation applied to it.

inst <HYP NAME> with n = M.

If the given assumption formula is of the form {G1,n:B,G2 |- M:A}, and the term M can be determined to be such that {G1 |- M : B} is valid then this tactic replaces the given assumption with one in which n:B is removed from the context expression and all occurrences of n are replaced by M.

prune <HYP NAME>.

If the given assumption is of the form {G |- X n1 ... nm : A} for some eigenvariable X and distinct nominal constants n1,...,nm then this tactic will prune those nominal constants appearing as arguments to X which

1. Do not already appear in G and
2. Are not permitted in the instantiations for the context variable in G.

undo.

Undoes the last step of reasoning.

skip.

Skip to the next subgoal of the derivation and completes the theorem if there are no more goals.

abort.

Abort the proof construction and return to top-level loop without adding formula to the available lemmas.

unfold [<HYP NAME>].

If the given assumption formula is a defined predicate then it is unfolded using the relevant definition, using the first clause which matches. If no assumption formula is given, the goal formula is unfolded.

applydfn <PROP> [to <HYP NAME>].

Applies a clause of the definition of <PROP> to the given assumption formula. The first clause which matches is the one used. If no assumption formula is provided the definition is applied to the goal formula.