Using new syntax for projection instance declarations

STYLE.md

@@ -509,22 +509,34 @@ IsTrunc n (P a)`, and similarly for other data types. For instance,
 
 ### 3.7. Coercions and Existing Instances
 
-A "coercion" from `A` to `B` is a function that Coq will insert
-silently if given an `A` when it expects a `B`, and which it doesn't
-display. For example, we have declared `equiv_fun` as a coercion from
-`A <~> B` to `A -> B`, so that we can use an equivalence as a function
-without needing to manually apply the projection `equiv_fun`.
-Coercions can make code easier to read and write, but when used
-carelessly they can have the opposite effect.
-
-When defining a `Record`, Coq allows you to declare a field as a
-coercion by writing its type with `:>` instead of `:`.
-When defining a `Class`, the `:>` notation has a
-different meaning: it declares a field as an `Existing Instance`.
-
-(In addition, the `:>` notation is used when needed for path types
-to indicate the type in which the paths are taken: `x = y :> A`
-for `x, y : A`.)
+A ["coercion" from `A` to
+`B`](https://rocq-prover.org/refman/addendum/implicit-coercions.html)
+is a function that Coq will insert silently if given an `A` when it
+expects a `B`, and which it doesn't display. For example, we have
+declared `equiv_fun` as a coercion from `A <~> B` to `A -> B`, so that
+we can use an equivalence as a function without needing to manually
+apply the projection `equiv_fun`. Coercions can make code easier to
+read and write, but when used carelessly they can have the opposite
+effect.
+
+When making a record field `proj1` into a coercion, we prefer that the
+coercion should not be reversible, because of the additional
+complexity that reversible coercions add to unification problems, and
+we prefer that coercions be conspicuous when reading the source code.
+Therefore, define the coercion on its own line after the record
+declaration as `Coercion proj1 : MyRec >-> FieldType` rather than
+using the reversible coercion syntax `proj1 :> FieldType`.
+
+(This library also uses the `:>` notation when needed for path types
+to indicate the type in which the paths are taken: `x = y :> A` for
+`x, y : A`.)
+
+If `proj1` is a record field whose type is a typeclass and we'd
+like to add this field as a typeclass instance, then we prefer
+the concise ["substructure"
+notation](https://rocq-prover.org/refman/addendum/type-classes.html#substructures)
+`proj1 :: ClassType` over the separate vernacular command
+`Existing Instance proj1.` after the record declaration.
 
 ## 4. Axioms
 

theories/Algebra/AbGroups/AbelianGroup.v

@@ -18,11 +18,10 @@ Local Open Scope mc_add_scope.
 
 Record AbGroup := {
   abgroup_group : Group;
-  abgroup_commutative : @Commutative abgroup_group _ (+);
+  abgroup_commutative :: @Commutative abgroup_group _ (+);
 }.
 
 Coercion abgroup_group : AbGroup >-> Group.
-Existing Instance abgroup_commutative.
 
 Definition zero_abgroup (A : AbGroup) : Zero A := mon_unit.
 Definition negate_abgroup (A : AbGroup) : Negate A := inv.

theories/Algebra/AbGroups/Abelianization.v

@@ -21,9 +21,8 @@ Definition group_precomp {a b} := @cat_precomp Group _ _ a b.
 
 Class IsAbelianization {G : Group} (G_ab : AbGroup)
       (eta : GroupHomomorphism G G_ab)
-  := issurjinj_isabel : forall (A : AbGroup),
+  := issurjinj_isabel :: forall (A : AbGroup),
       IsSurjInj (group_precomp A eta).
-Existing Instance issurjinj_isabel.
 
 Definition isequiv_group_precomp_isabelianization `{Funext}
   {G : Group} {G_ab : AbGroup} (eta : GroupHomomorphism G G_ab)

theories/Algebra/AbGroups/FreeAbelianGroup.v

@@ -13,9 +13,8 @@ Definition FactorsThroughFreeAbGroup (S : Type) (F_S : AbGroup)
 
 (** Universal property of a free abelian group on a set (type). *)
 Class IsFreeAbGroupOn (S : Type) (F_S : AbGroup) (i : S -> F_S)
-  := contr_isfreeabgroupon : forall (A : AbGroup) (g : S -> A),
+  := contr_isfreeabgroupon :: forall (A : AbGroup) (g : S -> A),
       Contr (FactorsThroughFreeAbGroup S F_S i A g).
-Existing Instance contr_isfreeabgroupon.
 
 (** A abelian group is free if there exists a generating type on which it is a free group (a basis). *)
 Class IsFreeAbGroup (F_S : AbGroup)

theories/Algebra/AbSES/Core.v

@@ -22,16 +22,14 @@ Record AbSES' {B A : AbGroup@{u}} := Build_AbSES {
     middle :  AbGroup@{u};
     inclusion : A $-> middle;
     projection : middle $-> B;
