7.8 Equality

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:
  1. No equality here
  2. Failed to progress
    This happens if term1 does not occur in the goal.



Variants:
  1. Rewrite -> term
    Is equivalent to Rewrite term

  2. Rewrite <- term
    Uses the equality term1=term2 from right to left

  3. Rewrite term in ident
    Analogous to Rewrite term but rewriting is done in the hypothesis named ident.

  4. Rewrite -> term in ident
    Behaves as Rewrite term in ident.
  5. 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

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.


Variants:
  1. Replace term1 with term2 in ident This replaces term1 with term2 in the hypothesis named ident, and generates the subgoal term2=term1.
    Error messages:
    1. No such hypothesis

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:
  1. Not a predefined equality
  2. 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.

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