quotient

Quotient.v

Set Primitive Projections.

From Coq Require
  Program
  Logic.ProofIrrelevance
  Logic.PropExtensionality
  Logic.FunctionalExtensionality
  Logic.Epsilon
  Relations.Relation_Operators.

Import ProofIrrelevance.

Definition subst {A : Type} (B : A -> Type) {a a'} (p : a = a') (b : B a) : B a' :=
  match p with
  | eq_refl => b
  end.

Arguments subst {_} _ {_ _} _ _.

Lemma subst_trans {A : Type} (B : A -> Type) {a1 a2 a3} (p : a1 = a2) (q : a2 = a3) (b : B a1) :
  subst B (eq_trans p q) b = subst B q (subst B p b).
Proof.
  destruct q. reflexivity.
Defined.

Definition depeq_flip {A : Type} (P : A -> Type) {x y} (p : x = y)
  : forall {u : P x} {v : P y}, subst P p u = v -> u = subst P (eq_sym p) v :=
  match p with
  | eq_refl => fun u v H => H
  end.

Definition depeq_coflip {A : Type} (P : A -> Type) {x y} (p : y = x)
  : forall {u : P x} {v : P y}, u = subst P p v -> subst P (eq_sym p) u = v :=
  match p with
  | eq_refl => fun u v H => H
  end.

Definition eq_sigT_intro {X : Type} (P : X -> Type) {x1 x2 : X} (p : x1 = x2)
  : forall {H1 : P x1} {H2 : P x2}, subst P p H1 = H2 -> existT P x1 H1 = existT P x2 H2 :=
  match p with
  | eq_refl => fun H1 H2 e => f_equal (existT P x1) e
  end.

Definition eq_sigT_projT1 {X : Type} (P : X -> Type) {u1 u2 : {x & P x}}
  : u1 = u2 -> projT1 u1 = projT1 u2 :=
  fun p => f_equal (fun x => projT1 x) p.

Definition eq_sigT_projT2 {X : Type} (P : X -> Type) {u1 u2 : {x & P x}}
  : forall (p : u1 = u2), subst P (eq_sigT_projT1 P p) (projT2 u1) = projT2 u2 :=
  fun p =>
    match p with
    | eq_refl => eq_refl
    end.

Definition eq_sigT_projT2' {X : Type} (P : X -> Type) {u1 u2 : {x & P x}}
  : forall (p : u1 = u2), projT2 u1 = subst P (eq_sym (eq_sigT_projT1 P p)) (projT2 u2) :=
  fun p =>
    match p with
    | eq_refl => eq_refl
    end.

Definition eq_sig_intro {X : Type} (P : X -> Prop) {x1 x2 : X} (p : x1 = x2)
  : forall {H1 : P x1} {H2 : P x2}, subst P p H1 = H2 -> exist P x1 H1 = exist P x2 H2 :=
  match p with
  | eq_refl => fun H1 H2 e => f_equal (exist P x1) e
  end.

Lemma eq_sig_intro' {X : Type} (P : X -> Prop) {x1 x2 : X} (p : x1 = x2)
  : forall {H1 : P x1} {H2 : P x2}, exist P x1 H1 = exist P x2 H2.
Proof.
  intros. eapply (eq_sig_intro P p). eapply proof_irrelevance.
Qed.

