Library Ssreflect.generic_quotient

Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.


Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Reserved Notation "\pi_ Q" (at level 0, format "\pi_ Q").
Reserved Notation "\pi" (at level 0, format "\pi").
Reserved Notation "x == y %[mod_eq e ]" (at level 70, y at next level,
  no associativity, format "'[hv ' x '/' == y '/' %[mod_eq e ] ']'").
Reserved Notation "x = y %[mod_eq e ]" (at level 70, y at next level,
  no associativity, format "'[hv ' x '/' = y '/' %[mod_eq e ] ']'").
Reserved Notation "x != y %[mod_eq e ]" (at level 70, y at next level,
  no associativity, format "'[hv ' x '/' != y '/' %[mod_eq e ] ']'").
Reserved Notation "x <> y %[mod_eq e ]" (at level 70, y at next level,
  no associativity, format "'[hv ' x '/' <> y '/' %[mod_eq e ] ']'").
Reserved Notation "{eq_quot e }" (at level 0, T at level 0,
  format "{eq_quot e }", only parsing).

Delimit Scope quotient_scope with qT.
Local Open Scope quotient_scope.

Section QuotientDef.

Variable T : Type.

Record quot_mixin_of qT := QuotClass {
  quot_repr : qT → T;
  quot_pi : T → qT;
  _ : cancel quot_repr quot_pi
}.

Notation quot_class_of := quot_mixin_of.

Record quotType := QuotTypePack {
  quot_sort :> Type;
  quot_class : quot_class_of quot_sort;
  _ : Type
}.

Definition QuotType_pack qT m := @QuotTypePack qT m qT.

Variable qT : quotType.
Definition pi_of of phant qT := quot_pi (quot_class qT).
Local Notation "\pi" := (pi_of (Phant qT)).
Definition repr_of := quot_repr (quot_class qT).

Lemma repr_ofK : cancel repr_of \pi.
Proof. by rewrite /pi_of /repr_of /=; case:qT⇒ [? []]. Qed.

Definition QuotType_clone (Q : Type) qT cT
  of phant_id (quot_class qT) cT := @QuotTypePack Q cT Q.

End QuotientDef.

Module Type PiSig.
Parameter f : ∀ (T : Type) (qT : quotType T), phant qT → T → qT.
Axiom E : f = pi_of.
End PiSig.

Module Pi : PiSig.
Definition f := pi_of.
Definition E := erefl f.
End Pi.

Module MPi : PiSig.
Definition f := pi_of.
Definition E := erefl f.
End MPi.

Module Type ReprSig.
Parameter f : ∀ (T : Type) (qT : quotType T), qT → T.
Axiom E : f = repr_of.
End ReprSig.

Module Repr : ReprSig.
Definition f := repr_of.
Definition E := erefl f.
End Repr.

Notation repr := Repr.f.
Notation "\pi_ Q" := (@Pi.f _ _ (Phant Q)) : quotient_scope.
Notation "\pi" := (@Pi.f _ _ (Phant _)) (only parsing) : quotient_scope.
Notation "x == y %[mod Q ]" := (\pi_Q x == \pi_Q y) : quotient_scope.
Notation "x = y %[mod Q ]" := (\pi_Q x = \pi_Q y) : quotient_scope.
Notation "x != y %[mod Q ]" := (\pi_Q x != \pi_Q y) : quotient_scope.
Notation "x <> y %[mod Q ]" := (\pi_Q x ≠ \pi_Q y) : quotient_scope.

Local Notation "\mpi" := (@MPi.f _ _ (Phant _)).
Canonical mpi_unlock := Unlockable MPi.E.
Canonical pi_unlock := Unlockable Pi.E.
Canonical repr_unlock := Unlockable Repr.E.

Notation quot_class_of := quot_mixin_of.
Notation QuotType Q m := (@QuotType_pack _ Q m).
Notation "[ 'quotType' 'of' Q ]" := (@QuotType_clone _ Q _ _ id)
 (at level 0, format "[ 'quotType' 'of' Q ]") : form_scope.

