Require Coq.Logic.Eqdep_dec.
Require EquivDec.
Require Import ExtLib.Core.RelDec.
Require Import ExtLib.Tactics.Consider.

Set Implicit Arguments.
Set Strict Implicit.

Section Classes.
  Context {A : Type}.
  Context {dec : EquivDec.EqDec A (@eq A)}.

  Theorem UIP_refl : forall {x : A} (p1 : x = x), p1 = refl_equal _.
(* Goal: forall a : A, @eq (sumbool (@Equivalence.equiv A (@eq A) (@RelationClasses.eq_equivalence A) a a) (@RelationClasses.complement A (@Equivalence.equiv A (@eq A) (@RelationClasses.eq_equivalence A)) a a)) (@EquivDec.equiv_dec A (@eq A) (@RelationClasses.eq_equivalence A) dec a a) (@left (@eq A a a) (@RelationClasses.complement A (@Equivalence.equiv A (@eq A) (@RelationClasses.eq_equivalence A)) a a) (@eq_refl A a)) *)
    intros.
(* Goal: forall (x y : A) (p1 p2 : @eq A x y), @eq (@eq A x y) p1 p2 *)
    eapply Coq.Logic.Eqdep_dec.UIP_dec. apply EquivDec.equiv_dec.
  Qed.

  Theorem UIP_equal : forall {x y : A} (p1 p2 : x = y), p1 = p2.
(* Goal: forall (x y : A) (p1 p2 : @eq A x y), @eq (@eq A x y) p1 p2 *)
    eapply Coq.Logic.Eqdep_dec.UIP_dec. apply EquivDec.equiv_dec.
  Qed.

  Lemma inj_pair2 :
    forall (P:A -> Type) (p:A) (x y:P p),
      existT P p x = existT P p y -> x = y.
  Proof.
(* Goal: forall a : A, @eq (sumbool (@Equivalence.equiv A (@eq A) (@RelationClasses.eq_equivalence A) a a) (@RelationClasses.complement A (@Equivalence.equiv A (@eq A) (@RelationClasses.eq_equivalence A)) a a)) (@EquivDec.equiv_dec A (@eq A) (@RelationClasses.eq_equivalence A) dec a a) (@left (@eq A a a) (@RelationClasses.complement A (@Equivalence.equiv A (@eq A) (@RelationClasses.eq_equivalence A)) a a) (@eq_refl A a)) *)
    intros. eapply Coq.Logic.Eqdep_dec.inj_pair2_eq_dec; auto.
  Qed.

  Theorem equiv_dec_refl_left : forall a, @EquivDec.equiv_dec _ _ _ dec a a = left eq_refl.
  Proof.
(* Goal: forall a : A, @eq (sumbool (@Equivalence.equiv A (@eq A) (@RelationClasses.eq_equivalence A) a a) (@RelationClasses.complement A (@Equivalence.equiv A (@eq A) (@RelationClasses.eq_equivalence A)) a a)) (@EquivDec.equiv_dec A (@eq A) (@RelationClasses.eq_equivalence A) dec a a) (@left (@eq A a a) (@RelationClasses.complement A (@Equivalence.equiv A (@eq A) (@RelationClasses.eq_equivalence A)) a a) (@eq_refl A a)) *)
    intros. destruct (EquivDec.equiv_dec a a); try congruence.
(* Goal: @eq (sumbool (@Equivalence.equiv A (@eq A) (@RelationClasses.eq_equivalence A) a a) (@RelationClasses.complement A (@Equivalence.equiv A (@eq A) (@RelationClasses.eq_equivalence A)) a a)) (@left (@Equivalence.equiv A (@eq A) (@RelationClasses.eq_equivalence A) a a) (@RelationClasses.complement A (@Equivalence.equiv A (@eq A) (@RelationClasses.eq_equivalence A)) a a) e) (@left (@eq A a a) (@RelationClasses.complement A (@Equivalence.equiv A (@eq A) (@RelationClasses.eq_equivalence A)) a a) (@eq_refl A a)) *)
    f_equal. apply UIP_equal.
  Qed.

End Classes.

Section from_rel_dec.
  Variable T : Type.
  Variable RD : RelDec (@eq T).
  Variable RDC : RelDec_Correct RD.

  Global Instance EqDec_RelDec : EquivDec.EqDec T (@eq T).
  Proof.
(* Goal: forall a : A, @eq (sumbool (@Equivalence.equiv A (@eq A) (@RelationClasses.eq_equivalence A) a a) (@RelationClasses.complement A (@Equivalence.equiv A (@eq A) (@RelationClasses.eq_equivalence A)) a a)) (@EquivDec.equiv_dec A (@eq A) (@RelationClasses.eq_equivalence A) dec a a) (@left (@eq A a a) (@RelationClasses.complement A (@Equivalence.equiv A (@eq A) (@RelationClasses.eq_equivalence A)) a a) (@eq_refl A a)) *)
    red; intros.
(* Goal: sumbool (@Equivalence.equiv T (@eq T) (@RelationClasses.eq_equivalence T) x y) (@RelationClasses.complement T (@Equivalence.equiv T (@eq T) (@RelationClasses.eq_equivalence T)) x y) *)
    consider (x ?[ eq ] y); intros; subst; auto.
(* Goal: sumbool (@Equivalence.equiv T (@eq T) (@RelationClasses.eq_equivalence T) y y) (@RelationClasses.complement T (@Equivalence.equiv T (@eq T) (@RelationClasses.eq_equivalence T)) y y) *)
    left. reflexivity.
  Qed.
End from_rel_dec.
