7.9 Equality and inductive sets

We describe in this section some special purpose tactics dealing with equality and inductive sets or types. These tactics use the equalities eq:(A:Set)A->A->Prop defined in file Logic.v and eqT:(A:Type)A->A->Prop defined in file Logic_Type.v (see section 3.1.1). They are written t=u and t==u, respectively. In the following, unless it is stated otherwise, the notation t=u will represent either one of these two equalities.

7.9.1 Decide Equality

This tactic solves a goal of the form (x,y:R){x=y}+{~x=y}, where R is an inductive type such that its constructors do not take proofs or functions as arguments, nor objects in dependent types.


Variants:
  1. Decide Equality term1 term2 .
    Solves a goal of the form {term1=term2}+{~term1=term2}.

7.9.2 Compare term1 term2

This tactic compares two given objects term1 and term2 of an inductive datatype. If G is the current goal, it leaves the sub-goals term1=term2 -> G and ~term1=term2 -> G. The type of term1 and term2 must satisfy the same restrictions as in the tactic Decide Equality.

7.9.3 Discriminate ident

This tactic proves any goal from an absurd hypothesis stating that two structurally different terms of an inductive set are equal. For example, from the hypothesis (S (S O))=(S O) we can derive by absurdity any proposition. Let ident be a hypothesis of type term1 = term2 in the local context, term1 and term2 being elements of an inductive set. To build the proof, the tactic traverses the normal forms1 of term1 and term2 looking for a couple of subterms u and w (u subterm of the normal form of term1 and w subterm of the normal form of term2), placed at the same positions and whose head symbols are two different constructors. If such a couple of subterms exists, then the proof of the current goal is completed, otherwise the tactic fails.


Error messages:
  1. ident Not a discriminable equality occurs when the type of the specified hypothesis is an equation but does not verify the expected preconditions.
  2. identNot an equation occurs when the type of the specified hypothesis is not an equation.

Variants:
  1. Discriminate
    It applies to a goal of the form ~term1=term2 and it is equivalent to: Unfold not; Intro ident ; Discriminate ident.


    Error messages:
    1. goal does not satisfy the expected preconditions.
    2. Not a discriminable equality

  2. Simple Discriminate
    This tactic applies to a goal which has the form ~term1=term2 where term1 and term2 belong to an inductive set and = denotes the equality eq. This tactic proves trivial disequalities such as ~O=(S n) It checks that the head symbols of the head normal forms of term1 and term2 are not the same constructor. When this is the case, the current goal is solved.


    Error messages:
    1. Not a discriminable equality

7.9.4 Injection ident

The Injection tactic is based on the fact that constructors of inductive sets are injections. That means that if c is a constructor of an inductive set, and if (c t1) and (c t2) are two terms that are equal then  t1 and  t2 are equal too.

If ident is an hypothesis of type term1 = term2, then Injection behaves as applying injection as deep as possible to derive the equality of all the subterms of term1 and term2 placed in the same positions. For example, from the hypothesis (S (S n))=(S (S (S m)) we may derive n=(S m). To use this tactic term1 and term2 should be elements of an inductive set and they should be neither explicitly equal, nor structurally different. We mean by this that, if n1 and n2 are their respective normal forms, then: If these conditions are satisfied, then, the tactic derives the equality of all the subterms of term1 and term2 placed in the same positions and puts them as antecedents of the current goal.
Example: Consider the following goal:

Coq < Inductive list : Set  := 
Coq <         nil: list | cons: nat-> list -> list.

Coq < Variable  P : list -> Prop.
Coq < Show.
1 subgoal
  
  l : list
  n : nat
  H : (P nil)
  H0 : (cons n l)=(cons O nil)
  ============================
   (P l)

Coq < Injection H0.
1 subgoal
  
  l : list
  n : nat
  H : (P nil)
  H0 : (cons n l)=(cons O nil)
  ============================
   l=nil->n=O->(P l)

Beware that Injection yields always an equality in a sigma type whenever the injected object has a dependent type.


Error messages:
  1. ident is not a projectable equality occurs when the type of the hypothesis id does not verify the preconditions.
  2. Not an equation occurs when the type of the hypothesis id is not an equation.

Variants:
  1. Injection
    If the current goal is of the form ~term1=term2, the tactic computes the head normal form of the goal and then behaves as the sequence: Unfold not; Intro ident; Injection ident.

    Error message: goal does not satisfy the expected preconditions

7.9.5 Simplify_eq ident

Let ident be the name of an hypothesis of type term1=term2 in the local context. If term1 and term2 are structurally different (in the sense described for the tactic Discriminate), then the tactic Simplify_eq behaves as Discriminate ident otherwise it behaves as Injection ident.


Variants:
  1. Simplify_eq If the current goal has form ~t1=t2, then this tactic does Hnf; Intro ident; Simplify_eq ident.

7.9.6 Dependent Rewrite -> ident

This tactic applies to any goal. If ident has type (existS A B a b)=(existS A B a' b') in the local context (i.e. each term of the equality has a sigma type { a:A  & (B a)}) this tactic rewrites a into a' and b into b' in the current goal. This tactic works even if B is also a sigma type. This kind of equalities between dependent pairs may be derived by the injection and inversion tactics.


Variants:
  1. Dependent Rewrite <- ident
    Analogous to Dependent Rewrite -> but uses the equality from right to left.