Implicit Arguments repr [T qT].
Prenex Implicits repr.

Section QuotTypeTheory.

Variable T : Type.
Variable qT : quotType T.

Lemma reprK : cancel repr \pi_qT.
Proof. by move⇒ x; rewrite !unlock repr_ofK. Qed.

Lemma mpiE : \mpi =1 \pi_qT.
Proof. by move⇒ x; rewrite !unlock. Qed.

Lemma quotW P : (∀ y : T, P (\pi_qT y)) → ∀ x : qT, P x.
Proof. by move⇒ Py x; rewrite -[x]reprK; apply: Py. Qed.

Lemma quotP P : (∀ y : T, repr (\pi_qT y) = y → P (\pi_qT y))
  → ∀ x : qT, P x.
Proof. by move⇒ Py x; rewrite -[x]reprK; apply: Py; rewrite reprK. Qed.

End QuotTypeTheory.


Structure pi_morph T (x : T) := PiMorph {pi_op : T; _ : x = pi_op}.
Lemma piE (T : Type) (x : T) (m : pi_morph x) : pi_op m = x. Proof. by case: m. Qed.

Canonical pi_morph_pi T (qT : quotType T) (x : T) :=
  @PiMorph _ (\pi_qT x) (\pi x) (erefl _).

Implicit Arguments PiMorph [T x pi_op].
Prenex Implicits PiMorph.

Section Morphism.

Variables T U : Type.
Variable (qT : quotType T).
Variable (qU : quotType U).

Variable (f : T → T) (g : T → T → T) (p : T → U) (r : T → T → U).
Variable (fq : qT → qT) (gq : qT → qT → qT) (pq : qT → U) (rq : qT → qT → U).
Variable (h : T → U) (hq : qT → qU).
Hypothesis pi_f : {morph \pi : x / f x >-> fq x}.
Hypothesis pi_g : {morph \pi : x y / g x y >-> gq x y}.
Hypothesis pi_p : {mono \pi : x / p x >-> pq x}.
Hypothesis pi_r : {mono \pi : x y / r x y >-> rq x y}.
Hypothesis pi_h : ∀ (x : T), \pi_qU (h x) = hq (\pi_qT x).
Variables (a b : T) (x : pi_morph (\pi_qT a)) (y : pi_morph (\pi_qT b)).

Lemma pi_morph1 : \pi (f a) = fq (pi_op x). Proof. by rewrite !piE. Qed.
Lemma pi_morph2 : \pi (g a b) = gq (pi_op x) (pi_op y). Proof. by rewrite !piE. Qed.
Lemma pi_mono1 : p a = pq (pi_op x). Proof. by rewrite !piE. Qed.
Lemma pi_mono2 : r a b = rq (pi_op x) (pi_op y). Proof. by rewrite !piE. Qed.
Lemma pi_morph11 : \pi (h a) = hq (pi_op x). Proof. by rewrite !piE. Qed.

End Morphism.

Implicit Arguments pi_morph1 [T qT f fq].
Implicit Arguments pi_morph2 [T qT g gq].
Implicit Arguments pi_mono1 [T U qT p pq].
Implicit Arguments pi_mono2 [T U qT r rq].
Implicit Arguments pi_morph11 [T U qT qU h hq].
Prenex Implicits pi_morph1 pi_morph2 pi_mono1 pi_mono2 pi_morph11.

Notation PiMorph1 pi_f :=
  (fun a (x : pi_morph (\pi a)) ⇒ PiMorph (pi_morph1 pi_f a x)).
Notation PiMorph2 pi_g :=
  (fun a b (x : pi_morph (\pi a)) (y : pi_morph (\pi b))
    ⇒ PiMorph (pi_morph2 pi_g a b x y)).
Notation PiMono1 pi_p :=
  (fun a (x : pi_morph (\pi a)) ⇒ PiMorph (pi_mono1 pi_p a x)).
Notation PiMono2 pi_r :=
  (fun a b (x : pi_morph (\pi a)) (y : pi_morph (\pi b))
    ⇒ PiMorph (pi_mono2 pi_r a b x y)).
