diff --git a/theories/Algebra/ooGroup.v b/theories/Algebra/ooGroup.v index c1a1682561..5d56ca6cf5 100644 --- a/theories/Algebra/ooGroup.v +++ b/theories/Algebra/ooGroup.v @@ -218,25 +218,25 @@ Section Subgroups. Definition in_coset : G -> G -> Type := fun g1 g2 => hfiber incl (g1 @ g2^). - Instance ishprop_in_coset : is_mere_relation G in_coset. + #[export] Instance ishprop_in_coset : is_mere_relation G in_coset. Proof. exact _. Defined. - Instance reflexive_coset : Reflexive in_coset. + #[export] Instance reflexive_coset : Reflexive in_coset. Proof. intros g. exact (1 ; grouphom_1 incl @ (concat_pV g)^). Defined. - Instance symmetric_coset : Symmetric in_coset. + #[export] Instance symmetric_coset : Symmetric in_coset. Proof. intros g1 g2 [h p]. exists (h^). exact (grouphom_V incl h @ inverse2 p @ inv_pp _ _ @ whiskerR (inv_V _) _). Defined. - Instance transitive_coset : Transitive in_coset. + #[export] Instance transitive_coset : Transitive in_coset. Proof. intros g1 g2 g3 [h1 p1] [h2 p2]. exists (h1 @ h2). diff --git a/theories/Classes/orders/lattices.v b/theories/Classes/orders/lattices.v index b3e0f146a9..026b94dc50 100644 --- a/theories/Classes/orders/lattices.v +++ b/theories/Classes/orders/lattices.v @@ -279,7 +279,7 @@ Section meet_semilattice_order. - rewrite <-E. apply meet_lb_r. Qed. - #[export] Instance: forall z, OrderPreserving (z ⊓). + #[export] Instance OrderPreserving_left_meet : forall z, OrderPreserving (z ⊓). Proof. red;intros. apply meet_glb. @@ -287,7 +287,7 @@ Section meet_semilattice_order. - apply meet_le_compat_l. trivial. Qed. - #[export] Instance: forall z, OrderPreserving (⊓ z). + #[export] Instance OrderPreserving_right_meet: forall z, OrderPreserving (⊓ z). Proof. intros. exact maps.order_preserving_flip. Qed. @@ -346,10 +346,10 @@ End meet_semilattice_order. Section lattice_order. Context `{LatticeOrder L}. - Instance: IsJoinSemiLattice L := join_sl_order_join_sl. - Instance: IsMeetSemiLattice L := meet_sl_order_meet_sl. + Instance IsJoinSemilattice_LatticeOrder : IsJoinSemiLattice L := join_sl_order_join_sl. + Instance IsMeetSemilattice_LatticeOrder : IsMeetSemiLattice L := meet_sl_order_meet_sl. - Instance: Absorption (⊓) (⊔). + Instance Absorption_join_meet : Absorption (⊓) (⊔). Proof. intros x y. apply (antisymmetry (≤)). - apply meet_lb_l. @@ -358,7 +358,7 @@ Section lattice_order. + apply join_ub_l. Qed. - Instance: Absorption (⊔) (⊓). + Instance Absorption_meet_join : Absorption (⊔) (⊓). Proof. intros x y. apply (antisymmetry (≤)). - apply join_le. diff --git a/theories/Classes/orders/nat_int.v b/theories/Classes/orders/nat_int.v index 5a9881e52c..ed79287786 100644 --- a/theories/Classes/orders/nat_int.v +++ b/theories/Classes/orders/nat_int.v @@ -147,7 +147,7 @@ Section another_semiring. `{PropHolds ((1 : R2) ≶ 0)} `{!IsSemiRingPreserving (f : R -> R2)}. - Instance: OrderPreserving f. + Instance OrderPreserving_SemiRing_Homomorphism : OrderPreserving f. Proof. repeat (split; try exact _). intros x y E. apply nat_int_le_plus in E. destruct E as [z E]. @@ -155,7 +155,7 @@ Section another_semiring. apply nonneg_plus_le_compat_r. apply to_semiring_nonneg. Qed. - #[export] Instance: StrictlyOrderPreserving f | 50. + #[export] Instance StrictlyOrderPreserving_SemiRing_Homomorphism : StrictlyOrderPreserving f | 50. Proof. repeat (split; try exact _). intros x y E. apply nat_int_lt_plus in E. destruct E as [z E]. diff --git a/theories/Classes/orders/naturals.v b/theories/Classes/orders/naturals.v index c60456170b..b6423e28eb 100644 --- a/theories/Classes/orders/naturals.v +++ b/theories/Classes/orders/naturals.v @@ -59,7 +59,7 @@ etransitivity. - apply pos_ge_1. Qed. -#[export] Instance: forall (z : N), PropHolds (z <> 0) -> OrderReflecting (z *.). +#[export] Instance OrderReflecting_left_mult : forall (z : N), PropHolds (z <> 0) -> OrderReflecting (z *.). Proof. intros z ?. red. apply (order_reflecting_pos (.*.) z). apply nat_ne_0_pos. trivial. diff --git a/theories/Classes/orders/orders.v b/theories/Classes/orders/orders.v index 995763bda1..0c4546cfcd 100644 --- a/theories/Classes/orders/orders.v +++ b/theories/Classes/orders/orders.v @@ -558,6 +558,6 @@ Section pseudo. - destruct (pseudo_order_antisym y z (ltyz , ltzy)). Qed. - Existing Instance lt_transitive. + #[export] Existing Instance lt_transitive. End pseudo. diff --git a/theories/Classes/orders/semirings.v b/theories/Classes/orders/semirings.v index c70348f6c5..c53e9fd2b2 100644 --- a/theories/Classes/orders/semirings.v +++ b/theories/Classes/orders/semirings.v @@ -437,7 +437,7 @@ Section pseudo_semiring_order. exact strictly_order_reflecting_flip. Qed. - Global Instance apartzero_mult_strong_cancel_l + #[export] Instance apartzero_mult_strong_cancel_l : forall z, PropHolds (z ≶ 0) -> StrongLeftCancellation (.*.) z. Proof. intros z Ez x y E. red in Ez. @@ -602,12 +602,12 @@ Section full_pseudo_semiring_order. destruct (neg_mult_decompose x y E) as [[? ?]|[? ?]];auto. Qed. - #[export] Instance : forall (z : R), PropHolds (0 < z) -> OrderReflecting (z *.). + #[export] Instance OrderReflecting_left_mult : forall (z : R), PropHolds (0 < z) -> OrderReflecting (z *.). Proof. intros z E. exact full_pseudo_order_reflecting. Qed. - #[export] Instance: forall (z : R), PropHolds (0 < z) -> OrderReflecting (.* z). + #[export] Instance OrderReflecting_right_mult : forall (z : R), PropHolds (0 < z) -> OrderReflecting (.* z). Proof. intros. exact order_reflecting_flip. Qed. diff --git a/theories/Classes/theory/apartness.v b/theories/Classes/theory/apartness.v index 782ccd48a5..d44d9a784b 100644 --- a/theories/Classes/theory/apartness.v +++ b/theories/Classes/theory/apartness.v @@ -12,7 +12,7 @@ intros ap e;revert ap. apply tight_apart. assumption. Qed. -#[export] Instance: forall x y : A, Stable (x = y). +#[export] Instance apartness_eq_stable: forall x y : A, Stable (x = y). Proof. intros x y. unfold Stable. intros dn. apply tight_apart. diff --git a/theories/Classes/theory/fields.v b/theories/Classes/theory/fields.v index 23bac28ce5..c9a12cb318 100644 --- a/theories/Classes/theory/fields.v +++ b/theories/Classes/theory/fields.v @@ -52,7 +52,7 @@ Proof. intros ? E. rewrite <-E. trivial. Qed. -#[export] Instance: IsStrongInjective (-). +#[export] Instance IsStrongInjective_FieldNegation: IsStrongInjective (-). Proof. repeat (split; try exact _); intros x y E. - apply (strong_extensionality (+ x + y)). @@ -67,7 +67,7 @@ repeat (split; try exact _); intros x y E. apply symmetry;trivial. Qed. -#[export] Instance: IsStrongInjective (//). +#[export] Instance IsStrongInjective_FieldDivision: IsStrongInjective (//). Proof. repeat (split; try exact _); intros x y E. - apply (strong_extensionality (x.1 *.)). @@ -82,7 +82,7 @@ repeat (split; try exact _); intros x y E. rewrite mult_1_l,mult_1_r. apply symmetry;trivial. Qed. -#[export] Instance: forall z, StrongLeftCancellation (+) z. +#[export] Instance StrongLeftCancellation_plus_field: forall z, StrongLeftCancellation (+) z. Proof. intros z x y E. apply (strong_extensionality (+ -z)). do 2 rewrite (commutativity (f:=plus) z _), @@ -90,12 +90,12 @@ do 2 rewrite (commutativity (f:=plus) z _), trivial. Qed. -#[export] Instance: forall z, StrongRightCancellation (+) z. +#[export] Instance StrongRightCancellation_plus_field : forall z, StrongRightCancellation (+) z. Proof. intros. exact (strong_right_cancel_from_left (+)). Qed. -#[export] Instance: forall z, PropHolds (z ≶ 0) -> StrongLeftCancellation (.*.) z. +#[export] Instance StrongLeftCancellation_times_field : forall z, PropHolds (z ≶ 0) -> StrongLeftCancellation (.*.) z. Proof. intros z Ez x y E. red in Ez. rewrite !(commutativity z). @@ -104,7 +104,7 @@ rewrite <-!simple_associativity, !reciperse_alt. rewrite !mult_1_r;trivial. Qed. -#[export] Instance: forall z, PropHolds (z ≶ 0) -> StrongRightCancellation (.*.) z. +#[export] Instance StrongRightCancellation_times_field : forall z, PropHolds (z ≶ 0) -> StrongRightCancellation (.*.) z. Proof. intros. exact (strong_right_cancel_from_left (.*.)). Qed. @@ -130,7 +130,7 @@ rewrite <-simple_associativity, reciperse_alt, mult_1_r, mult_0_l. trivial. Qed. -Instance: NoZeroDivisors F. +Instance NoZeroDivisors_Field : NoZeroDivisors F. Proof. intros x [x_nonzero [y [y_nonzero E]]]. assert (~ ~ apart y 0) as Ey. @@ -142,9 +142,9 @@ assert (~ ~ apart y 0) as Ey. apply mult_0_l. Qed. -#[export] Instance : IsIntegralDomain F := {}. +#[export] Instance IsIntegralDomain_Field : IsIntegralDomain F := {}. -#[export] Instance apart_0_sig_apart_0: forall (x : ApartZero F), PropHolds (x.1 ≶ 0). +#[export] Instance apart_0_sig_apart_0 : forall (x : ApartZero F), PropHolds (x.1 ≶ 0). Proof. intros [??];trivial. Qed. @@ -296,7 +296,7 @@ Section morphisms. (* We have the following for morphisms to non-trivial strong rings as well. However, since we do not have an interface for strong rings, we ignore it. *) - #[export] Instance: IsStrongInjective f. + #[export] Instance IsStrongInjective_FieldHomomorphism : IsStrongInjective f. Proof. apply strong_injective_preserves_0. intros x Ex. diff --git a/theories/Classes/theory/naturals.v b/theories/Classes/theory/naturals.v index 295c8d173a..809ea2cc4f 100644 --- a/theories/Classes/theory/naturals.v +++ b/theories/Classes/theory/naturals.v @@ -76,7 +76,7 @@ Section retract_is_nat. Section for_another_semirings. Context `{IsSemiCRing R}. - Instance: IsSemiRingPreserving (naturals_to_semiring N R ∘ f^-1) := {}. + Instance IsSemiRingPreserving_naturals_to_semiring : IsSemiRingPreserving (naturals_to_semiring N R ∘ f^-1) := {}. Context (h : SR -> R) `{!IsSemiRingPreserving h}. @@ -144,7 +144,7 @@ Section borrowed_from_nat. simpl. intros [|x];eauto. Qed. - #[export] Instance: Biinduction N. + #[export] Instance biinduction_nat : Biinduction N. Proof. hnf. intros P E0 ES. apply induction;trivial. @@ -158,20 +158,20 @@ Section borrowed_from_nat. simpl. first [exact nat_plus_cancel_l@{U i}|exact nat_plus_cancel_l@{U}]. Qed. - #[export] Instance: forall z : N, RightCancellation (+) z. + #[export] Instance RightCancellation_plus_nat : forall z : N, RightCancellation (+) z. Proof. intro. exact (right_cancel_from_left (+)). Qed. - #[export] Instance: forall z : N, PropHolds (z <> 0) -> LeftCancellation (.*.) z. + #[export] Instance LeftCancellation_plus_nat : forall z : N, PropHolds (z <> 0) -> LeftCancellation (.*.) z. Proof. refine (from_nat_stmt nat (fun s => forall z : s, PropHolds (z <> 0) -> LeftCancellation mult z) _). simpl. exact nat_mult_cancel_l. Qed. - #[export] Instance: forall z : N, PropHolds (z <> 0) -> RightCancellation (.*.) z. + #[export] Instance RightCancellation_times_nat : forall z : N, PropHolds (z <> 0) -> RightCancellation (.*.) z. Proof. intros ? ?. exact (right_cancel_from_left (.*.)). Qed. - Instance nat_nontrivial: PropHolds ((1:N) <> 0). + Instance nat_nontrivial : PropHolds ((1:N) <> 0). Proof. refine (from_nat_stmt nat (fun s => PropHolds ((1:s) <> 0)) _). exact _. @@ -202,7 +202,7 @@ Section borrowed_from_nat. apply S_inj in E. destruct (S_neq_0 _ E). Qed. - #[export] Instance: ZeroProduct N. + #[export] Instance ZeroProduct_N : ZeroProduct N. Proof. refine (from_nat_stmt nat (fun s => ZeroProduct s) _). simpl. red. exact mult_eq_zero. diff --git a/theories/HIT/V.v b/theories/HIT/V.v index c71d8f9298..af1a950547 100644 --- a/theories/HIT/V.v +++ b/theories/HIT/V.v @@ -277,7 +277,7 @@ Defined. Notation "u ~~ v" := (bisimulation u v) : set_scope. -Instance reflexive_bisimulation : Reflexive bisimulation. +#[export] Instance reflexive_bisimulation : Reflexive bisimulation. Proof. refine (V_ind_hprop _ _ _). intros A f H_f. split. @@ -443,7 +443,7 @@ Defined. (** ** Two useful lemmas *) -Instance irreflexive_mem : Irreflexive mem. +#[export] Instance irreflexive_mem : Irreflexive mem. Proof. assert (forall v, IsHProp (complement (fun x x0 : V => x ∈ x0) v v)). (* https://coq.inria.fr/bugs/show_bug.cgi?id=3854 *) { intro. @@ -478,7 +478,7 @@ Definition V_empty : V := set (Empty_ind (fun _ => V)). (** The singleton {u} *) Definition V_singleton (u : V) : V@{U' U} := set (Unit_ind u). -Instance isequiv_ap_V_singleton {u v : V} +#[export] Instance isequiv_ap_V_singleton {u v : V} : IsEquiv (@ap _ _ V_singleton u v). Proof. simple refine (Build_IsEquiv _ _ _ _ _ _ _); try solve [ intro; apply path_ishprop ]. diff --git a/theories/HoTT.v b/theories/HoTT.v index ac5bae5dd0..881537b891 100644 --- a/theories/HoTT.v +++ b/theories/HoTT.v @@ -161,9 +161,11 @@ Require Export HoTT.Homotopy.HSpace. Require Export HoTT.Homotopy.ClassifyingSpace. Require Export HoTT.Homotopy.CayleyDickson. Require Export HoTT.Homotopy.EMSpace. +Require Export HoTT.Homotopy.ExactSequence. Require Export HoTT.Homotopy.HSpaceS1. Require Export HoTT.Homotopy.Bouquet. Require Export HoTT.Homotopy.EncodeDecode. +Require Export HoTT.Homotopy.SuccessorStructure. Require Export HoTT.Homotopy.Syllepsis. Require Export HoTT.Homotopy.Hopf. Require Export HoTT.Homotopy.IdentitySystems. diff --git a/theories/Spaces/Nat.v b/theories/Spaces/Nat.v index 9141d9b2cc..9d6f3b1aef 100644 --- a/theories/Spaces/Nat.v +++ b/theories/Spaces/Nat.v @@ -2,4 +2,6 @@ Require Export Nat.Core. Require Export Nat.Arithmetic. +Require Export Nat.Division. Require Export Nat.Paths. +Require Export Nat.Factorial. \ No newline at end of file diff --git a/theories/Universes/HSet.v b/theories/Universes/HSet.v index 8d00c2cde7..31209cfa8a 100644 --- a/theories/Universes/HSet.v +++ b/theories/Universes/HSet.v @@ -38,7 +38,7 @@ Proof. eapply path_ishprop. Defined. -Instance axiomK_isprop A : IsHProp (axiomK A) | 0. +#[export] Instance axiomK_isprop A : IsHProp (axiomK A) | 0. Proof. exact (istrunc_equiv_istrunc _ equiv_hset_axiomK). Defined.