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:
-
Functional extensionality
-
Propositional extensionality
-
Constructive definite description (also known as the axiom of unique choice)
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.
intros e.
inversion e.
rewrite H0.
reflexivity.
Qed.
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.
destruct q.
unfold Quot.
destruct quot_classP0;
simpl.
rewrite e.
eauto.
Qed.
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.
destruct q;
simpl.
destruct quot_classP0 as [
x q].
rewrite q.
exists (
f x).
split.
-
eauto.
-
intros x' [?[??]].
subst.
inversion x1.
assert (
eqq:
R x0 x).
{
apply Quot_inj;
apply eq_Quot.
rewrite H0;
reflexivity.
}
rewrite <- (@
fP x0 x eqq).
do 2
f_equal.
apply proof_irrelevance.
Unshelve.
exact x.
reflexivity.
Qed.
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.
assert (
Hpf:
forall x0 y :
T1,
R1 x0 y ->
Quot R2 (
f x0) =
Quot R2 (
f y)).
{
intros.
apply eq_Quot;
trivial.
rewrite H.
reflexivity.
}
apply (@
quot_rec _ _ equivR1 (
quot R2) (
fun y =>
Quot R2 (
f y))
Hpf).
Defined.
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.