-    isembedding_inclusion : IsEmbedding inclusion;
-    issurjection_projection : IsSurjection projection;
-    isexact_inclusion_projection : IsExact (Tr (-1)) inclusion projection;
+    isembedding_inclusion :: IsEmbedding inclusion;
+    issurjection_projection :: IsSurjection projection;
+    isexact_inclusion_projection :: IsExact (Tr (-1)) inclusion projection;
   }.
 
 (** Given a short exact sequence [A -> E -> B : AbSES B A], we coerce it to [E]. *)
 Coercion middle : AbSES' >-> AbGroup.
 
-Existing Instances isembedding_inclusion issurjection_projection isexact_inclusion_projection.
-
 Arguments AbSES' B A : clear implicits.
 Arguments Build_AbSES {B A}.
 

theories/Algebra/Groups/Group.v

@@ -1153,9 +1153,8 @@ Definition FactorsThroughFreeGroup (S : Type) (F_S : Group)
 
 (** Universal property of a free group on a set (type). *)
 Class IsFreeGroupOn (S : Type) (F_S : Group) (i : S -> F_S)
-  := contr_isfreegroupon : forall (A : Group) (g : S -> A),
+  := contr_isfreegroupon :: forall (A : Group) (g : S -> A),
       Contr (FactorsThroughFreeGroup S F_S i A g).
-Existing Instance contr_isfreegroupon.
 
 (** A group is free if there exists a generating type on which it is a free group. *)
 Class IsFreeGroup (F_S : Group)

theories/Algebra/Groups/Subgroup.v

@@ -14,14 +14,12 @@ Generalizable Variables G H A B C N f g.
 
 (** A subgroup H of a group G is a predicate (i.e. an hProp-valued type family) on G which is closed under the group operations. The group underlying H is given by the total space { g : G & H g }, defined in [subgroup_group] below. *)
 Class IsSubgroup {G : Group} (H : G -> Type) := {
-  issubgroup_predicate : forall x, IsHProp (H x) ;
+  issubgroup_predicate :: forall x, IsHProp (H x) ;
   issubgroup_in_unit : H mon_unit ;
   issubgroup_in_op : forall x y, H x -> H y -> H (x * y) ;
   issubgroup_in_inv : forall x, H x -> H x^ ;
 }.
 
-Existing Instance issubgroup_predicate.
-
 Definition issig_issubgroup {G : Group} (H : G -> Type) : _ <~> IsSubgroup H
   := ltac:(issig).
 
@@ -130,11 +128,10 @@ Defined.
 (** The type (set) of subgroups of a group G. *)
 Record Subgroup (G : Group) := {
   subgroup_pred : G -> Type ;
-  subgroup_issubgroup : IsSubgroup subgroup_pred ;
+  subgroup_issubgroup :: IsSubgroup subgroup_pred ;
 }.
 
 Coercion subgroup_pred : Subgroup >-> Funclass.
-Existing Instance subgroup_issubgroup.
 
 Definition issig_subgroup {G : Group} : _ <~> Subgroup G
   := ltac:(issig).
@@ -442,13 +439,12 @@ Class IsNormalSubgroup {G : Group} (N : Subgroup G)
 
 Record NormalSubgroup (G : Group) := {
   normalsubgroup_subgroup : Subgroup G ;
-  normalsubgroup_isnormal : IsNormalSubgroup normalsubgroup_subgroup ;
+  normalsubgroup_isnormal :: IsNormalSubgroup normalsubgroup_subgroup ;
 }.
 
 Arguments Build_NormalSubgroup G N _ : rename.
 
 Coercion normalsubgroup_subgroup : NormalSubgroup >-> Subgroup.
