Merge pull request #9 from coq-community/compat-8.20

Compatibility with Coq 8.20

Author: palmskog

.github/workflows/docker-action.yml

@@ -18,6 +18,7 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.20'
           - 'coqorg/coq:8.19'
           - 'coqorg/coq:8.18'
           - 'coqorg/coq:8.17'

Hierarchy/Type_class_definition.v

@@ -38,120 +38,147 @@ Definition scalar A B := A -> B -> B.
 Definition value A := A -> R.
 
 Class Metric_Space (A : Type) (eqA : relation A) (d : A -> A -> R) := {
-  metric_space_setoid :> Equivalence eqA ;
+  metric_space_setoid : Equivalence eqA ;
   metric_space_positive : forall x y : A, 0 <= d x y ;
   metric_space_symmetry : forall x y : A, d x y = d y x ;
   metric_space_separation : forall x y : A, (0 = d x y -> eqA x y) /\ (eqA x y -> 0 = d x y);
   metric_space_triangular_inequality : forall x y z : A, d x z <= (d x y) + (d y z)
 }.
+#[global] Existing Instance metric_space_setoid.
 
 Class Monoid (M : Type) (eqM : relation M) (f : operation M) (eps : M) := {
-  monoid_setoid :> Equivalence eqM ;
+  monoid_setoid : Equivalence eqM ;
   monoid_iden_l : forall x : M, eqM (f eps x) x ;
   monoid_iden_r : forall x : M, eqM (f x eps) x ;
-  monoid_assoc :> Associative eqM f;
+  monoid_assoc : Associative eqM f;
   monoid_eq_compat_l : forall x y z : M, eqM y z -> eqM (f x y) (f x z);
   monoid_eq_compat_r: forall x y z : M, eqM x y -> eqM (f x z) (f y z)
 }.
+#[global] Existing Instance monoid_setoid.
+#[global] Existing Instance monoid_assoc.
 
 Class Monoid_Commutative (M : Type) (eqM : relation M) (f : operation M) (eps : M) := {
-  monoid_comm_monoid :> Monoid M eqM f eps ;
-  monoid_comm :> Commutative eqM f
+  monoid_comm_monoid : Monoid M eqM f eps ;
+  monoid_comm : Commutative eqM f
 }.
+#[global] Existing Instance monoid_comm_monoid.
+#[global] Existing Instance monoid_comm.
 
 Class Group (G : Type) (eqG : relation G) (f : operation G) (eps : G) := {
-  group_monoid :> Monoid G eqG f eps;
+  group_monoid : Monoid G eqG f eps;
   group_reverse : forall x : G, sig (fun y => eqG (f x y) eps)
 }.
+#[global] Existing Instance group_monoid.
 
 Class Group_Commutative (G : Type) (eqG : relation G) (f : operation G) (eps : G) := {
-  group_comm_group :> Group G eqG f eps ;
-  group_comm :> Commutative eqG f
+  group_comm_group : Group G eqG f eps ;
+  group_comm : Commutative eqG f
 }.
+#[global] Existing Instance group_comm_group.
+#[global] Existing Instance group_comm.
 
 Class Group_Multiplicative (G : Type) (eqG : relation G) (mult : operation G) (eps0 : G) (eps1 : G) := {
-  group_setoid :> Equivalence eqG ;
+  group_setoid : Equivalence eqG ;
   group_multiplicative_iden_l : forall x : G, eqG (mult eps1 x) x ;
   group_multiplicative_iden_r : forall x : G, eqG (mult x eps1) x ;
   group_multiplicative_reverse : forall x : G, ~(eqG x eps0) -> sig (fun y => eqG (mult x y) eps1);
-  group_multiplicative_assoc :> Associative eqG mult;
+  group_multiplicative_assoc : Associative eqG mult;
   group_multiplicative_eq_compat_l : forall x y z : G, eqG y z -> eqG (mult x y) (mult x z);
   group_multiplicative_eq_compat_r: forall x y z : G, eqG x y -> eqG (mult x z) (mult y z)
 }.
