Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Adjustments to support Coq 8.18.0 #1763

Merged
merged 4 commits into from
Sep 18, 2023
Merged

Adjustments to support Coq 8.18.0 #1763

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
3502cdd
Colimits/Pushout: allow Pushout_ind to simplify, since it computes on…
jdchristensen Sep 18, 2023
26006f2
ReflectiveSubuniverse: conn_map_homotopic: loosen universe vars to ma…
jdchristensen Sep 18, 2023
0f828c4
Change "Let ... Qed" to "Local Definition ... Qed" in many places
jdchristensen Sep 18, 2023
7bb620c
Categories/LaxComma/Core: add Set annotation to silence warnings
jdchristensen Sep 18, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion theories/Basics/Equivalences.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 2 additions & 2 deletions theories/Categories/LaxComma/Core.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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} {_}.
Expand Down Expand Up @@ -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.

Expand Down
62 changes: 29 additions & 33 deletions theories/Classes/implementations/binary_naturals.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,15 +62,15 @@ 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.
- reflexivity.
- 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.
Expand All @@ -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.
Expand Down Expand Up @@ -421,24 +421,15 @@ 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.
rewrite <- (unaryplus a a').
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.
Expand All @@ -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.
Expand All @@ -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).
Expand All @@ -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).
Expand All @@ -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)).
Expand All @@ -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
Expand Down Expand Up @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand All @@ -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).
Expand All @@ -692,15 +688,15 @@ 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.
- right; exists (double m); reflexivity.
- 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).
Expand All @@ -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.
Expand All @@ -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)) ^).
Expand Down
27 changes: 14 additions & 13 deletions theories/Classes/implementations/peano_naturals.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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').
Expand All @@ -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').
Expand All @@ -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 :
Expand Down
10 changes: 5 additions & 5 deletions theories/Colimits/Pushout.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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].
Expand All @@ -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.
Expand All @@ -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 _ _ _ _).
Expand All @@ -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.
Expand Down
5 changes: 3 additions & 2 deletions theories/Modalities/ReflectiveSubuniverse.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand All @@ -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.

Expand Down
Loading