-Existing Instance normalsubgroup_isnormal.
 
 Definition equiv_symmetric_in_normalsubgroup {G : Group}
   (N : Subgroup G) `{!IsNormalSubgroup N}

theories/Algebra/Rings/Ring.v

@@ -33,7 +33,6 @@ Record Ring := Build_Ring' {
   ring_mult_assoc_opp : forall z y x, (x * y) * z = x * (y * z);
 }.
 
-
 Arguments ring_mult {R} : rename.
 Arguments ring_one {R} : rename.
 Arguments ring_isring {R} : rename.
@@ -144,12 +143,11 @@ End RingHomoLaws.
 (** Isomorphisms of commutative rings *)
 Record RingIsomorphism (A B : Ring) := {
   rng_iso_homo : RingHomomorphism A B ;
-  isequiv_rng_iso_homo : IsEquiv rng_iso_homo ;
+  isequiv_rng_iso_homo :: IsEquiv rng_iso_homo ;
 }.
 
 Arguments rng_iso_homo {_ _ }.
 Coercion rng_iso_homo : RingIsomorphism >-> RingHomomorphism.
-Existing Instance isequiv_rng_iso_homo.
 
 Definition issig_RingIsomorphism {A B : Ring}
   : _ <~> RingIsomorphism A B := ltac:(issig).

theories/Algebra/Universal/Algebra.v

@@ -38,15 +38,11 @@ Record Signature := Build_Signature
   { Sort : Type
   ; Symbol : Type
   ; symbol_types : Symbol -> SymbolTypeOf Sort
-  ; hset_sort : IsHSet Sort
-  ; hset_symbol : IsHSet Symbol }.
+  ; hset_sort :: IsHSet Sort
+  ; hset_symbol :: IsHSet Symbol }.
 
 Notation SymbolType σ := (SymbolTypeOf (Sort σ)).
 
-Existing Instance hset_sort.
-
-Existing Instance hset_symbol.
-
 Global Coercion symbol_types : Signature >-> Funclass.
 
 (** Each [Algebra] has a collection of carrier types [Carriers σ],
@@ -81,14 +77,12 @@ Definition Operation {σ} (A : Carriers σ) (w : SymbolType σ) : Type
 Record Algebra {σ : Signature} : Type := Build_Algebra
   { carriers : Carriers σ
   ; operations : forall (u : Symbol σ), Operation carriers (σ u)
-  ; hset_algebra : forall (s : Sort σ), IsHSet (carriers s) }.
+  ; hset_algebra :: forall (s : Sort σ), IsHSet (carriers s) }.
 
 Arguments Algebra : clear implicits.
 
 Arguments Build_Algebra {σ} carriers operations {hset_algebra}.
 
-Existing Instance hset_algebra.
-
 Global Coercion carriers : Algebra >-> Funclass.
 
 Bind Scope Algebra_scope with Algebra.

theories/Algebra/Universal/Congruence.v

@@ -53,20 +53,14 @@ Section congruence.
       mere equivalence relations and [OpsCompatible A Φ] holds. *)
 
   Class IsCongruence : Type := Build_IsCongruence
-   { is_mere_relation_cong : forall (s : Sort σ), is_mere_relation (A s) (Φ s)
-   ; equiv_rel_cong : forall (s : Sort σ), EquivRel (Φ s)
-   ; ops_compatible_cong : OpsCompatible }.
+   { is_mere_relation_cong :: forall (s : Sort σ), is_mere_relation (A s) (Φ s)
+   ; equiv_rel_cong :: forall (s : Sort σ), EquivRel (Φ s)
+   ; ops_compatible_cong :: OpsCompatible }.
 
   Global Arguments Build_IsCongruence {is_mere_relation_cong}
                                       {equiv_rel_cong}
                                       {ops_compatible_cong}.
 
-  #[export] Existing Instance is_mere_relation_cong.
-
-  #[export] Existing Instance equiv_rel_cong.
-
-  #[export] Existing Instance ops_compatible_cong.
-
   #[export] Instance hprop_is_congruence `{Funext} : IsHProp IsCongruence.
   Proof.
     apply (equiv_hprop_allpath _)^-1.

theories/Algebra/Universal/Homomorphism.v

@@ -38,16 +38,14 @@ End is_homomorphism.
 
 Record Homomorphism {σ} {A B : Algebra σ} : Type := Build_Homomorphism
   { def_homomorphism : forall (s : Sort σ), A s -> B s
-  ; is_homomorphism : IsHomomorphism def_homomorphism }.
+  ; is_homomorphism :: IsHomomorphism def_homomorphism }.
 
 Arguments Homomorphism {σ}.
 
 Arguments Build_Homomorphism {σ A B} def_homomorphism {is_homomorphism}.
 
 Global Coercion def_homomorphism : Homomorphism >-> Funclass.
 
-Existing Instance is_homomorphism.
-
 Instance isgraph_algebra (σ : Signature) : IsGraph (Algebra σ)
   := Build_IsGraph (Algebra σ) Homomorphism.
 

theories/Algebra/ooGroup.v

@@ -20,11 +20,9 @@ Local Unset Keyed Unification.
 
 Record ooGroup :=
   { classifying_space : pType ;
-    isconn_classifying_space : IsConnected 0 classifying_space
+    isconn_classifying_space :: IsConnected 0 classifying_space
   }.
 
-Existing Instance isconn_classifying_space.
-
 Local Notation B := classifying_space.
 
 Definition group_type (G : ooGroup) : Type

theories/Basics/Decidable.v

@@ -67,8 +67,7 @@ Ltac decidable_false p n :=
   try intro.
 
 Class DecidablePaths (A : Type) :=
-  dec_paths : forall (x y : A), Decidable (x = y).
-Existing Instance dec_paths.
+  dec_paths :: forall (x y : A), Decidable (x = y).
 
 Class Stable P := stable : ~~P -> P.
 
