Set Implicit Arguments.

Require Import LogicUtil.
Require Import Setoid.

Require Export EqdepFacts.
Require Export Eqdep_dec.

Section eq_dep.

Variables (U : Type) (eq_dec : ∀ x y : U, {x=y}+{¬x=y}).

Lemma eq_rect_eq : ∀ (p : U) Q x h, x = eq_rect p Q x p h.

Proof.
exact (eq_rect_eq_dec eq_dec).
Qed.

Lemma eq_dep_eq : ∀ P (p : U) x y, eq_dep U P p x p y → x = y.

Proof.
exact (eq_rect_eq__eq_dep_eq U eq_rect_eq).
Qed.

Lemma UIP : ∀ (x y : U) (p1 p2 : x = y), p1 = p2.

Proof.
exact (eq_dep_eq__UIP U eq_dep_eq).
Qed.

Lemma UIP_refl : ∀ (x : U) (p : x = x), p = refl_equal x.

Proof.
exact (UIP__UIP_refl U UIP).
Qed.

Lemma Streicher_K :
  ∀ (x : U) (P : x = x → Prop), P (refl_equal x) → ∀ p, P p.

Proof.
exact (K_dec_type eq_dec).
Qed.

Lemma inj_pairT2 : ∀ P (p : U) x y, existT P p x = existT P p y → x = y.

Proof.
exact (eq_dep_eq__inj_pairT2 U eq_dep_eq).
Qed.

Lemma inj_pairP2 :
  ∀ P (x : U) p q, ex_intro P x p = ex_intro P x q → p = q.

Proof.
intros. apply inj_right_pair with (A:=U).
intros x0 y0; case (eq_dec x0 y0); [left|right]; assumption.
assumption.
Qed.

End eq_dep.

Implicit Arguments UIP_refl [U x].

Section beq.

Variable A : Type.
Variable beq : A → A → bool.
Variable beq_ok : ∀ x y, beq x y = true ↔ x = y.

Lemma beq_refl : ∀ x, beq x x = true.

Proof.
intro. ded (beq_ok x x). rewrite H. refl.
Qed.

Require Import BoolUtil.

Lemma beq_ko : ∀ x y, beq x y = false ↔ x ≠ y.

Proof.
intros. destruct (beq_ok x y). case_eq (beq x y); intuition.
rewrite H1 in H4. discriminate.
Defined.

Lemma dec_beq : ∀ x y : A, {x=y}+{¬x=y}.

Proof.
intros. ded (beq_ok x y). case_eq (beq x y); intuition. rewrite beq_ko in H0.
auto.
Defined.

Lemma beq_com : ∀ x y, beq x y = beq y x.

Proof.
intros. case_eq (beq x y); symmetry.
rewrite beq_ok. symmetry. rewrite <- beq_ok. assumption.
rewrite beq_ko. cut (x≠y). auto. rewrite <- beq_ko. assumption.
Qed.

Lemma beq_sym : ∀ x y, beq x y = true → beq y x = true.

Proof.
intros. rewrite beq_com. exact H.
Qed.

Lemma beq_trans : ∀ x y z,
  beq x y = true → beq y z = true → beq x z = true.

Proof.
intros. rewrite beq_ok in H. rewrite beq_ok in H0.
assert (x = z). apply trans_eq with y; assumption.
rewrite beq_ok. exact H1.
Qed.

End beq.

Implicit Arguments beq_refl [A beq].
Implicit Arguments dec_beq [A beq].
Implicit Arguments beq_com [A beq].
Implicit Arguments beq_ko [A beq].

Ltac case_beq beq_ok e := coq_case_eq e;
  [let h := fresh in intro h; rewrite beq_ok in h;
    match type of h with ?x = ?y ⇒ subst y end
    | intro].

Section eq_dec.

Variable A : Type.
Variable eq_dec : ∀ x y : A, {x=y}+{¬x=y}.

Definition beq_dec x y :=
  match eq_dec x y with
    | left _ ⇒ true
    | right _ ⇒ false
  end.

Lemma beq_dec_ok : ∀ x y, beq_dec x y = true ↔ x = y.

Proof.
intros. unfold beq_dec. case (eq_dec x y); intuition. discriminate.
Qed.

Lemma beq_dec_refl : ∀ x, beq_dec x x = true.

Proof.
intro. unfold beq_dec. case (eq_dec x x); intros. refl. irrefl.
Qed.

Lemma beq_dec_sym : ∀ x y, beq_dec x y = beq_dec y x.

Proof.
intros. unfold beq_dec. case (eq_dec x y); case (eq_dec y x); intros;
(refl || irrefl).
Qed.

Lemma beq_dec_trans : ∀ x y z,
  implb (beq_dec x y && beq_dec y z) (beq_dec x z) = true.

Proof.
intros. unfold beq_dec.
case (eq_dec x y); case (eq_dec y z); case (eq_dec x z);
intros; (refl || (irrefl || idtac)).
Qed.

Lemma beq_dec_ko : ∀ x y, beq_dec x y = false ↔ x ≠ y.

Proof.
intros. case (eq_dec x y); case_eq (beq_dec x y); intuition.
subst y. rewrite beq_dec_refl in H. discriminate.
rewrite beq_dec_ok in H. contradiction.
Qed.

End eq_dec.

Record Bool_eq_type : Type := mkBool_eq_type {
  bet_type :> Type;
  bet_eq : bet_type → bet_type → bool;
  bet_ok : ∀ x y, bet_eq x y = true ↔ x = y
}.