Notation PiMorph11 pi_f :=
  (fun a (x : pi_morph (\pi a)) ⇒ PiMorph (pi_morph11 pi_f a x)).

Notation lift_op1 qT f := (locked (fun x : qT ⇒ \pi_qT (f (repr x)) : qT)).
Notation lift_op2 qT g :=
  (locked (fun x y : qT ⇒ \pi_qT (g (repr x) (repr y)) : qT)).
Notation lift_fun1 qT f := (locked (fun x : qT ⇒ f (repr x))).
Notation lift_fun2 qT g := (locked (fun x y : qT ⇒ g (repr x) (repr y))).
Notation lift_op11 qT qU f := (locked (fun x : qT ⇒ \pi_qU (f (repr x)) : qU)).

Notation lift_cst qT x := (locked (\pi_qT x : qT)).
Notation PiConst a := (@PiMorph _ _ a (lock _)).

Notation lift_embed qT e := (locked (fun x ⇒ \pi_qT (e x) : qT)).

Lemma eq_lock T T' e : e =1 (@locked (T → T') (fun x : T ⇒ e x)).
Proof. by rewrite -lock. Qed.
Prenex Implicits eq_lock.

Notation PiEmbed e :=
  (fun x ⇒ @PiMorph _ _ (e x) (eq_lock (fun _ ⇒ \pi _) _)).


Section EqQuotTypeStructure.

Variable T : Type.
Variable eq_quot_op : rel T.

Definition eq_quot_mixin_of (Q : Type) (qc : quot_class_of T Q)
  (ec : Equality.class_of Q) :=
  {mono \pi_(QuotTypePack qc Q) : x y /
   eq_quot_op x y >-> @eq_op (Equality.Pack ec Q) x y}.

Record eq_quot_class_of (Q : Type) : Type := EqQuotClass {
  eq_quot_quot_class :> quot_class_of T Q;
  eq_quot_eq_mixin :> Equality.class_of Q;
  pi_eq_quot_mixin :> eq_quot_mixin_of eq_quot_quot_class eq_quot_eq_mixin
}.

Record eqQuotType : Type := EqQuotTypePack {
  eq_quot_sort :> Type;
  _ : eq_quot_class_of eq_quot_sort;
  _ : Type
}.

Implicit Type eqT : eqQuotType.

Definition eq_quot_class eqT : eq_quot_class_of eqT :=
  let: EqQuotTypePack _ cT _ as qT' := eqT return eq_quot_class_of qT' in cT.

Canonical eqQuotType_eqType eqT := EqType eqT (eq_quot_class eqT).
Canonical eqQuotType_quotType eqT := QuotType eqT (eq_quot_class eqT).

Coercion eqQuotType_eqType : eqQuotType >-> eqType.
Coercion eqQuotType_quotType : eqQuotType >-> quotType.

Definition EqQuotType_pack Q :=
  fun (qT : quotType T) (eT : eqType) qc ec
  of phant_id (quot_class qT) qc & phant_id (Equality.class eT) ec ⇒
    fun m ⇒ EqQuotTypePack (@EqQuotClass Q qc ec m) Q.

Definition EqQuotType_clone (Q : Type) eqT cT
  of phant_id (eq_quot_class eqT) cT := @EqQuotTypePack Q cT Q.

Lemma pi_eq_quot eqT : {mono \pi_eqT : x y / eq_quot_op x y >-> x == y}.
Proof. by case: eqT ⇒ [] ? []. Qed.

Canonical pi_eq_quot_mono eqT := PiMono2 (pi_eq_quot eqT).

End EqQuotTypeStructure.

Notation EqQuotType e Q m := (@EqQuotType_pack _ e Q _ _ _ _ id id m).
Notation "[ 'eqQuotType' e 'of' Q ]" := (@EqQuotType_clone _ e Q _ _ id)
 (at level 0, format "[ 'eqQuotType' e 'of' Q ]") : form_scope.


Module QuotSubType.
Section SubTypeMixin.

Variable T : eqType.
Variable qT : quotType T.