@@ -199,13 +198,11 @@ Defined.
 (** A type is collapsible if it admits a weakly constant endomap. *)
 Class Collapsible (A : Type) :=
   { collapse : A -> A ;
-    wconst_collapse : WeaklyConstant collapse
+    wconst_collapse :: WeaklyConstant collapse
   }.
-Existing Instance wconst_collapse.
 
 Class PathCollapsible (A : Type) :=
-  path_coll : forall (x y : A), Collapsible (x = y).
-Existing Instance path_coll.
+  path_coll :: forall (x y : A), Collapsible (x = y).
 
 Instance collapsible_decidable (A : Type) `{Decidable A}
 : Collapsible A.

theories/Basics/Overture.v

@@ -92,11 +92,8 @@ Class Transitive {A} (R : Relation A) :=
 
 (** A [PreOrder] is both Reflexive and Transitive. *)
 Class PreOrder {A} (R : Relation A) :=
-  { PreOrder_Reflexive : Reflexive R | 2 ;
-    PreOrder_Transitive : Transitive R | 2 }.
-
-Existing Instance PreOrder_Reflexive.
-Existing Instance PreOrder_Transitive.
+  { PreOrder_Reflexive :: Reflexive R | 2 ;
+    PreOrder_Transitive :: Transitive R | 2 }.
 
 Arguments reflexivity {A R _} / _.
 Arguments symmetry {A R _} / _ _ _.
@@ -488,13 +485,11 @@ Global Opaque eisadj.
 (** A record that includes all the data of an adjoint equivalence. *)
 Record Equiv A B := {
   equiv_fun : A -> B ;
-  equiv_isequiv : IsEquiv equiv_fun
+  equiv_isequiv :: IsEquiv equiv_fun
 }.
 
 Coercion equiv_fun : Equiv >-> Funclass.
 
-Existing Instance equiv_isequiv.
-
 Arguments equiv_fun {A B} _ _.
 Arguments equiv_isequiv {A B} _.
 
@@ -728,12 +723,10 @@ Arguments point A {_}.
 
 Record pType :=
   { pointed_type : Type ;
-    ispointed_type : IsPointed pointed_type }.
+    ispointed_type :: IsPointed pointed_type }.
 
 Coercion pointed_type : pType >-> Sortclass.
 
-Existing Instance ispointed_type.
-
 (** *** Homotopy fibers *)
 
 (** Homotopy fibers are homotopical inverse images of points.  *)

theories/Basics/Trunc.v

@@ -378,9 +378,7 @@ Definition istrunc_equiv_istrunc A {B} (f : A <~> B) `{IsTrunc n A}
 (** ** Truncated morphisms *)
 
 Class IsTruncMap (n : trunc_index) {X Y : Type} (f : X -> Y)
-  := istruncmap_fiber : forall y:Y, IsTrunc n (hfiber f y).
-
-Existing Instance istruncmap_fiber.
+  := istruncmap_fiber :: forall y:Y, IsTrunc n (hfiber f y).
 
 Notation IsEmbedding := (IsTruncMap (-1)).
 
@@ -390,15 +388,14 @@ Notation IsEmbedding := (IsTruncMap (-1)).
 
 Record TruncType (n : trunc_index) := {
   trunctype_type : Type ;
-  trunctype_istrunc : IsTrunc n trunctype_type
+  trunctype_istrunc :: IsTrunc n trunctype_type
 }.
 
 Arguments Build_TruncType _ _ {_}.
 Arguments trunctype_type {_} _.
 Arguments trunctype_istrunc [_] _.
 
 Coercion trunctype_type : TruncType >-> Sortclass.
-Existing Instance trunctype_istrunc.
 
 Notation "n -Type" := (TruncType n) : type_scope.
 Notation HProp := (-1)-Type.

theories/Categories/Category/Core.v

@@ -71,7 +71,7 @@ Record PreCategory :=
       (** Ask for the double-identity version so that [InitialTerminalCategory.Functors.from_terminal Cᵒᵖ X] and [(InitialTerminalCategory.Functors.from_terminal C X)ᵒᵖ] are convertible. *)
       identity_identity : forall x, identity x o identity x = identity x;
 
-      trunc_morphism : forall s d, IsHSet (morphism s d)
+      trunc_morphism :: forall s d, IsHSet (morphism s d)
     }.
 
 Bind Scope category_scope with PreCategory.
@@ -106,8 +106,6 @@ Definition Build_PreCategory
        right_identity
        (fun _ => left_identity _ _ _).
 
-Existing Instance trunc_morphism.
-
 (** create a hint db for all category theory things *)
 Create HintDb category discriminated.
 (** create a hint db for morphisms in categories *)