Require Import Base.

Section EQDEP.

Variable X : Type.
Variable P : X -> Prop.

(* This version is missing in the Coq standard library! *)
Lemma eq_dep_dec_sig (x y : X) (h : P x) (h' : P y) (p : x = y)
  (q : match p with eq_refl => h end = h') :
  exist P x h = exist P y h'.
Proof. now destruct p,q. Qed.

End EQDEP.

Section Quotient.

Variable X : Type.
Variable R : X -> X -> Prop.
Variable r_dec : forall x y, dec (R x y).

Variable r_refl : forall x, R x x.
Variable r_sym : forall x y, R x y -> R y x.
Variable r_trans : 
         forall x y z, R x y -> R y z -> R x z.

Variable f : X -> nat.
Variable f_rev : nat -> X.
Variable f_f_rev_id : forall x y, R x y -> f x = f y.
Variable R_f_rev : forall x, R x (f_rev (f x)).

Definition eta n := f (f_rev n).

Definition quot := 
   {n| n = eta n}.

Definition repr (q : quot) := let (n,_) := q in f_rev n.

Lemma f_repr x : f x = eta (f x).
Proof.
  unfold eta. auto. 
Qed.

Definition norm (x : X) : quot := exist (fun n => n = eta n) (f x) (f_repr x).

Definition norm_corr : forall x : X, R x (repr (norm x)).		
Proof.
  intros. unfold norm. simpl. auto.
Qed.

Lemma R_repr x y : R x y <-> repr (norm x) = repr (norm y).
Proof.
  split; intros.
  - unfold norm. simpl. f_equal. auto.
  - unfold norm in H; simpl in *. eapply r_trans.
    + apply R_f_rev.
    + rewrite H. apply r_sym. apply R_f_rev. 
Qed.

Lemma repr_char x y : repr (norm x) = repr (norm y) <-> norm x = norm y.
Proof.
  unfold norm; split; intros; simpl in *.
  - assert (R x y). { apply R_repr; auto. }
    assert (f x = f y). { auto. } apply eq_dep_dec_sig with (p := H1).
    apply UIP_nat.
  - injection H; intros. rewrite H0. reflexivity.
Qed.

Theorem R_repr_iff x y : R x y <-> norm x = norm y.
Proof.
  split; intros.
  - apply repr_char, R_repr; auto.
  - apply R_repr, repr_char; auto.
Qed.

Lemma quot_R_eq (a b : quot) : R (repr a) (repr b) <-> a = b.
Proof.
  split; intros.
  - unfold repr in H. unfold quot in *. destruct a, b.
    apply R_repr_iff in H. unfold norm in H; simpl in H. injection H. intros. 
    unfold eta in *. assert (x = x0) by congruence. 
    apply eq_dep_dec_sig with (p := H1). apply UIP_nat.
  - rewrite H. apply r_refl.
Qed.

End Quotient.