7.3 Basics

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


Error messages:
  1. Intro needs a product



Variants:
  1. Intros
    It is equivalent to Repeat Intro, except that it fails when the goal is not a product.
  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

7.3.4 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.8, 7.5.1).

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

  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.5 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.6 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 ident1 ...identn
    Is equivalent to Generalize identn; ...; Generalize ident1. Note that the sequence of identi's are processed from n to 1.

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

Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.1.2.2.html at 8/10/98