Require Export misc_.

Implicit Arguments On.

Module Equiv_.

Export Misc_.

Section Equivalence_Theory.

Variable A:Type; Q:A->A->Prop.

Record Equivalence_Theory : Prop := {
  ax_eqv_refl : (x:A) (Q x x);
  ax_eqv_sym : (x,y:A) (Q x y) -> (Q y x);
  ax_eqv_trans : (x,y,z:A) (Q x y) -> (Q y z) -> (Q x z)
 }.

End Equivalence_Theory.

Record Equivalence [A:Type] : Type := {
  equivalence_pred :> A->A->Prop;
  equivalence_theory :> (Equivalence_Theory equivalence_pred)
 }.

Section Equivalence_Facts.

Variable A:Type; Q:(Equivalence A).

Lemma eqv_refl : (x:A) (Q x x).
Proof.
  Intros; Apply (ax_eqv_refl Q).
Qed.

Lemma eqv_eqT : (x,y:A) x==y -> (Q x y).
Proof.
  NewDestruct 1; Apply eqv_refl.
Qed.

Lemma eqv_sym : (x,y:A) (Q x y) -> (Q y x).
Proof.
  Intros; Apply (ax_eqv_sym Q); Assumption.
Qed.

Lemma eqv_trans : (x,y,z:A) (Q x y) -> (Q y z) -> (Q x z).
Proof.
  Intros; Apply (ax_eqv_trans Q) with y; Assumption.
Qed.

End Equivalence_Facts.

Hints Resolve eqv_refl eqv_eqT eqv_sym eqv_trans.

Definition Compatible [X:Type; Q:(Equivalence X); Y:Type; f:X->Y] :=
  (x,y:X) (Q x y) -> (f x)==(f y).
Hints Unfold Compatible.