Library basis.decidable_set
Require Import Relations.
Module Type S.
Parameter A : Set.
Axiom eq_dec : forall a1 a2 : A, {a1 = a2} + {a1 <> a2}.
End S.
Module Type ES.
Parameter A : Set.
Parameter eq_A : relation A.
Axiom eq_dec : forall a1 a2 : A, {eq_A a1 a2} + {~eq_A a1 a2}.
Axiom eq_proof : equivalence A eq_A.
Add Relation A eq_A
reflexivity proved by (equiv_refl _ _ eq_proof)
symmetry proved by (equiv_sym _ _ eq_proof)
transitivity proved by (equiv_trans _ _ eq_proof) as EQA.
End ES.
Module Convert (DS : S) :
ES with Definition A := DS.A
with Definition eq_A := @eq DS.A.
Definition A := DS.A.
Definition eq_A := @eq A.
Lemma eq_dec : forall a1 a2 : A, {eq_A a1 a2} + {~eq_A a1 a2}.
Proof.
unfold eq_A; apply DS.eq_dec.
Defined.
Lemma eq_proof : equivalence A eq_A.
Proof.
unfold eq_A; split.
intro a; reflexivity.
intros a1 a2 a3 H1 H2; transitivity a2; trivial.
intros a1 a2 H; symmetry; trivial.
Qed.
Add Relation A eq_A
reflexivity proved by (equiv_refl _ _ eq_proof)
symmetry proved by (equiv_sym _ _ eq_proof)
transitivity proved by (equiv_trans _ _ eq_proof) as EQA.
End Convert.