+#[global] Existing Instance group_setoid.
+#[global] Existing Instance group_multiplicative_assoc.
 
 Class SemiRing (S : Type) (eqS : relation S) (add : operation S) (mult : operation S) (eps0 : S) (eps1 : S) := {
-  semiring_monoid_comm :> Monoid_Commutative S eqS add eps0 ;
-  semiring_monoid :> Monoid S eqS mult eps1 ;
+  semiring_monoid_comm : Monoid_Commutative S eqS add eps0 ;
+  semiring_monoid : Monoid S eqS mult eps1 ;
   semiring_distributive_r : forall x y z : S, eqS (mult x (add y z)) (add (mult x y) (mult x z)) ;
   semiring_distributive_l : forall x y z : S, eqS (mult (add x y) z) (add (mult x z) (mult y z)) ;
   semiring_absorption_r : forall x : S, eqS (mult x eps0) eps0 ;
   semiring_absorption_l : forall x : S, eqS (mult eps0 x) eps0
 }.
+#[global] Existing Instance semiring_monoid_comm.
+#[global] Existing Instance semiring_monoid.
 
 Class SemiRing_Commutative (S : Type) (eqS : relation S) (add : operation S) (mult : operation S) (eps0 : S) (eps1 : S) := {
-  semiring_comm_semiring :> SemiRing S eqS add mult eps0 eps1 ;
-  semiring_comm :> Commutative eqS mult
+  semiring_comm_semiring : SemiRing S eqS add mult eps0 eps1 ;
+  semiring_comm : Commutative eqS mult
 }.
+#[global] Existing Instance semiring_comm_semiring.
+#[global] Existing Instance semiring_comm.
 
 Class Ring (R : Type) (eqR : relation R) (add : operation R) (mult : operation R) (eps0 : R) (eps1 : R) := {
-  ring_group_comm :> Group_Commutative R eqR add eps0 ;
-  ring_monoid :> Monoid R eqR mult eps1 ;
+  ring_group_comm : Group_Commutative R eqR add eps0 ;
+  ring_monoid : Monoid R eqR mult eps1 ;
   ring_distributive_r : forall x y z : R, eqR (mult x (add y z)) (add (mult x y) (mult x z)) ;
   ring_distributive_l : forall x y z : R, eqR (mult (add x y) z) (add (mult x z) (mult y z))
 }.
+#[global] Existing Instance ring_group_comm.
+#[global] Existing Instance ring_monoid.
 
 Class Ring_Commutative (R : Type) (eqR : relation R) (add : operation R) (mult : operation R) (eps0 : R) (eps1 : R) := {
-  ring_comm_ring :> Ring R eqR add mult eps0 eps1 ;
-  ring_comm :> Commutative eqR mult
+  ring_comm_ring : Ring R eqR add mult eps0 eps1 ;
+  ring_comm : Commutative eqR mult
 }.
+#[global] Existing Instance ring_comm_ring.
+#[global] Existing Instance ring_comm.
 
 Class Field (F : Type) (eqF : relation F) (add : operation F) (mult : operation F) (eps0 : F) (eps1 : F) := {
-  field_group_comm :> Group_Commutative F eqF add eps0 ;
-  field_group_multiplicative :> Group_Multiplicative F eqF mult eps0 eps1 ;
+  field_group_comm : Group_Commutative F eqF add eps0 ;
+  field_group_multiplicative : Group_Multiplicative F eqF mult eps0 eps1 ;
   field_distributive_r : forall x y z : F, eqF (mult x (add y z)) (add (mult x y) (mult x z)) ;
   field_distributive_l : forall x y z : F, eqF (mult (add x y) z) (add (mult x z) (mult y z))
 }.
+#[global] Existing Instance field_group_comm.
+#[global] Existing Instance field_group_multiplicative.
 
 Class Field_Commutative (F : Type) (eqF : relation F) (add : operation F) (mult : operation F) (eps0 : F) (eps1 : F) := {
-  field_comm_field :> Field F eqF add mult eps0 eps1 ;
-  field_comm :> Commutative eqF mult
+  field_comm_field : Field F eqF add mult eps0 eps1 ;
+  field_comm : Commutative eqF mult
 }.
