Merge pull request #2254 from patrick-nicodemus/tc_fixes

Typeclass hints

Author: Alizter

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).

theories/Classes/orders/lattices.v

@@ -279,15 +279,15 @@ 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.
   - apply meet_lb_l.
   - 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.

theories/Classes/orders/nat_int.v

@@ -147,15 +147,15 @@ 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].
   rewrite E, (preserves_plus (f:=f)), (naturals.to_semiring_twice f _ _).
   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].

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.

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.

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.

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 stable_eq_apartness: forall x y : A, Stable (x = y).
 Proof.
   intros x y. unfold Stable.
   intros dn. apply tight_apart.

theories/Classes/theory/fields.v

@@ -52,7 +52,7 @@ Proof.
 intros ? E. rewrite <-E. trivial.
 Qed.
 
-#[export] Instance: IsStrongInjective (-).
+#[export] Instance isstronginjective_negation_field: 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_recip_field: IsStrongInjective (//).
 Proof.
 repeat (split; try exact _); intros x y E.
 - apply (strong_extensionality (x.1 *.)).
@@ -82,20 +82,20 @@ 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 _),
   <-simple_associativity,right_inverse,plus_0_r.
 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_mult_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_mult_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_field_homomorphism : IsStrongInjective f.
   Proof.
   apply strong_injective_preserves_0.
   intros x Ex.

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_mult_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_nat : ZeroProduct N.
   Proof.
   refine (from_nat_stmt nat (fun s => ZeroProduct s) _).
   simpl. red. exact mult_eq_zero.

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 ].