Definition Sub x (px : repr (\pi_qT x) == x) := \pi_qT x.

Lemma qreprK x Px : repr (@Sub x Px) = x.
Proof. by rewrite /Sub (eqP Px). Qed.

Lemma sortPx (x : qT) : repr (\pi_qT (repr x)) == repr x.
Proof. by rewrite !reprK eqxx. Qed.

Lemma sort_Sub (x : qT) : x = Sub (sortPx x).
Proof. by rewrite /Sub reprK. Qed.

Lemma reprP K (PK : ∀ x Px, K (@Sub x Px)) u : K u.
Proof. by rewrite (sort_Sub u); apply: PK. Qed.

Canonical subType := SubType _ _ _ reprP qreprK.
Definition eqMixin := Eval hnf in [eqMixin of qT by <:].

End SubTypeMixin.

Definition choiceMixin (T : choiceType) (qT : quotType T) :=
  Eval hnf in [choiceMixin of qT by <:].

End QuotSubType.

Notation "[ 'subType' 'of' Q 'by' %/ ]" :=
  (SubType Q _ _ QuotSubType.reprP QuotSubType.qreprK)
  (at level 0, format "[ 'subType' 'of' Q 'by' %/ ]") : form_scope.

Notation "[ 'eqMixin' 'of' Q 'by' <:%/ ]" :=
  (@QuotSubType.eqMixin _ _: Equality.class_of Q)
  (at level 0, format "[ 'eqMixin' 'of' Q 'by' <:%/ ]") : form_scope.

Notation "[ 'choiceMixin' 'of' Q 'by' <:%/ ]" :=
  (@QuotSubType.choiceMixin _ _: Choice.mixin_of (seq (seq Q)))
  (at level 0, format "[ 'choiceMixin' 'of' Q 'by' <:%/ ]") : form_scope.


Section EquivRel.

Variable T : Type.

Lemma left_trans (e : rel T) :
  symmetric e → transitive e → left_transitive e.
Proof. by move⇒ s t ? × ?; apply/idP/idP; apply: t; rewrite // s. Qed.

Lemma right_trans (e : rel T) :
  symmetric e → transitive e → right_transitive e.
Proof. by move⇒ s t ? × x; rewrite ![e x _]s; apply: left_trans. Qed.

Record equiv_class_of (equiv : rel T) :=
  EquivClass of reflexive equiv & symmetric equiv & transitive equiv.

Record equiv_rel := EquivRelPack {
  equiv :> rel T;
  _ : equiv_class_of equiv
}.

Variable e : equiv_rel.

Definition equiv_class :=
  let: EquivRelPack _ ce as e' := e return equiv_class_of e' in ce.

Definition equiv_pack (r : rel T) ce of phant_id ce equiv_class :=
  @EquivRelPack r ce.

Lemma equiv_refl x : e x x. Proof. by case: e ⇒ [] ? []. Qed.
Lemma equiv_sym : symmetric e. Proof. by case: e ⇒ [] ? []. Qed.
Lemma equiv_trans : transitive e. Proof. by case: e ⇒ [] ? []. Qed.

Lemma eq_op_trans (T' : eqType) : transitive (@eq_op T').
Proof. by move⇒ x y z; move/eqP->; move/eqP→. Qed.

Lemma equiv_ltrans: left_transitive e.
Proof. by apply: left_trans; [apply: equiv_sym|apply: equiv_trans]. Qed.

Lemma equiv_rtrans: right_transitive e.
Proof. by apply: right_trans; [apply: equiv_sym|apply: equiv_trans]. Qed.

End EquivRel.

Hint Resolve equiv_refl.

Notation EquivRel r er es et := (@EquivRelPack _ r (EquivClass er es et)).
Notation "[ 'equiv_rel' 'of' e ]" := (@equiv_pack _ _ e _ id)
 (at level 0, format "[ 'equiv_rel' 'of' e ]") : form_scope.


Section EncodingModuloRel.

Variables (D E : Type) (ED : E → D) (DE : D → E) (e : rel D).

