7.8 Equality
These tactics use the equality eq:(A:Set)A->A->Prop defined in file Logic.v and the equality
eqT:(A:Type)A->A->Prop defined in file Logic_Type.v (see section 3.1.1). They
are simply written t=u and t==u,
respectively. In the following, the notation t=u will represent either one of these two
equalities.
7.8.1 Rewrite term
This tactic applies to any goal. The type of term
must have the form
(x1:A1) ... (xn:An)term1=term2.
Then Rewrite term replaces every occurrence of
term1 by term2 in the goal. Some of the variables x1 are
solved by unification, and some of the types A1, ...,
An become new subgoals.
Remark: In case the type of
term1 contains occurrences of variables bound in the
type of term, the tactic tries first to find a subterm of the goal
which matches this term in order to find a closed instance term'1
of term1, and then all instances of term'1 will be replaced.
Error messages:
-
No equality here
- Failed to progress
This happens if term1 does not occur in the goal.
Variants:
-
Rewrite -> term
Is equivalent to Rewrite term
- Rewrite <- term
Uses the equality term1=term2 from right to left
- Rewrite term in ident
Analogous to Rewrite term but rewriting is done in the
hypothesis named ident.
- Rewrite -> term in ident
Behaves as Rewrite term in ident.
- Rewrite <- term in ident
Uses the equality term1=term2 from right to left to
rewrite in the hypothesis named ident.
7.8.2 CutRewrite -> term1 = term2
This tactic acts like Replace term1 with term2
(see below).
7.8.3 Replace term1 with term2
This tactic applies to any goal. It replaces all free occurrences of
term1 in the current goal with term2 and generates the
equality term2=term1 as a subgoal. It is equivalent
to Cut term1=term2; Intro Hn; Rewrite Hn;
Clear Hn.
7.8.4 Reflexivity
This tactic applies to a goal which has the form t=u. It checks
that t and u are convertible and then solves the goal.
It is equivalent to Apply refl_equal (or Apply
refl_equalT for an equality in the Typeuniverse).
Error messages:
-
Not a predefined equality
- Impossible to unify ... With ..
7.8.5 Symmetry
This tactic applies to a goal which have form t=u
(resp. t==u) and changes it into u=t (resp. u==t).
7.8.6 Transitivity term
This tactic applies to a goal which have form t=u
and transforms it into the two subgoals
t=term and term=u.