(* This definition of quotient is well-behaved in the presence of PI and UIP *)
Module UniversalQuotient.

  Record Quotient (A : Type) (R : A -> A -> Prop) : Type :=
    { Quo         : Type
    ; class       : A -> Quo
    ; class_eq    : forall x y, R x y -> class x = class y
    ; rec         : forall (X : Type) (f : A -> X) (f_cong : forall x y, R x y -> f x = f y), Quo -> X
    ; rec_compute : forall (X : Type) (f : A -> X) (f_cong : forall x y, R x y -> f x = f y), forall x, rec X f f_cong (class x) = f x
    ; rec_unique  : forall (X : Type) (f : A -> X) (f_cong : forall x y, R x y -> f x = f y), forall rec', (forall x, rec' (class x) = f x) -> (forall cx, rec' cx = rec X f f_cong cx)
    }.

  Arguments Quotient _ _ : clear implicits.
  Arguments Quo {_ _}.
  Arguments class {_ _}.
  Arguments class_eq {_ _}.
  Arguments rec {_ _}.
  Arguments rec_compute {_ _}.
  Arguments rec_unique {_ _}.

  Section INDUCTION.
  
    Context {A : Type}.
    Context {R : A -> A -> Prop}.
    Context (Q : Quotient A R).
  
    Lemma elim_aux
      (X : Type)
      (f : A -> X)
      (f_cong : forall x y, R x y -> f x = f y)
      (p : X -> Q.(Quo))
      (f_respect : forall x, p (f x) = Q.(class) x)
      : forall cx, p (Q.(rec) X f f_cong cx) = cx.
    Proof.
      intro cx.
      transitivity (Q.(rec) Q.(Quo) Q.(class) Q.(class_eq) cx); [|symmetry].
      { exact (Q.(rec_unique)
                    Q.(Quo)
                    Q.(class)
                    Q.(class_eq)
                    (fun cx => p (Q.(rec) X f f_cong cx))
                    (fun x => eq_trans (f_equal p (Q.(rec_compute) X f f_cong x)) (f_respect x))
                    cx).
      }
      { exact (Q.(rec_unique)
                    Q.(Quo)
                    Q.(class)
                    Q.(class_eq)
                    (fun cx => cx)
                    (fun x => eq_refl)
                    cx).
      }
    Defined.
  
    Lemma elim
      (P : Q.(Quo) -> Type)
      (f : forall x, P (Q.(class) x))
      (f_cong : forall x y (r : R x y), subst P (Q.(class_eq) x y r) (f x) = f y)
      : forall cx, P cx.
    Proof.
      pose (f' := fun x => existT P (Q.(class) x) (f x)).
      pose proof (f'_cong :=
                    fun x y r => eq_sigT_intro
                                P
                                (Q.(class_eq) x y r)
                                (f_cong x y r)).
      pose proof (g := fun cx => projT2 (Q.(rec) {cx & P cx} f' f'_cong cx)).
      pose proof (H := elim_aux {cx & P cx} f' f'_cong (fun x => projT1 x) (fun x => eq_refl)).
      simpl in *.
      exact (fun cx => subst P (H cx) (g cx)).
    Defined.
  
    Lemma elim_compute
      (P : Q.(Quo) -> Type)
      (f : forall x, P (Q.(class) x))
      (f_cong : forall x y (r : R x y), subst P (Q.(class_eq) x y r) (f x) = f y)
      : forall x, elim P f f_cong (Q.(class) x) = f x.
    Proof.
      intro x. unfold elim. unfold elim_aux. simpl in *.
      pose (f' := fun x => existT P (Q.(class) x) (f x)); fold f'.
      pose (f'_cong := fun x y r => eq_sigT_intro P (Q.(class_eq) x y r) (f_cong x y r)); fold f'_cong.
      rewrite (eq_sigT_projT2' P (Q.(rec_compute) {cx & P cx} f' f'_cong x)); simpl.
      rewrite <- subst_trans.
      match goal with |- ?lhs = _ => change (lhs = subst P eq_refl (f x)) end.
      f_equal. eapply proof_irrelevance.
    Qed.
  
    Lemma ind
      (P : Q.(Quo) -> Prop)
      (f : forall x, P (Q.(class) x))
      : forall cx, P cx.
    Proof.
      assert (f_cong : forall x y (r : R x y), subst P (Q.(class_eq) x y r) (f x) = f y).
      { intros. eapply proof_irrelevance. }
      exact (elim P f f_cong).
    Defined.
  
    Lemma ind_compute
      (P : Q.(Quo) -> Prop)
      (f : forall x, P (Q.(class) x))
      : forall x, ind P f (Q.(class) x) = f x.
    Proof.
      eapply elim_compute.
    Qed.
  
  End INDUCTION.

End UniversalQuotient.

Module EpsilonQuotient. Section EpsilonQuotient.

 Import
   PropExtensionality
   FunctionalExtensionality
   Relation_Operators
   Epsilon.

  Notation ec R := (clos_refl_sym_trans_1n _ R).

  Context (A : Type).
  Context (R : A -> A -> Prop).

  Definition Quo : Type := {cx : A -> Prop | exists x, ec R x = cx }.

  Definition class : A -> Quo :=
    fun x => exist _ (ec R x) (ex_intro _ x eq_refl).

  Lemma class_eq : forall x1 x2, R x1 x2 -> class x1 = class x2.
  Proof.
    intros x1 x2 r.
    eapply eq_sig_intro'.
    eapply functional_extensionality; intro y.
    eapply propositional_extensionality.
    split.
    - intro H. econstructor.
      + right. apply r.
      + eauto.
    - intro H. econstructor.
      + left. apply r.
      + eauto.
  Qed.

  Lemma class_nonempty : forall (cx : Quo), exists x, proj1_sig cx x.
  Proof.
    intros [cx [x H]]. simpl. subst.
    exists x. econstructor.
  Qed.

  Definition repr : Quo -> A :=
    fun cx => proj1_sig (constructive_indefinite_description (proj1_sig cx) (class_nonempty cx)).

  Definition rec : forall (X : Type) (f : A -> X) (f_cong : forall x y, R x y -> f x = f y), Quo -> X :=
    fun X f f_cong cx => f (repr cx).

  Lemma rec_compute
    (X : Type)
    (f : A -> X)
    (f_cong : forall x y, R x y -> f x = f y)
    : forall x, rec X f f_cong (class x) = f x.
  Proof.
    intros x. unfold rec, repr; simpl.
    generalize (constructive_indefinite_description (ec R x) (class_nonempty (class x))).
    intros [y r]; simpl.
    induction r.
    - reflexivity.
    - transitivity (f y).
      + eauto.
      + destruct H.
        * symmetry. eapply f_cong. eapply H.
        * eapply f_cong. eapply H.
  Qed.

  Lemma rec_unique
    (X : Type)
    (f : A -> X)
    (f_cong : forall x y, R x y -> f x = f y)
    : forall rec', (forall x, rec' (class x) = f x) -> (forall cx, rec' cx = rec X f f_cong cx).
  Proof.
    intros rec' rec'_compute.
    intros cx. destruct cx as [cx [x H]]; subst.
    change (rec' (class x) = rec X f f_cong (class x)).
    rewrite rec'_compute.
    rewrite rec_compute.
    reflexivity.
  Qed.

  Definition Quotient : UniversalQuotient.Quotient A R :=
    {|
      UniversalQuotient.Quo         := Quo;
      UniversalQuotient.class       := class;
      UniversalQuotient.class_eq    := class_eq;
      UniversalQuotient.rec         := rec;
      UniversalQuotient.rec_compute := rec_compute;
      UniversalQuotient.rec_unique  := rec_unique;
    |}.

End EpsilonQuotient. End EpsilonQuotient.

Axiom quotient_type : forall A R, UniversalQuotient.Quotient A R.

Section QUOTIENT.

  Definition Quo (A : Type) (R : A -> A -> Prop) : Type :=
    (quotient_type A R).(UniversalQuotient.Quo).

  Context {A : Type}.
  Context {R : A -> A -> Prop}.

  Definition class : A -> Quo A R :=
    (quotient_type A R).(UniversalQuotient.class).

  Definition class_eq : forall x y, R x y -> class x = class y :=
    (quotient_type A R).(UniversalQuotient.class_eq).
    
  Definition rec : forall (X : Type) (f : A -> X) (f_cong : forall x y, R x y -> f x = f y), Quo A R -> X :=
    (quotient_type A R).(UniversalQuotient.rec).

  Definition rec_compute : forall (X : Type) (f : A -> X) (f_cong : forall x y, R x y -> f x = f y), forall x, rec X f f_cong (class x) = f x :=
    (quotient_type A R).(UniversalQuotient.rec_compute).

  Definition rec_unique  : forall (X : Type) (f : A -> X) (f_cong : forall x y, R x y -> f x = f y), forall rec', (forall x, rec' (class x) = f x) -> (forall cx, rec' cx = rec X f f_cong cx) :=
    (quotient_type A R).(UniversalQuotient.rec_unique).

  Definition elim_aux
      (X : Type)
      (f : A -> X)
      (f_cong : forall x y, R x y -> f x = f y)
      (p : X -> Quo A R)
      (f_respect : forall x, p (f x) = class x)
    : forall cx, p (rec X f f_cong cx) = cx :=
    UniversalQuotient.elim_aux (quotient_type A R) X f f_cong p f_respect.

  Definition elim
    (P : Quo A R -> Type)
    (f : forall x, P (class x))
    (f_cong : forall x y (r : R x y), subst P (class_eq x y r) (f x) = f y)
    : forall cx, P cx :=
    UniversalQuotient.elim (quotient_type A R) P f f_cong.

  Definition elim_compute
    (P : Quo A R -> Type)
    (f : forall x, P (class x))
    (f_cong : forall x y (r : R x y), subst P (class_eq x y r) (f x) = f y)
    : forall x, elim P f f_cong (class x) = f x :=
    UniversalQuotient.elim_compute (quotient_type A R) P f f_cong.
  
  Definition ind
    (P : Quo A R -> Prop)
    (f : forall x, P (class x))
    : forall cx, P cx :=
    UniversalQuotient.ind (quotient_type A R) P f.
  
  Definition ind_compute
    (P : Quo A R -> Prop)
    (f : forall x, P (class x))
    : forall x, ind P f (class x) = f x :=
    UniversalQuotient.ind_compute (quotient_type A R) P f.

End QUOTIENT.