The Coq mailing list

[Brian Aydemir <baydemir AT cis.upenn.edu>]

Hi all,

I'm curious why some things work and why others don't when using the
Equivalence type class (from Coq.Classes.Equivalence).  My typical uses
of the class arise indirectly, via EqDec, so I'll give a simple example
using EqDec.

<<
Require Import Coq.Classes.EquivDec.

Lemma test : forall `(EqDec A eq) (x y : A), y = x \/ y <> x.
Proof.
  intros ? ? ? x y.
  destruct (x == y) as [J | J].
>>

At this point, the first subgoal looks as follows

<<
  A : Type
  equiv0 : Equivalence eq
  H : EqDec A eq
  x : A
  y : A
  J : x === y
  ============================
   y = x \/ y <> x
>>

[rewrite J] works, which is great.
[left; congruence] works, which is also great.
[subst x] fails, which is not so great.

Is there a simple explanation for the behavior of these tactics in this
particular situation?  When the equivalence relation I work with is
[eq], as it is in the above example, it would be nice if "===" was
treated the same as "=".

Thanks,
Brian