The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Hi all,

Why are there two (seemingly identical) definitions of equivalence relations,

equivalence (Coq.Relations.Relation_Definitions.equivalence)

and

Equivalence (Coq.Classes.RelationClasses.Equivalence)

(the same of course goes for reflexive/Reflexive, transitive/Transitive, ... For your convenience, here are the definitions of, e.g., Reflexive/reflexive and Equivalence/equivalence)

Reflexive =
fun {A : Type} (R : relation A) => forall x : A, R x x
     : forall A : Type, relation A -> Prop

reflexive =
fun (A : Type) (R : relation A) => forall x : A, R x x
     : forall A : Type, relation A -> Prop

Note the sole difference: A is implicit in the definition of Reflexive (the two definitions are definitionally equal, Reflexive = reflexive).

Record Equivalence {A : Type} (R : relation A) : Prop := Build_Equivalence
  { Equivalence_Reflexive : Reflexive R;
    Equivalence_Symmetric : Symmetric R;
    Equivalence_Transitive : Transitive R }

Record equivalence (A : Type) (R : relation A) : Prop := Build_equivalence
  { equiv_refl : reflexive A R;
    equiv_trans : transitive A R;
    equiv_sym : symmetric A R }

(The equality of these two is independent)

Furthermore, if for some reason making the argument implicit warrants a new definition, why are the two not compatible (e.g., some Lemma registered with auto that they are equivalent?)

Kind regards,
jonas