Module FormalML.utils.quotient_space




Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Logic.PropExtensionality.
Require Import Coq.Logic.Description.
Require Import Coq.Relations.Relation_Definitions.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Unicode.Utf8.
Require Import Coq.Classes.Morphisms.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Quotients are crucial in mathematical practice, and it is a shame that they are not available in Coq's standard library. There was a recent discussion on the Coq GitHub page on this issue and the consequences of implementing quotients like #<a href=https://leanprover.github.io/>Lean</a># does, where the eliminator for function types has a reduction rule that breaks pleasant metatheoretic properties such as subject reduction. In this post, we are going to define quotients in Coq with three standard axioms:


As far as axioms go, these three are relatively harmless. In particular, they are valid in any #<a href=https://en.wikipedia.org/wiki/ToposElementary_topoi_(topoi_in_logic)>elementary topos</a>#, which are generally regarded as a good universe for doing constructive, higher-order reasoning. (Naturally, adding axioms in type theory does not come for free: since they have no useful reduction behavior, our quotients won't compute.)

Section Quotient.

We define the quotient of T by an equivalence relation R as usual: it is the type of equivalence classes of R.

  Context {T : Type} (R : relation T) {RP : Equivalence R}.

  Unset Elimination Schemes.
  Record quot := Quot_ {
                     quot_class : T → Prop;
                     quot_classP : ∃ x, quot_class = R x;
                   }.
  Set Elimination Schemes.

The projection into the quotient is given by the Quot constructor below, which maps x to its equivalence class R x. This definition satisfies the usual properties: Quot x = Quot y if and only if R x y. The "if" direction requires the principle of proof irrelevance, which is a consequence of propositional extensionality.

  Definition Quot (x : T) : quot :=
    @Quot_ (R x) (ex_intro _ x (eq_refl _)).

  Lemma Quot_inj x y : Quot x = Quot y → R x y.
  Proof.

  Lemma eq_Quot x y : R x y → Quot x = Quot y.
  Proof.

We can also show that Quot is surjective by extracting the witness in the existential.
  Lemma Quot_inv q : ∃ x, q = Quot x.
  Proof.

Unique choice comes into play when defining the elimination principles for the quotient. In its usual non-dependent form, the principle says that we can lift a function f : T → S to another function quot → S provided that f is constant on equivalence classes. We define a more general dependently typed version, which allows in particular to prove a property S q by proving that S (Quot x) holds for any x. The statement of the compatibility condition for f is a bit complicated because it needs to equate terms of different types S (Quot x) and S (Quot y), which requires us to transport the left-hand side along the equivalence R x y.

  Section Elim.

    Definition cast A B (e : A = B) : A → B :=
      match e with (eq_refl _) => id end.

    Context (S : quot → Type) (f : ∀ x, S (Quot x)).
    Context (fP : ∀ x y (exy : R x y), cast (f_equal S (eq_Quot exy)) (f x) = f y).

We begin with an auxiliary result that uniquely characterizes the result of applying the eliminator to an element q : quot. Thanks to unique choice, this allows us to define the eliminator as a function quot_rect.

    Lemma quot_rect_subproof (q : quot) :
      exists! a : S q, ∃ x (exq : Quot x = q), a = cast (f_equal S exq) (f x).
    Proof.

    Definition quot_rect q : S q :=
      proj1_sig (constructive_definite_description _ (quot_rect_subproof q)).

    Lemma quot_rectE x : quot_rect (Quot x) = f x.
    Proof.

  End Elim.

In the non-dependent case, the compatibility condition acquires its usual form.

  Section Rec.

    Context S (f : T → S) (fP : ∀ x y, R x y → f x = f y).

    Definition congr1CE (A B : Type) (b : B) x y (e : x = y) :
      f_equal (λ _ : A, b) e = (eq_refl _) :=
      match e with (eq_refl _) => (eq_refl _) end.

    Definition quot_rec : quot -> S :=
      @quot_rect (λ _, S) f
                 (λ x y exy, trans_eq
                               (f_equal (λ p, cast p (f x)) (congr1CE S (eq_Quot exy)))
                               (fP exy)).

    Lemma quot_recE x : quot_rec (Quot x) = f x.
    Proof.

  End Rec.

End Quotient.


Section Lift.
  Definition quot_lift {T1 T2 : Type} (R1 : T1->T1->Prop) (R2 : T2->T2->Prop)
             {equivR1:Equivalence R1} {equivR2:Equivalence R2}
             (f : T1 -> T2) {propR:Proper (R1 ==> R2) f} :
    quot R1 -> quot R2.
  Proof.

  Global Arguments quot_lift {T1 T2} {R1 R2} {equivR1} {equivR2} f {propR}.

  Lemma quot_liftE
        {T1 T2 : Type} (R1 : T1->T1->Prop) (R2 : T2->T2->Prop)
             {equivR1:Equivalence R1} {equivR2:Equivalence R2}
             (f : T1 -> T2) {propR:Proper (R1 ==> R2) f} :
    forall x, quot_lift f (Quot R1 x) = @Quot _ R2 (f x).
  Proof.
  
  Definition quot_lift2 {T1 T2 T3 : Type} (R1 : T1->T1->Prop) (R2 : T2->T2->Prop) (R3 : T3->T3->Prop)
             {equivR1:Equivalence R1} {equivR2:Equivalence R2} {equivR3:Equivalence R3}
             (f : T1 -> T2 -> T3) {propR:Proper (R1 ==> R2 ==> R3) f} :
    quot R1 -> quot R2 -> quot R3.
  Proof.

  Global Arguments quot_lift2 {T1 T2 T3} {R1 R2 R3} {equivR1} {equivR2} {equivR3} f {propR}.
  
  Lemma quot_lift2E
        {T1 T2 T3 : Type} (R1 : T1->T1->Prop) (R2 : T2->T2->Prop) (R3 : T3->T3->Prop)
        {equivR1:Equivalence R1} {equivR2:Equivalence R2} {equivR3:Equivalence R3}
        (f : T1 -> T2 -> T3) {propR:Proper (R1 ==> R2 ==> R3) f} :
        forall x y, quot_lift2 f (Quot R1 x) (Quot R2 y) = @Quot _ R3 (f x y).
  Proof.
  
  Definition quot_lift2_to {T S : Type} (R : T->T->Prop)
             {equivR:Equivalence R}
             (f : T -> T -> S) {propR:Proper (R ==> R ==> eq) f} :
    quot R -> quot R -> S.
  Proof.

  Global Arguments quot_lift2_to {T} {S} R {equivR} f {propR}.
  
  Lemma quot_lift2_toE
        {T S : Type} (R : T->T->Prop)
        {equivR:Equivalence R}
        (f : T -> T -> S) {propR:Proper (R ==> R ==> eq) f} :
    forall x y, quot_lift2_to R f (Quot R x) (Quot R y) = f x y.
  Proof.

  Definition quot_lift_ball {T S : Type} (R : T->T->Prop)
             {equivR:Equivalence R}
             (f : T -> S -> T -> Prop) {propR:Proper (R ==> eq ==> R ==> iff) f} :
    quot R -> S -> quot R -> Prop.
  Proof.

  Global Arguments quot_lift_ball {T} {S} R {equivR} f {propR}.
  
  Lemma quot_lift_ballE
        {T S : Type} (R : T->T->Prop)
        {equivR:Equivalence R}
        (f : T -> S -> T -> Prop) {propR:Proper (R ==> eq ==> R ==> iff) f} :

    forall x e y, quot_lift_ball R f (Quot R x) e (Quot R y) = f x e y.
  Proof.

End Lift.

Generated by coq2html