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:
  1. 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:
  1. 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:
  1. Cannot move ident1 after ident2: it occurs in ident2
  2. 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:
  1. No product even after head-reduction

Warning: : ident1 is already used; changed to ident2


Variants:
  1. Intros
    Repeats Intro until it meets the head-constant. It never reduces head-constants and it never fails.

  2. 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.

  3. 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.
  4. 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
  5. 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.

  6. Intro after ident
    Applies Intro but puts the introduced hypothesis after the hypothesis ident in the hypotheses.


    Error messages:
    1. No product even after head-reduction
    2. No such hypothesis : ident

  7. 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:
    1. No product even after head-reduction
    2. 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:
  1. 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).

  2. 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:
  1. 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

  2. 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).

  3. 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.

  4. 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:
  1. Let ident0 := term in ident1

    This behaves the same but substitutes term not in the goal but in the hypothesis named ident1.

  2. 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.

  3. 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:
  1. 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:
  1. Generalize term1 ... termn
    Is equivalent to Generalize termn; ... ; Generalize term1. Note that the sequence of termi's are processed from n to 1.

  2. 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:
  1. convert-concl rule passed non-converting term

Variants:
  1. 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.