+#[global] Existing Instance field_comm_field.
+#[global] Existing Instance field_comm.
 
 Class Field_Valued (F : Type) (eqF : relation F) (add : operation F) (mult : operation F) (eps0 : F) (eps1 : F) (abs : value F) := {
-  field_valued_field_commutative :> Field_Commutative F eqF add mult eps0 eps1 ;
+  field_valued_field_commutative : Field_Commutative F eqF add mult eps0 eps1 ;
   field_valued_positive : forall x : F, 0 <= (abs x) ;
   field_valued_separation : (abs eps0) = 0 /\ forall x : F, (abs x) = 0 -> eqF x eps0 ;
   field_valued_triangular_inequality : forall x y : F, abs (add x y) <= (abs x) + (abs y);
   field_valued_homogeneity : forall x y : F, abs (mult x y) = (abs x) * (abs y)
 }.
+#[global] Existing Instance field_valued_field_commutative.
 
 Class Vector_Space (E : Type) (eqE : relation E) (F : Type) (eqF : relation F)
                                  (v_add : operation E) (v_mult : scalar F E)
                                  (add : operation F) (mult : operation F)
                                  (v_null : E)
                                  (eps0 : F) (eps1 : F):= {
-  vector_space_field :> Field_Commutative F eqF add mult eps0 eps1 ;
-  vector_space_group_comm :> Group_Commutative E eqE v_add v_null ;
+  vector_space_field : Field_Commutative F eqF add mult eps0 eps1 ;
+  vector_space_group_comm : Group_Commutative E eqE v_add v_null ;
   vector_space_distributive_r : forall a : F, forall x y : E, eqE (v_mult a (v_add x y)) (v_add (v_mult a x) (v_mult a y)) ;
   vector_space_distributive_l : forall a b : F, forall x : E, eqE (v_mult (add a b) x) (v_add (v_mult a x) (v_mult b x)) ;
   vector_space_assoc : forall a b : F, forall x : E, eqE (v_mult (mult a b) x) (v_mult a (v_mult b x)) ;
   vector_space_iden_l : forall a : F, forall x : E, eqE (v_mult eps1 x) x;
   vector_space_eq_compat_l : forall a : F, forall x y :E, eqE x y -> eqE (v_mult a x) (v_mult a y);
   vector_space_eq_compat_r : forall a b : F, forall x : E, eqF a b -> (eqE (v_mult a x) (v_mult b x))
 }.
+#[global] Existing Instance vector_space_field.
+#[global] Existing Instance vector_space_group_comm.
 
 Class Vector_Space_Normed (E : Type) (eqE : relation E) (F : Type) (eqF : relation F)
                                  (v_add : operation E) (v_mult : scalar F E)
                                  (add : operation F) (mult : operation F)
                                  (v_null : E)
                                  (eps0 : F) (eps1 : F)
                                  (norm: value E) (abs : value F) := {
-  vector_space_normed_field_valued :> Field_Valued F eqF add mult eps0 eps1 abs ;
-  vector_space_normed_vector_space :> Vector_Space E eqE F eqF v_add v_mult add mult v_null eps0 eps1 ;
+  vector_space_normed_field_valued : Field_Valued F eqF add mult eps0 eps1 abs ;
+  vector_space_normed_vector_space : Vector_Space E eqE F eqF v_add v_mult add mult v_null eps0 eps1 ;
   vector_space_normed_separation : forall v : E, (norm v) = 0 -> eqE v v_null ;
   vector_space_normed_triangular_inequality : forall v w : E, norm (v_add v w) <= (norm v) + (norm w) ;
   vector_space_normed_homogeneity : forall x : F, forall v : E, norm (v_mult x v) = (abs x) * (norm v)
 }.
+#[global] Existing Instance vector_space_normed_field_valued.
+#[global] Existing Instance vector_space_normed_vector_space.
 
 Close Scope R_scope.
 
@@ -168,4 +195,4 @@ Hint Rewrite
   @monoid_eq_compat_r
   @op_assoc
   @op_comm
-: typeclass.*)
+: typeclass.*)

meta.yml

@@ -42,6 +42,7 @@ tested_coq_nix_versions:
 
 tested_coq_opam_versions:
 - version: dev
+- version: '8.20'
 - version: '8.19'
 - version: '8.18'
 - version: '8.17'