7.3 Basics
Tactics presented in this section implement the basic typing rules of
Cic given in chapter 4.
7.3.1 Assumption
This tactic applies to any goal. It implements the
``Var'' rule given in section
4.2. It looks in the local context for an hypothesis
which type is equal to the goal. If it is the case, the subgoal is
proved. Otherwise, it fails.
Error messages:
-
No such assumption
7.3.2 Clear ident.
This tactic erases the hypothesis named ident in the local context
of the current goal. Then ident is no more displayed and no more
usable in the proof development.
Error messages:
-
ident is not among the assumptions.
7.3.3 Move ident1 after ident2.
This moves the hypothesis named ident1 in the local context
after the hypothesis named ident2.
If ident1 comes before ident2 in the order of dependences,
then all hypotheses between ident1 and ident2 which
(possibly indirectly) depend on ident1 are moved also.
If ident1 comes after ident2 in the order of dependences,
then all hypotheses between ident1 and ident2 which
(possibly indirectly)) occur in ident1 are moved also.
Error messages:
-
Cannot move ident1 after ident2:
it occurs in ident2
- Cannot move ident1 after ident2:
it depends on ident2
7.3.4 Intro
This tactic applies to a goal which is a product. It implements the
``Lam'' rule given in section
4.2. Actually, only one subgoal will be generated since the
other one can be automatically checked.
If the current goal is a dependent product (x:T)U and
x is a name that does not exist in the current context, then
Intro puts x:T in the local context. Otherwise, it puts
xn:T where n is such that xn is a
fresh name. The new subgoal is U. If the x has been
renamed xn then it is replaced by xn in U.
If the goal is a non dependent product T -> U, then it
puts in the local context either Hn:T
(if T is Set or Prop) or Xn:T (if
the type of T is Type) or ln:T with l
the first letter of the type of x. n is such that Hn or Xn ln or are fresh identifiers.
In both cases the new subgoal is U.
If the goal is not a product, the tactic Intro applies the tactic
Red until the tactic Intro can be applied or the goal is not
reducible.
Error messages:
-
No product even after head-reduction
Warning: : ident1 is already used; changed to ident2
Variants:
-
Intros
Repeats Intro until it meets the head-constant. It never reduces
head-constants and it never fails.
- Intro ident
Applies Intro but forces ident to be the name of the
introduced hypothesis.
Error message: name ident is already bound
Remark: Intro doesn't check the whole current context. Actually,
identifiers declared or defined in required modules can be used as
ident and, in this case, the old ident of the module is no
more reachable.
- Intros ident1 ... identn
Is equivalent to the composed tactic Intro ident1; ... ; Intro
identn.
More generally, the Intros tactic takes a pattern as argument
in order to introduce names for components of an inductive
definition, it will be explained in 7.7.3.
- Intros until ident
Repeats Intro until it meets a premise of the goal having form
( ident : term )
and discharges the variable named ident of
the current goal.
Error message: No such hypothesis in current goal
- Intros until num
Repeats Intro until the num-th non-dependant premise. For instance,
on the subgoal (x,y:nat)x=y->(z:nat)h=x->z=y
the tactic
Intros until 2 is equivalent to Intros x y H z H0 (assuming
x, y, H, z and H0 do not already occur in context).
Error message: No such hypothesis in current goal
Happens when num is 0 or is greater than the number of non-dependant
products of the goal.
- Intro after ident
Applies Intro but puts the introduced
hypothesis after the hypothesis ident in the hypotheses.
Error messages:
-
No product even after head-reduction
- No such hypothesis : ident
- Intro ident1 after ident2
Behaves as previously but ident1 is the name of the introduced
hypothesis.
It is equivalent to Intro ident1; Move ident1 after ident2.
Error messages:
-
No product even after head-reduction
- No such hypothesis : ident
7.3.5 Apply term
This tactic applies to any goal.
The argument term is a term well-formed in the local context.
The tactic Apply tries to match the
current goal against the conclusion of the type of term. If it
succeeds, then the tactic returns as many subgoals as the
instantiations of the premises of the type of
term.
Error messages:
-
Impossible to unify ... with ...
Since higher order unification is undecidable, the Apply
tactic may fail when you think it should work. In this case, if you
know that the conclusion of term and the current goal are
unifiable, you can help the Apply tactic by transforming your
goal with the Change or Pattern tactics (see sections
7.5.7, 7.3.9).
- Cannot refine to conclusions with meta-variables
This occurs when some instantiations of premises of term are not
deducible from the unification. This is the case, for instance, when
you want to apply a transitivity property. In this case, you have to
use one of the variants below:
Variants:
-
Apply term with term1 ... termn
Provides Apply with explicit instantiations for all dependent
premises of the type of term which do not occur in the
conclusion and consequently cannot be found by unification. Notice
that term1 ... termn must be given according to the order
of these dependent premises of the type of term.
Error message: Not the right number of missing arguments
- Apply term with ref1 := term1 ... refn
:= termn
This also provides Apply with values for instantiating
premises. But variables are referred by names and non dependent
products by order (see syntax in the section 7.3.10).
- EApply term
The tactic EApply behaves as Apply but does not fail when
no instantiation are deducible for some variables in the premises.
Rather, it turns these variables into so-called existential variables
which are variables still to instantiate. An existential variable is
identified by a name of the form ?n where n is a number.
The instantiation is intended to be found later in the proof.
An example of use of EApply is given in section
8.2.
- LApply term
This tactic applies to any goal, say G. The argument term
has to be well-formed in the current context, its type being
reducible to a non-dependent product A -> B with B
possibly containing products. Then it generates two subgoals B->G and A. Applying LApply H (where H has type
A->B and B does not start with a product) does the same
as giving the sequence Cut B. 2:Apply H. where Cut is
described below.
Warning: Be careful, when term contains more than one non
dependent product the tactic LApply only takes into account the
first product.
7.3.6 Let ident := term in
Goal
This replaces term by ident in the goal and add the
equality ident= term in the local context.
Variants:
-
Let ident0 := term in ident1
This behaves the same but substitutes term not in the goal but in
the hypothesis named ident1.
- Let ident0 := term in num1 ...
numn ident1
This notation allows to specify which occurrences of the hypothesis
named ident1 (or the goal if ident1 is
the word Goal) should be substituted. The occurrences are numbered
from left to right. A negative occurrence number means an occurrence
which should not be substituted.
- Let ident0 := term in num11 ...
numn11 ident1 ...num1m ...
numnmm identm
This is the general form. It substitutes term at occurrences
num1i ... numnii of hypothesis identi. One
of the ident's may be the word Goal.
7.3.7 Cut form
This tactic applies to any goal. It implements the
``App'' rule given in section
4.2. Cut U transforms the current goal T
into the two following subgoals: U -> T and U.
Error messages:
-
Not a proposition or a type
Arises when the argument form is neither of type Prop, Set nor Type.
7.3.8 Generalize term
This tactic applies to any goal. It generalizes the conclusion w.r.t. one
subterm of it. For example:
Coq < Show.
1 subgoal
x : nat
y : nat
============================
(le O (plus (plus x y) y))
Coq < Generalize (plus (plus x y) y).
1 subgoal
x : nat
y : nat
============================
(n:nat)(le O n)
If the goal is G and t is a subterm of type T
in the goal, then Generalize t replaces the goal by (x:T)G' where G' is obtained from G by replacing all
occurrences of t by x. The name of the variable (here x)
is chosen accordingly to T.
Variants:
-
Generalize term1 ... termn
Is equivalent to Generalize termn; ... ; Generalize
term1. Note that the sequence of termi's are processed from
n to 1.
- Generalize Dependent term
This generalizes term but
also all hypotheses which depend on term.
7.3.9 Change term
This tactic applies to any goal. It implements the rule
``Conv'' given in section 4.3.
Change U replaces the current goal T with a U providing
that U is well-formed and that T and U are
convertible.
Error messages:
-
convert-concl rule passed non-converting term
Variants:
-
Change term in ident
This applies the Change tactic not to the goal but to the
hypothesis ident.
See also: 7.5
7.3.10 Bindings list
A bindings list is generally used after the keyword with in
tactics. The general shape of a bindings list is ref1 :=
term1 ... refn := termn where ref is either an
ident or a num. It is used to provide a tactic with a list of
values (term1, ..., termn) that have to be substituted
respectively to ref1, ..., refn. For all i Î [1... n], if
refi is identi then it references the dependent product identi:T (for some type T); if refi is numi then it
references the numi-th non dependent premise.
A bindings list can also be a simple list of terms term1
term2 ...termn. In that case the references to which these
terms correspond are determined by the tactic. In case of Elim
term (see section 7.7.1) the terms should correspond to all the dependent products in
the type of term while in the case of Apply term only the
dependent products which are not bound in the conclusion of the type
are given.