From 3502cddfcb078946767f1ea50c735f578700956a Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Mon, 18 Sep 2023 12:06:15 -0400 Subject: [PATCH 1/4] Colimits/Pushout: allow Pushout_ind to simplify, since it computes on point constructors --- theories/Colimits/Pushout.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Colimits/Pushout.v b/theories/Colimits/Pushout.v index daf6ca19bc1..e476e216517 100644 --- a/theories/Colimits/Pushout.v +++ b/theories/Colimits/Pushout.v @@ -61,8 +61,8 @@ End PushoutInd. Arguments Pushout : simpl never. Arguments push : simpl never. Arguments pglue : simpl never. -Arguments Pushout_ind : simpl never. Arguments Pushout_ind_beta_pglue : simpl never. +(** However, we do allow [Pushout_ind] to simplify, as it computes on point constructors. *) Definition Pushout_rec {A B C} {f : A -> B} {g : A -> C} (P : Type) (pushb : B -> P) From 26006f2306e0c3944afc0a64c8a8a0d879036339 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Mon, 18 Sep 2023 12:07:00 -0400 Subject: [PATCH 2/4] ReflectiveSubuniverse: conn_map_homotopic: loosen universe vars to match 8.17 --- theories/Modalities/ReflectiveSubuniverse.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/theories/Modalities/ReflectiveSubuniverse.v b/theories/Modalities/ReflectiveSubuniverse.v index 261dfa38400..0a4f95440c2 100644 --- a/theories/Modalities/ReflectiveSubuniverse.v +++ b/theories/Modalities/ReflectiveSubuniverse.v @@ -1550,7 +1550,8 @@ Global Existing Instance isconnected_hfiber_conn_map. Section ConnectedMaps. Context `{Univalence} `{Funext}. - Context (O : ReflectiveSubuniverse). + Universe i. + Context (O : ReflectiveSubuniverse@{i}). (** Any equivalence is connected *) Global Instance conn_map_isequiv {A B : Type} (f : A -> B) `{IsEquiv _ _ f} @@ -1564,7 +1565,7 @@ Section ConnectedMaps. : IsConnMap O f -> IsConnMap O g. Proof. intros ? b. - exact (isconnected_equiv O (hfiber f b) + exact (isconnected_equiv O (hfiber@{i i} f b) (equiv_hfiber_homotopic f g h b) _). Defined. From 0f828c42d3c0c943d7f60c554bfbe84d9aad8483 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Mon, 18 Sep 2023 12:09:08 -0400 Subject: [PATCH 3/4] Change "Let ... Qed" to "Local Definition ... Qed" in many places --- theories/Basics/Equivalences.v | 2 +- .../Classes/implementations/binary_naturals.v | 62 +++++++++---------- .../Classes/implementations/peano_naturals.v | 27 ++++---- theories/Colimits/Pushout.v | 8 +-- 4 files changed, 48 insertions(+), 51 deletions(-) diff --git a/theories/Basics/Equivalences.v b/theories/Basics/Equivalences.v index a9a0c5833a8..d55200ac193 100644 --- a/theories/Basics/Equivalences.v +++ b/theories/Basics/Equivalences.v @@ -93,7 +93,7 @@ Section IsEquivHomotopic. Let sect := (fun a:A => (ap f^-1 (h a))^ @ eissect f a). (* We prove the triangle identity with rewrite tactics. Since we lose control over the proof term that way, we make the result opaque with "Qed". *) - Let adj (a : A) : retr (g a) = ap g (sect a). + Local Definition adj (a : A) : retr (g a) = ap g (sect a). Proof. unfold sect, retr. rewrite ap_pp. apply moveR_Vp. diff --git a/theories/Classes/implementations/binary_naturals.v b/theories/Classes/implementations/binary_naturals.v index 2537531adde..b3c162aac1a 100644 --- a/theories/Classes/implementations/binary_naturals.v +++ b/theories/Classes/implementations/binary_naturals.v @@ -62,7 +62,7 @@ Section binary_equiv. | double2 n' => Double2 (unary' n') end. - Let succunary (n : binnat) : unary' (Succ n) = S (unary' n). + Local Definition succunary (n : binnat) : unary' (Succ n) = S (unary' n). Proof. induction n. - reflexivity. @@ -70,7 +70,7 @@ Section binary_equiv. - simpl. rewrite IHn. reflexivity. Qed. - Let unarybinary : unary' o binary == idmap. + Local Definition unarybinary : unary' o binary == idmap. Proof. intros n; induction n as [|n IHn]. - reflexivity. @@ -93,7 +93,7 @@ Section binary_equiv. rewrite IHn. reflexivity. Qed. - Let binaryunary : binary o unary' == idmap. + Local Definition binaryunary : binary o unary' == idmap. Proof. intros n; induction n. - reflexivity. @@ -421,16 +421,7 @@ Section naturals. reflexivity. Qed. - Let f_preserves_0: toR 0 = 0. - Proof. reflexivity. Qed. - - Let f_preserves_1: toR 1 = 1. - Proof. - rewrite (f_nat 1). - reflexivity. - Qed. - - Let f_preserves_plus (a a' : binnat) : toR (a + a') = toR a + toR a'. + Local Definition f_preserves_plus (a a' : binnat) : toR (a + a') = toR a + toR a'. Proof. rewrite f_nat, f_nat, f_nat. unfold Compose. @@ -438,7 +429,7 @@ Section naturals. apply nat_to_sr_morphism. Qed. - Let f_preserves_mult (a a' : binnat) : toR (a * a') = toR a * toR a'. + Local Definition f_preserves_mult (a a' : binnat) : toR (a * a') = toR a * toR a'. Proof. rewrite f_nat, f_nat, f_nat. unfold Compose. @@ -449,8 +440,13 @@ Section naturals. Global Instance binnat_to_sr_morphism : IsSemiRingPreserving toR. Proof. - repeat (split;try apply _);trivial. - Qed. + split; split. + - rapply f_preserves_plus. + - reflexivity. + - rapply f_preserves_mult. + - unfold IsUnitPreserving. + apply f_nat. + Defined. Lemma binnat_toR_unique (h : binnat -> R) `{!IsSemiRingPreserving h} : forall x, toR x = h x. @@ -475,7 +471,7 @@ End naturals. Section decidable. - Let ineq_bzero_double1 n : bzero <> double1 n. + Local Definition ineq_bzero_double1 n : bzero <> double1 n. Proof. intros p. change ((fun x => match x with | double1 y => Unit | _ => Empty end) bzero). @@ -484,7 +480,7 @@ Section decidable. - exact tt. Qed. - Let ineq_bzero_double2 n : bzero <> double2 n. + Local Definition ineq_bzero_double2 n : bzero <> double2 n. Proof. intros p. change ((fun x => match x with | double2 y => Unit | _ => Empty end) bzero). @@ -493,7 +489,7 @@ Section decidable. - exact tt. Qed. - Let ineq_double1_double2 m n : double1 m <> double2 n. + Local Definition ineq_double1_double2 m n : double1 m <> double2 n. Proof. intros p. change ((fun x => match x with | double2 y => Unit | _ => Empty end) (double1 m)). @@ -502,7 +498,7 @@ Section decidable. - exact tt. Qed. - Let undouble (m : binnat) : binnat := + Local Definition undouble (m : binnat) : binnat := match m with | bzero => bzero | double1 k => k @@ -602,7 +598,7 @@ Section minus. | double2 m' => double1 m' end. - Let succ_double (m : binnat) : Succ (double m) = double1 m. + Local Definition succ_double (m : binnat) : Succ (double m) = double1 m. Proof. induction m. - reflexivity. @@ -612,7 +608,7 @@ Section minus. rewrite IHm; reflexivity. Qed. - Let double_succ (m : binnat) : double (Succ m) = double2 m. + Local Definition double_succ (m : binnat) : double (Succ m) = double2 m. Proof. induction m. - reflexivity. @@ -622,24 +618,24 @@ Section minus. rewrite IHm; reflexivity. Qed. - Let pred_succ (m : binnat) : Pred (Succ m) = m. + Local Definition pred_succ (m : binnat) : Pred (Succ m) = m. Proof. induction m; try reflexivity. - exact (double_succ m). Qed. - Let double_pred (m : binnat) : double (Pred m) = Pred (Pred (double m)). + Local Definition double_pred (m : binnat) : double (Pred m) = Pred (Pred (double m)). Proof. induction m; try reflexivity. - exact (double_succ (double m))^. Qed. - Let pred_double2 (m : binnat) : Pred (double2 m) = double1 m. + Local Definition pred_double2 (m : binnat) : Pred (double2 m) = double1 m. Proof. induction m; reflexivity. Qed. - Let pred_double1 (m : binnat) : Pred (double1 m) = double m. + Local Definition pred_double1 (m : binnat) : Pred (double1 m) = double m. Proof. induction m; reflexivity. Qed. @@ -662,17 +658,17 @@ Section minus. Global Instance binnat_cut_minus: CutMinus binnat := binnat_cut_minus'. - Let binnat_minus_zero (m : binnat) : m ∸ bzero = m. + Local Definition binnat_minus_zero (m : binnat) : m ∸ bzero = m. Proof. induction m; reflexivity. Qed. - Let binnat_zero_minus (m : binnat) : bzero ∸ m = bzero. + Local Definition binnat_zero_minus (m : binnat) : bzero ∸ m = bzero. Proof. induction m; reflexivity. Qed. - Let pred_succ_minus (m n : binnat) : Pred (Succ m ∸ n) = m ∸ n. + Local Definition pred_succ_minus (m n : binnat) : Pred (Succ m ∸ n) = m ∸ n. Proof. revert n; induction m; intros n; induction n; try reflexivity. - change (Pred (double (bzero ∸ n)) = bzero). @@ -692,7 +688,7 @@ Section minus. exact (IHm n). Qed. - Let double_cases (m : binnat) : (bzero = double m) + hfiber double2 (double m). + Local Definition double_cases (m : binnat) : (bzero = double m) + hfiber double2 (double m). Proof. induction m. - left; reflexivity. @@ -700,7 +696,7 @@ Section minus. - right; exists (Succ (double m)); reflexivity. Defined. - Let binnat_minus_succ (m n : binnat) : Succ m ∸ Succ n = m ∸ n. + Local Definition binnat_minus_succ (m n : binnat) : Succ m ∸ Succ n = m ∸ n. Proof. revert n; induction m; intros n; induction n; try reflexivity. - change (Pred (double (bzero ∸ n)) = bzero ∸ double1 n). @@ -719,7 +715,7 @@ Section minus. rewrite IHm. reflexivity. Qed. - Let binaryminus (x y : nat) : binary x ∸ binary y = binary (x ∸ y). + Local Definition binaryminus (x y : nat) : binary x ∸ binary y = binary (x ∸ y). Proof. revert y; induction x; intros y; induction y; try reflexivity. - apply binnat_zero_minus. @@ -728,7 +724,7 @@ Section minus. rewrite IHx. reflexivity. Qed. - Let unaryminus (m n : binnat) : unary m ∸ unary n = unary (m ∸ n). + Local Definition unaryminus (m n : binnat) : unary m ∸ unary n = unary (m ∸ n). Proof. etransitivity (unary (binary (_^-1 m ∸ _^-1 n))). - apply ((eissect binary (unary m ∸ unary n)) ^). diff --git a/theories/Classes/implementations/peano_naturals.v b/theories/Classes/implementations/peano_naturals.v index 7ac1d9bf4ab..4737e3b7211 100644 --- a/theories/Classes/implementations/peano_naturals.v +++ b/theories/Classes/implementations/peano_naturals.v @@ -18,8 +18,11 @@ Universe N. Let natpaths := @paths@{N} nat. Infix "=N=" := natpaths. -Let natpaths_symm : Symmetric@{N N} natpaths. -Proof. unfold natpaths;apply _. Qed. + +Definition natpaths_symm : Symmetric@{N N} natpaths. +Proof. + unfold natpaths; apply _. +Defined. Global Instance nat_0: Zero@{N} nat := 0%nat. Global Instance nat_1: One@{N} nat := 1%nat. @@ -582,20 +585,14 @@ Section for_another_semiring. (* Add Ring R: (rings.stdlib_semiring_theory R). *) - Let f_preserves_0: toR 0 = 0. - Proof. reflexivity. Qed. - - Let f_preserves_1: toR 1 = 1. - Proof. reflexivity. Qed. - - Let f_S : forall x, toR (S x) = 1 + toR x. + Local Definition f_S : forall x, toR (S x) = 1 + toR x. Proof. intros [|x]. - symmetry;apply plus_0_r. - reflexivity. - Qed. + Defined. - Let f_preserves_plus a a': toR (a + a') = toR a + toR a'. + Local Definition f_preserves_plus a a': toR (a + a') = toR a + toR a'. Proof. induction a as [|a IHa]. - change (toR a' = 0 + toR a'). @@ -605,7 +602,7 @@ Section for_another_semiring. apply associativity. Qed. - Let f_preserves_mult a a': toR (a * a') = toR a * toR a'. + Local Definition f_preserves_mult a a': toR (a * a') = toR a * toR a'. Proof. induction a as [|a IHa]. - change (0 = 0 * toR a'). @@ -620,7 +617,11 @@ Section for_another_semiring. Global Instance nat_to_sr_morphism : IsSemiRingPreserving (naturals_to_semiring nat R). Proof. - repeat (split;try apply _);trivial. + split; split. + - rapply f_preserves_plus. + - reflexivity. + - rapply f_preserves_mult. + - reflexivity. Defined. Lemma toR_unique (h : nat -> R) `{!IsSemiRingPreserving h} x : diff --git a/theories/Colimits/Pushout.v b/theories/Colimits/Pushout.v index e476e216517..e00c1e2a0ef 100644 --- a/theories/Colimits/Pushout.v +++ b/theories/Colimits/Pushout.v @@ -259,7 +259,7 @@ Section EquivSigmaPushout. (A : X -> Type) (B : X -> Type) (C : X -> Type) (f : forall x, A x -> B x) (g : forall x, A x -> C x). - Let esp1 : { x : X & Pushout (f x) (g x) } + Local Definition esp1 : { x : X & Pushout (f x) (g x) } -> Pushout (functor_sigma idmap f) (functor_sigma idmap g). Proof. intros [x p]. @@ -269,7 +269,7 @@ Section EquivSigmaPushout. + intros a; cbn. exact (pglue (x;a)). Defined. - Let esp1_beta_pglue (x : X) (a : A x) + Local Definition esp1_beta_pglue (x : X) (a : A x) : ap esp1 (path_sigma' (fun x => Pushout (f x) (g x)) 1 (pglue a)) = pglue (x;a). Proof. @@ -280,7 +280,7 @@ Section EquivSigmaPushout. reflexivity. Qed. - Let esp2 : Pushout (functor_sigma idmap f) (functor_sigma idmap g) + Local Definition esp2 : Pushout (functor_sigma idmap f) (functor_sigma idmap g) -> { x : X & Pushout (f x) (g x) }. Proof. srefine (Pushout_rec _ _ _ _). @@ -291,7 +291,7 @@ Section EquivSigmaPushout. apply pglue. Defined. - Let esp2_beta_pglue (x : X) (a : A x) + Local Definition esp2_beta_pglue (x : X) (a : A x) : ap esp2 (pglue (x;a)) = path_sigma' (fun x:X => Pushout (f x) (g x)) 1 (pglue a). Proof. unfold esp2. From 7bb620c295871dae3affaa8656fe09c6fc152324 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Mon, 18 Sep 2023 12:09:40 -0400 Subject: [PATCH 4/4] Categories/LaxComma/Core: add Set annotation to silence warnings --- theories/Categories/LaxComma/Core.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/Categories/LaxComma/Core.v b/theories/Categories/LaxComma/Core.v index 212d8746ce1..f4dfd385bcf 100644 --- a/theories/Categories/LaxComma/Core.v +++ b/theories/Categories/LaxComma/Core.v @@ -175,7 +175,7 @@ Module Export LaxCommaCoreNotations. (** We play some games to get nice notations for lax comma categories. *) Section tc_notation_boiler_plate. Local Open Scope type_scope. - Class LCC_Builder {A B C} (x : A) (y : B) (z : C) := lcc_builder_dummy : True. + Class LCC_Builder {A B C} (x : A) (y : B) (z : C) : Set := lcc_builder_dummy : True. Definition get_LCC `{@LCC_Builder A B C x y z} : C := z. Global Arguments get_LCC / {A B C} x y {z} {_}. @@ -210,7 +210,7 @@ Module Export LaxCommaCoreNotations. : LCC_Builder (@sub_pre_cat _ P HF) a (@lax_coslice_category_over _ P HF a _) | 10 := I. - Class OLCC_Builder {A B C} (x : A) (y : B) (z : C) := olcc_builder_dummy : True. + Class OLCC_Builder {A B C} (x : A) (y : B) (z : C) : Set := olcc_builder_dummy : True. Definition get_OLCC `{@OLCC_Builder A B C x y z} : C := z.