From 0ddc04ff2a71e0805448fbdcaeb195cf9b265b9d Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sat, 21 Sep 2024 14:26:39 -0400 Subject: [PATCH 1/5] STYLE.md: add remark about composing equivalences --- STYLE.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/STYLE.md b/STYLE.md index f0b0b3c15a..72ca480201 100644 --- a/STYLE.md +++ b/STYLE.md @@ -339,6 +339,11 @@ The inverse function can then be referred to as `foo ^-1`. Avoid using `equiv_foo` unless you really do need an `Equiv` object, rather than a function which happens to be an equivalence. +On the other hand, sometimes it is easier to define an equivalence +by composing together existing equivalences, in which case one goes +immediately to the last step, defining `equiv_foo`. If the equivalence +is used frequently as an ordinary function, one might also define `foo` +as the underlying function of `equiv_foo`; see `path_equiv`, as an example. ## 3. Records, Structures, Typeclasses ## From ffddf2e7ac94f988332222314aafa7b24c29bcc0 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sat, 21 Sep 2024 14:27:23 -0400 Subject: [PATCH 2/5] Move path_via from Overture to Basics/Tactics; other cleanups --- theories/Basics/Overture.v | 17 +++-------------- theories/Basics/Tactics.v | 4 ++++ theories/Diagrams/CommutativeSquares.v | 2 +- 3 files changed, 8 insertions(+), 15 deletions(-) diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v index 779cda59d5..b627e05404 100644 --- a/theories/Basics/Overture.v +++ b/theories/Basics/Overture.v @@ -655,10 +655,9 @@ Existing Class Funext. Axiom isequiv_apD10 : forall `{Funext} (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g). Global Existing Instance isequiv_apD10. -Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) : - f == g -> f = g - := - (@apD10 A P f g)^-1. +Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) + : f == g -> f = g + := (@apD10 A P f g)^-1. Global Arguments path_forall {_ A%_type_scope P} (f g)%_function_scope _. @@ -674,9 +673,6 @@ Global Arguments path_forall {_ A%_type_scope P} (f g)%_function_scope _. #[export] Hint Resolve idpath inverse : path_hints. #[export] Hint Resolve idpath : core. -Ltac path_via mid := - apply @concat with (y := mid); auto with path_hints. - (** ** Natural numbers *) (** Natural numbers. *) @@ -688,13 +684,6 @@ Scheme nat_ind := Induction for nat Sort Type. Scheme nat_rect := Induction for nat Sort Type. Scheme nat_rec := Induction for nat Sort Type. -(** These schemes are therefore defined in Spaces.Nat *) -(* -Scheme nat_ind := Induction for nat Sort Type. -Scheme nat_rect := Induction for nat Sort Type. -Scheme nat_rec := Minimality for nat Sort Type. - *) - Declare Scope nat_scope. Delimit Scope nat_scope with nat. Bind Scope nat_scope with nat. diff --git a/theories/Basics/Tactics.v b/theories/Basics/Tactics.v index 9cc6200b67..c8e24b779a 100644 --- a/theories/Basics/Tactics.v +++ b/theories/Basics/Tactics.v @@ -6,6 +6,10 @@ Require Import Basics.Overture. (** This module implements various tactics used in the library. *) +(** If the goal is [x = z], [path_via y] will replace this with two goals, [x = y] and [y = z]. *) +Ltac path_via mid := + apply @concat with (y := mid); auto with path_hints. + (** The following tactic is designed to be more or less interchangeable with [induction n as [ | n' IH ]] whenever [n] is a [nat] or a [trunc_index]. The difference is that it produces proof terms involving [fix] explicitly rather than [nat_ind] or [trunc_index_ind], and therefore does not introduce higher universe parameters. It works if [n] is in the context or in the goal. *) Ltac simple_induction n n' IH := try generalize dependent n; diff --git a/theories/Diagrams/CommutativeSquares.v b/theories/Diagrams/CommutativeSquares.v index de7daa1197..01cceb906e 100644 --- a/theories/Diagrams/CommutativeSquares.v +++ b/theories/Diagrams/CommutativeSquares.v @@ -1,4 +1,4 @@ -Require Import Basics.Overture Basics.PathGroupoids. +Require Import Basics.Overture Basics.PathGroupoids Basics.Tactics. (** * Comutative squares *) From b517d6736a04d6d3532d08cf9a9c7ec03d105bf5 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sat, 21 Sep 2024 14:35:33 -0400 Subject: [PATCH 3/5] Quotient.v: mv Quotient_rec2 early; fix up comments, var names. --- theories/Colimits/Quotient.v | 79 +++++++++++++++++++----------------- 1 file changed, 41 insertions(+), 38 deletions(-) diff --git a/theories/Colimits/Quotient.v b/theories/Colimits/Quotient.v index 3ee2c9cb20..d4a1f59ee1 100644 --- a/theories/Colimits/Quotient.v +++ b/theories/Colimits/Quotient.v @@ -8,7 +8,7 @@ Require Import PropResizing. Local Open Scope path_scope. -(** * The set-quotient of a type by an hprop-valued relation +(** * The set-quotient of a type by a relation We aim to model: << @@ -19,7 +19,10 @@ Inductive Quotient R : Type := >> We do this by defining the quotient as a 0-truncated graph quotient. -Throughout this file [a], [b] and [c] are elements of [A], [R] is a relation on [A], [x], [y] and [z] are elements of [Quotient R], [p] is a proof of [R a b]. *) +Some results require additional assumptions, for example, that the relation be hprop-valued, or that the relation be reflexive, transitive or symmetric. + +Throughout this file [a], [b] and [c] are elements of [A], [R] is a relation on [A], [x], [y] and [z] are elements of [Quotient R], [p] is a proof of [R a b]. +*) Definition Quotient@{i j k} {A : Type@{i}} (R : Relation@{i j} A) : Type@{k} := Trunc@{k} 0 (GraphQuotient@{i j k} R). @@ -92,7 +95,7 @@ Arguments Quotient_rec_beta_qglue : simpl never. Notation "A / R" := (Quotient (A:=A) R). -(* Quotient induction into a hprop. *) +(** Quotient induction into an hprop. *) Definition Quotient_ind_hprop {A : Type@{i}} (R : Relation@{i j} A) (P : A / R -> Type) `{forall x, IsHProp (P x)} (dclass : forall a, P (class_of R a)) @@ -122,12 +125,39 @@ Proof. exact (dclass a b c). Defined. +Definition Quotient_rec2 {A : Type} (R : Relation A) `{Reflexive _ R} + {B : Type} `{IsHSet B} + {dclass : A -> A -> B} + {dequiv : forall a a', R a a' -> forall b b', + R b b' -> dclass a b = dclass a' b'} + : A / R -> A / R -> B. +Proof. + intro x. + srapply Quotient_rec. + - intro b. + revert x. + srapply Quotient_rec. + + intro a. + exact (dclass a b). + + cbn beta. + intros a a' p. + by apply (dequiv a a' p b b). + - cbn beta. + intros b b' p. + revert x. + srapply Quotient_ind. + + cbn; intro a. + by apply dequiv. + + intros a a' q. + apply path_ishprop. +Defined. + Section Equiv. Context `{Univalence} {A : Type} (R : Relation A) `{is_mere_relation _ R} `{Transitive _ R} `{Symmetric _ R} `{Reflexive _ R}. - (* The proposition of being in a given class in a quotient. *) + (** The proposition of being in a given class in a quotient. This requires [Univalence] so that we know that [HProp] is a set. *) Definition in_class : A / R -> A -> HProp. Proof. intros x b; revert x. @@ -140,20 +170,20 @@ Section Equiv. apply (transitivity p). Defined. - (* Being in a class is decidable if the Relation is decidable. *) + (** Being in a class is decidable if the relation is decidable. *) Global Instance decidable_in_class `{forall a b, Decidable (R a b)} : forall x a, Decidable (in_class x a). Proof. by srapply Quotient_ind_hprop. Defined. - (* if x is in a class q, then the class of x is equal to q. *) + (** If [a] is in a class [x], then the class of [a] is equal to [x]. *) Lemma path_in_class_of : forall x a, in_class x a -> x = class_of R a. Proof. srapply Quotient_ind. - { intros x y p. + { intros a b p. exact (qglue p). } - intros x y p. + intros a b p. funext ? ?. apply hset_path2. Defined. @@ -167,7 +197,7 @@ Section Equiv. cbv; reflexivity. Defined. - (** Thm 10.1.8 *) + (** Theorem 10.1.8. *) Theorem path_quotient (a b : A) : R a b <~> (class_of R a = class_of R b). Proof. @@ -176,33 +206,7 @@ Section Equiv. - apply related_quotient_paths. Defined. - Definition Quotient_rec2 {B : Type} `{IsHSet B} {dclass : A -> A -> B} - {dequiv : forall a a', R a a' -> forall b b', - R b b' -> dclass a b = dclass a' b'} - : A / R -> A / R -> B. - Proof. - clear H. (* Ensure that we don't use Univalence. *) - intro x. - srapply Quotient_rec. - - intro b. - revert x. - srapply Quotient_rec. - + intro a. - exact (dclass a b). - + cbn beta. - intros a a' p. - by apply (dequiv a a' p b b). - - cbn beta. - intros b b' p. - revert x. - srapply Quotient_ind. - + cbn; intro a. - by apply dequiv. - + intros a a' q. - apply path_ishprop. - Defined. - - (** The map class_of : A -> A/R is a surjection. *) + (** The map [class_of : A -> A/R] is a surjection. *) Global Instance issurj_class_of : IsSurjection (class_of R). Proof. apply BuildIsSurjection. @@ -212,8 +216,7 @@ Section Equiv. by exists a. Defined. - (* Universal property of quotient *) - (* Lemma 6.10.3 *) + (** The universal property of the quotient. This is Lemma 6.10.3. *) Theorem equiv_quotient_ump (B : Type) `{IsHSet B} : (A / R -> B) <~> {f : A -> B & forall a b, R a b -> f a = f b}. Proof. From 2bf42eeacb77b4c023664fe6f97c29dda1315163 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sat, 21 Sep 2024 14:37:07 -0400 Subject: [PATCH 4/5] Quotient.v: remove reflexivity hyp from Quotient_rec2 --- theories/Algebra/Groups/QuotientGroup.v | 5 ++--- theories/Algebra/Rings/Localization.v | 16 ++++++---------- theories/Algebra/Rings/QuotientRing.v | 5 ++--- theories/Colimits/Quotient.v | 15 ++++++--------- 4 files changed, 16 insertions(+), 25 deletions(-) diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v index 91c0c3396f..765ae89a41 100644 --- a/theories/Algebra/Groups/QuotientGroup.v +++ b/theories/Algebra/Groups/QuotientGroup.v @@ -30,9 +30,8 @@ Section GroupCongruenceQuotient. srapply Quotient_rec2. - intros x y. exact (class_of _ (x * y)). - - intros x x' p y y' q. - apply qglue. - by apply iscong. + - intros x x' y p. apply qglue. by apply iscong. + - intros x y y' q. apply qglue. by apply iscong. Defined. Global Instance congquot_mon_unit : MonUnit CongruenceQuotient. diff --git a/theories/Algebra/Rings/Localization.v b/theories/Algebra/Rings/Localization.v index 2e5197ca3a..db5873a094 100644 --- a/theories/Algebra/Rings/Localization.v +++ b/theories/Algebra/Rings/Localization.v @@ -166,13 +166,11 @@ Section Localization. Instance plus_rng_localization : Plus (Quotient fraction_eq). Proof. srapply Quotient_rec2. - - rapply fraction_eq_refl. - cbn. intros f1 f2. exact (class_of _ (frac_add f1 f2)). - - cbn beta. - intros f1 f1' p f2 f2' q. - by apply qglue, frac_add_wd. + - intros f1 f1' f2 p. by apply qglue, frac_add_wd_l. + - intros f1 f2 f2' q. by apply qglue, frac_add_wd_r. Defined. (** *** Multiplication operation *) @@ -212,15 +210,13 @@ Section Localization. Instance mult_rng_localization: Mult (Quotient fraction_eq). Proof. srapply Quotient_rec2. - - rapply fraction_eq_refl. - cbn. intros f1 f2. exact (class_of _ (frac_mult f1 f2)). - - cbn beta. - intros f1 f1' p f2 f2' q. - transitivity (class_of fraction_eq (frac_mult f1' f2)). - + by apply qglue, frac_mult_wd_l. - + by apply qglue, frac_mult_wd_r. + - intros f1 f1' f2 p; cbn beta. + by apply qglue, frac_mult_wd_l. + - intros f1 f2 f2' q; cbn beta. + by apply qglue, frac_mult_wd_r. Defined. (** *** Zero element *) diff --git a/theories/Algebra/Rings/QuotientRing.v b/theories/Algebra/Rings/QuotientRing.v index 514c3a1a99..f191421ea1 100644 --- a/theories/Algebra/Rings/QuotientRing.v +++ b/theories/Algebra/Rings/QuotientRing.v @@ -42,9 +42,8 @@ Section QuotientRing. Proof. srapply Quotient_rec2. - exact (fun x y => class_of _ (x * y)). - - intros x x' p y y' q; simpl. - apply qglue. - by rapply iscong. + - intros x x' y p. apply qglue. by apply iscong. + - intros x y y' q. apply qglue. by apply iscong. Defined. Instance one_quotient_abgroup : One (QuotientAbGroup R I) := class_of _ one. diff --git a/theories/Colimits/Quotient.v b/theories/Colimits/Quotient.v index d4a1f59ee1..c83ddff112 100644 --- a/theories/Colimits/Quotient.v +++ b/theories/Colimits/Quotient.v @@ -125,11 +125,11 @@ Proof. exact (dclass a b c). Defined. -Definition Quotient_rec2 {A : Type} (R : Relation A) `{Reflexive _ R} +Definition Quotient_rec2 {A : Type} (R : Relation A) {B : Type} `{IsHSet B} {dclass : A -> A -> B} - {dequiv : forall a a', R a a' -> forall b b', - R b b' -> dclass a b = dclass a' b'} + {dequiv_l : forall a a' b, R a a' -> dclass a b = dclass a' b} + {dequiv_r : forall a b b', R b b' -> dclass a b = dclass a b'} : A / R -> A / R -> B. Proof. intro x. @@ -141,15 +141,12 @@ Proof. exact (dclass a b). + cbn beta. intros a a' p. - by apply (dequiv a a' p b b). + by apply dequiv_l. - cbn beta. intros b b' p. revert x. - srapply Quotient_ind. - + cbn; intro a. - by apply dequiv. - + intros a a' q. - apply path_ishprop. + srapply Quotient_ind_hprop; simpl. + intro a; by apply dequiv_r. Defined. Section Equiv. From e323ac819aa68f8e4c6b242ee35e5c3b0af98a06 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 21 Sep 2024 21:29:14 +0200 Subject: [PATCH 5/5] generalise Quotient_rec2 to Quotient_ind2 Signed-off-by: Ali Caglayan --- theories/Colimits/Quotient.v | 31 +++++++++++++++++++++++-------- 1 file changed, 23 insertions(+), 8 deletions(-) diff --git a/theories/Colimits/Quotient.v b/theories/Colimits/Quotient.v index c83ddff112..feae531e28 100644 --- a/theories/Colimits/Quotient.v +++ b/theories/Colimits/Quotient.v @@ -125,18 +125,19 @@ Proof. exact (dclass a b c). Defined. -Definition Quotient_rec2 {A : Type} (R : Relation A) - {B : Type} `{IsHSet B} - {dclass : A -> A -> B} - {dequiv_l : forall a a' b, R a a' -> dclass a b = dclass a' b} - {dequiv_r : forall a b b', R b b' -> dclass a b = dclass a b'} - : A / R -> A / R -> B. +Definition Quotient_ind2 {A : Type} (R : Relation A) + (P : A / R -> A / R -> Type) `{forall x y, IsHSet (P x y)} + (dclass : forall a b, P (class_of R a) (class_of R b)) + (dequiv_l : forall a a' b (p : R a a'), + transport (fun x => P x _) (qglue p) (dclass a b) = dclass a' b) + (dequiv_r : forall a b b' (p : R b b'), qglue p # dclass a b = dclass a b') + : forall x y, P x y. Proof. intro x. - srapply Quotient_rec. + srapply Quotient_ind. - intro b. revert x. - srapply Quotient_rec. + srapply Quotient_ind. + intro a. exact (dclass a b). + cbn beta. @@ -149,6 +150,20 @@ Proof. intro a; by apply dequiv_r. Defined. +Definition Quotient_rec2 {A : Type} (R : Relation A) (B : Type) `{IsHSet B} + (dclass : A -> A -> B) + (dequiv_l : forall a a' b, R a a' -> dclass a b = dclass a' b) + (dequiv_r : forall a b b', R b b' -> dclass a b = dclass a b') + : A / R -> A / R -> B. +Proof. + srapply Quotient_ind2. + - exact dclass. + - intros; lhs nrapply transport_const. + by apply dequiv_l. + - intros; lhs nrapply transport_const. + by apply dequiv_r. +Defined. + Section Equiv. Context `{Univalence} {A : Type} (R : Relation A) `{is_mere_relation _ R}