Record encModRel_class_of (r : rel D) :=
  EncModRelClassPack of (∀ x, r x x → r (ED (DE x)) x) & (r =2 e).

Record encModRel := EncModRelPack {
  enc_mod_rel :> rel D;
  _ : encModRel_class_of enc_mod_rel
}.

Variable r : encModRel.

Definition encModRelClass :=
  let: EncModRelPack _ c as r' := r return encModRel_class_of r' in c.

Definition encModRelP (x : D) : r x x → r (ED (DE x)) x.
Proof. by case: r ⇒ [] ? [] /= he _ /he. Qed.

Definition encModRelE : r =2 e. Proof. by case: r ⇒ [] ? []. Qed.

Definition encoded_equiv : rel E := [rel x y | r (ED x) (ED y)].

End EncodingModuloRel.

Notation EncModRelClass m :=
  (EncModRelClassPack (fun x _ ⇒ m x) (fun _ _ ⇒ erefl _)).
Notation EncModRel r m := (@EncModRelPack _ _ _ _ _ r (EncModRelClass m)).

Section EncodingModuloEquiv.

Variables (D E : Type) (ED : E → D) (DE : D → E) (e : equiv_rel D).
Variable (r : encModRel ED DE e).

Lemma enc_mod_rel_is_equiv : equiv_class_of (enc_mod_rel r).
Proof.
split ⇒ [x|x y|y x z]; rewrite !encModRelE //; first by rewrite equiv_sym.
by move⇒ exy /(equiv_trans exy).
Qed.

Definition enc_mod_rel_equiv_rel := EquivRelPack enc_mod_rel_is_equiv.

Definition encModEquivP (x : D) : r (ED (DE x)) x.
Proof. by rewrite encModRelP ?encModRelE. Qed.

Local Notation e' := (encoded_equiv r).

Lemma encoded_equivE : e' =2 [rel x y | e (ED x) (ED y)].
Proof. by move⇒ x y; rewrite /encoded_equiv /= encModRelE. Qed.
Local Notation e'E := encoded_equivE.

Lemma encoded_equiv_is_equiv : equiv_class_of e'.
Proof.
split ⇒ [x|x y|y x z]; rewrite !e'E //=; first by rewrite equiv_sym.
by move⇒ exy /(equiv_trans exy).
Qed.

Canonical encoded_equiv_equiv_rel := EquivRelPack encoded_equiv_is_equiv.

Lemma encoded_equivP x : e' (DE (ED x)) x.
Proof. by rewrite /encoded_equiv /= encModEquivP. Qed.

End EncodingModuloEquiv.


Module EquivQuot.
Section EquivQuot.

Variables (D : Type) (C : choiceType) (CD : C → D) (DC : D → C).
Variables (eD : equiv_rel D) (encD : encModRel CD DC eD).
Notation eC := (encoded_equiv encD).

Definition canon x := choose (eC x) (x).

Record equivQuotient := EquivQuotient {
  erepr : C;
  _ : (frel canon) erepr erepr
}.

Definition type_of of (phantom (rel _) encD) := equivQuotient.

Lemma canon_id : ∀ x, (invariant canon canon) x.
Proof.
move⇒ x /=; rewrite /canon (@eq_choose _ _ (eC x)).
  by rewrite (@choose_id _ (eC x) _ x) ?chooseP ?equiv_refl.
by move⇒ y; apply: equiv_ltrans; rewrite equiv_sym /= chooseP.
Qed.

Definition pi := locked (fun x ⇒ EquivQuotient (canon_id x)).

Lemma ereprK : cancel erepr pi.
Proof.
unlock pi; case⇒ x hx; move/eqP:(hx)=> hx'.
exact: (@val_inj _ _ [subType for erepr]).
Qed.

Local Notation encDE := (encModRelE encD).
Local Notation encDP := (encModEquivP encD).
Canonical encD_equiv_rel := EquivRelPack (enc_mod_rel_is_equiv encD).

