7.7 Eliminations (Induction and Case Analysis)

Elimination tactics are useful to prove statements by induction or case analysis. Indeed, they make use of the elimination (or induction) principles generated with inductive definitions (see section 4.5).

7.7.1 `Elim` term

This tactic applies to any goal. The type of the argument term must be an inductive constant. Then according to the type of the goal, the tactic Elim chooses the right destructor and applies it (as in the case of the Apply tactic). For instance, assume that our proof context contains n:nat, assume that our current goal is T of type Prop, then Elim n is equivalent to Apply nat_ind with n:=n.

Error messages:

Not an inductive product
Cannot refine to conclusions with meta-variables
As Elim uses Apply, see section 7.3.4 and the variant Elim ...with ... below.

Variants:

Elim term also works when the type of term starts with products and the head symbol is an inductive definition. In that case the tactic tries both to find an object in the inductive definition and to use this inductive definition for elimination. In case of non-dependent products in the type, subgoals are generated corresponding to the hypotheses. In the case of dependent products, the tactic will try to find an instance for which the elimination lemma applies.
Elim term with term₁ ...term_n
Allows the user to give explicitly the values for dependent premises of the elimination schema. All arguments must be given.

Error message: Not the right number of dependent arguments
Elim term with ref₁ := term₁ ...ref_n:=term_n
Provides also Elim with values for instantiating premises by associating explicitly variables (or non dependent products) with their intended instance.
Elim term₁ using term₂
Allows the user to give explicitly an elimination predicate term₂ which is not the standard one for the underlying inductive type of term₁. Each of the term₁ and term₂ is either a simple term or a term with a bindings list (see 7.3.7).
ElimType form
The argument form must be inductively defined. ElimType I is equivalent to Cut I. Intro Hn; Elim Hn; Clear Hn Therefore the hypothesis Hn will not appear in the context(s) of the subgoal(s).
Conversely, if t is a term of (inductive) type I and which does not occur in the goal then Elim t is equivalent to ElimType I; 2: Exact t.

Error message: Impossible to unify ...with ...
Arises when form needs to be applied to parameters.
Induction ident
Is equivalent to Intros until ident; Pattern ident; Elimident
Induction num
Is analogous to Induction ident but for the num-th non-dependent premise of the goal.

7.7.2 `Case` term

The tactic Case is used to perform case analysis without recursion. The type of term must be inductively defined.

Variants:

Case term with term₁ ...term_n
Analogous to Elim ...with above.
Destruct ident
Is equivalent to the tactical Intros Until ident; Case ident.
Destruct num
Is equivalent to Destruct ident but for the num-th non dependent premises of the goal.

7.7.3 `Intros` pattern

The tactic Intros applied to a pattern performs both introduction of variables and case analysis in order to give names to components of an hypothesis.

A pattern is either:

a variable
a list of patterns: p₁ ... p_n
a disjunction of patterns: [p₁ | ... | p_n ]
a conjunction of patterns: ( p₁ , ... , p_n )

The behavior of Intros is defined inductively over the structure of the pattern given as argument:

introduction on a variable behaves like described in 7.3.3;
introduction over a list of patterns p₁ ... p_n is equivalent to the sequence of introductions over the patterns namely: Intros p₁;...; Intros p_n, the goal should start with at least n products;
introduction over a disjunction of patterns [p₁ | ... | p_n], it introduces a new variable X, its type should be an inductive definition with n constructors, then it performs a case analysis over X (which generates n subgoals), it clears X and performs on each generated subgoals the corresponding Intros p_i tactic;
introduction over a conjunction of patterns (p₁,...,p_n), it introduces a new variable X, its type should be an inductive definition with 1 constructor with (at least) n arguments, then it performs a case analysis over X (which generates 1 subgoal with at least n products), it clears X and performs an introduction over the list of patterns p₁ ... p_n.

Coq < Lemma intros_test : (A,B,C:Prop)(A\/(B/\C))->(A->C)->C.
1 subgoal

  ============================
   (A,B,C:Prop)A\/B/\C->(A->C)->C

Coq < Intros A B C [a|(b,c)] f.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  a : A
  f : A->C
  ============================
   C
subgoal 2 is:
C

Coq < Apply (f a).
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  b : B
  c : C
  f : A->C
  ============================
   C

Coq < Proof c.
intros_test is defined

7.7.4 `Double Induction` num`₁` num`₂`

This tactic applies to any goal. If the num₁th and num₂th premises of the goal have an inductive type, then this tactic performs double induction on these premises. For instance, if the current goal is (n,m:nat)(P n m) then, Double Induction 1 2 yields the four cases with their respective inductive hypothesis. In particular the case for (P (S n) (S m)) with the inductive hypothesis about both n and m.

Remark: This tactic is not automatically loaded; it is available by doing Require Double.

7.7.5 `Decompose [` ident `...`idents `]` term

This tactic allows to recursively decompose a complex proposition in order to obtain atomic ones. Example:

Coq < Lemma ex1: (A,B,C:Prop)(A/\B/\C \/ B/\C \/ C/\A) -> C.
1 subgoal

  ============================
   (A,B,C:Prop)A/\B/\C\/B/\C\/C/\A->C

Coq < Intros A B C H; Decompose [and or] H; Assumption.
Subtree proved!

Coq < Qed.

Variants:

Decompose Sum term This decomposes sum types (like or).
Decompose Record term This decomposes record types (inductive types with one constructor, like and and exists and those defined with the Record macro, see p. X).

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