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:
-
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:
-
ident Not a discriminable equality
occurs when the type of
the specified hypothesis is an equation but does not verify the
expected preconditions.
- identNot an equation occurs when the type of the specified
hypothesis is not an equation.
Variants:
-
Discriminate
It applies to a goal of the form ~
term1=term2 and it is equivalent to:
Unfold not; Intro ident ; Discriminate
ident.
Error messages:
-
goal does not satisfy the expected preconditions.
- Not a discriminable equality
- 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:
-
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:
-
n1 and n2 should not be syntactically equal,
- there must not exist any couple of subterms u and w,
u subterm of n1 and w subterm of n2 ,
placed in the same positions and having different constructors as
head symbols.
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:
-
ident is not a projectable equality
occurs when the type of
the hypothesis id does not verify the preconditions.
- Not an equation occurs when the type of the
hypothesis id is not an equation.
Variants:
-
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:
-
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:
-
Dependent Rewrite <- ident
Analogous to Dependent Rewrite -> but uses the equality from
right to left.