Lemma pi_CD (x y : C) : reflect (pi x = pi y) (eC x y).
Proof.
apply: (iffP idP) ⇒ hxy.
  apply: (can_inj ereprK); unlock pi canon ⇒ /=.
  rewrite -(@eq_choose _ (eC x) (eC y)); last first.
    by move⇒ z; rewrite /eC /=; apply: equiv_ltrans.
  by apply: choose_id; rewrite ?equiv_refl //.
rewrite (equiv_trans (chooseP (equiv_refl _ _))) //=.
move: hxy ⇒ /(f_equal erepr) /=; unlock pi canon ⇒ /= →.
by rewrite equiv_sym /= chooseP.
Qed.

Lemma pi_DC (x y : D) :
  reflect (pi (DC x) = pi (DC y)) (eD x y).
Proof.
apply: (iffP idP)=> hxy.
  apply/pi_CD; rewrite /eC /=.
  by rewrite (equiv_ltrans (encDP _)) (equiv_rtrans (encDP _)) /= encDE.
rewrite -encDE -(equiv_ltrans (encDP _)) -(equiv_rtrans (encDP _)) /=.
exact/pi_CD.
Qed.

Lemma equivQTP : cancel (CD \o erepr) (pi \o DC).
Proof.
move⇒ x /=.
by rewrite (pi_CD _ (erepr x) _) ?ereprK /eC /= ?encDP.
Qed.

Local Notation qT := (type_of (Phantom (rel D) encD)).
Definition quotClass := QuotClass equivQTP.
Canonical quotType := QuotType qT quotClass.

Lemma eqmodP x y : reflect (x = y %[mod qT]) (eD x y).
Proof. by apply: (iffP (pi_DC _ _)); rewrite !unlock. Qed.

Fact eqMixin : Equality.mixin_of qT. Proof. exact: CanEqMixin ereprK. Qed.
Canonical eqType := EqType qT eqMixin.
Definition choiceMixin := CanChoiceMixin ereprK.
Canonical choiceType := ChoiceType qT choiceMixin.

Lemma eqmodE x y : x == y %[mod qT] = eD x y.
Proof. exact: sameP eqP (@eqmodP _ _). Qed.

Canonical eqQuotType := EqQuotType eD qT eqmodE.

End EquivQuot.
End EquivQuot.

Canonical EquivQuot.quotType.
Canonical EquivQuot.eqType.
Canonical EquivQuot.choiceType.
Canonical EquivQuot.eqQuotType.

Notation "{eq_quot e }" :=
(@EquivQuot.type_of _ _ _ _ _ _ (Phantom (rel _) e)) : quotient_scope.
Notation "x == y %[mod_eq r ]" := (x == y %[mod {eq_quot r}]) : quotient_scope.
Notation "x = y %[mod_eq r ]" := (x = y %[mod {eq_quot r}]) : quotient_scope.
Notation "x != y %[mod_eq r ]" := (x != y %[mod {eq_quot r}]) : quotient_scope.
Notation "x <> y %[mod_eq r ]" := (x ≠ y %[mod {eq_quot r}]) : quotient_scope.

Section EquivQuotTheory.

Variables (D : Type) (C : choiceType) (CD : C → D) (DC : D → C).
Variables (eD : equiv_rel D) (encD : encModRel CD DC eD).

Lemma eqmodE x y : x == y %[mod_eq encD] = encD x y.
Proof. by rewrite EquivQuot.eqmodE encModRelE. Qed.

Lemma eqmodP x y : reflect (x = y %[mod_eq encD]) (encD x y).
Proof. by rewrite encModRelE; apply: EquivQuot.eqmodP. Qed.

End EquivQuotTheory.

Implicit Arguments eqmodE [D C DC CD eD encD].
Implicit Arguments eqmodP [D C CD DC eD encD x y].
Prenex Implicits eqmodE eqmodP.



Section DefaultEncodingModuloRel.

Variables (D : choiceType) (r : rel D).

Definition defaultEncModRelClass :=
  @EncModRelClassPack D D id id r r (fun _ rxx ⇒ rxx) (fun _ _ ⇒ erefl _).

Canonical defaultEncModRel := EncModRelPack defaultEncModRelClass.

End DefaultEncodingModuloRel.