Adapt to rocq-prover/rocq#18590

Author: proux01

.github/workflows/docker-action.yml

@@ -18,11 +18,8 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.19'
           - 'coqorg/coq:8.18'
-          - 'coqorg/coq:8.17'
-          - 'coqorg/coq:8.16'
-          - 'coqorg/coq:8.15'
-          - 'coqorg/coq:8.14'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3

README.md

@@ -9,8 +9,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [![Code of Conduct][conduct-shield]][conduct-link]
 [![Zulip][zulip-shield]][zulip-link]
 
-[docker-action-shield]: https://github.com/coq-community/corn/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/coq-community/corn/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/coq-community/corn/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/corn/actions/workflows/docker-action.yml
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
@@ -87,7 +87,7 @@ CoRN includes the following parts:
   - Bas Spitters ([**@spitters**](https://github.com/spitters))
   - Vincent Semeria ([**@vincentse**](https://github.com/vincentse))
 - License: [GNU General Public License v2](LICENSE)
-- Compatible Coq versions: Coq 8.14 or greater
+- Compatible Coq versions: Coq 8.18 or greater
 - Additional dependencies:
   - [Math-Classes](https://github.com/coq-community/math-classes) 8.8.1 or
 greater, which is a library of abstract interfaces for mathematical

algebra/RSetoid.v

@@ -25,7 +25,9 @@ Set Warnings "-unsupported-attributes".
 Set Implicit Arguments.
 
 Require Export Coq.Setoids.Setoid.
+Require Export (hints) MathClasses.interfaces.orders.
 Require Import MathClasses.interfaces.abstract_algebra.
+Export (hints) MathClasses.interfaces.abstract_algebra.
 
 (**
 * Classic Setoids presented in a bundled way. 

classes/Qclasses.v

@@ -1,5 +1,6 @@
 Require Import 
   CoRN.model.totalorder.QMinMax
+  MathClasses.interfaces.orders
   MathClasses.interfaces.abstract_algebra
   MathClasses.orders.minmax.
 Require Export 

coq-corn.opam

@@ -46,7 +46,7 @@ build: [
 ]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.14" & < "8.19~") | (= "dev")}
+  "coq" {(>= "8.18" & < "8.20~") | (= "dev")}
   "coq-math-classes" {(>= "8.8.1") | (= "dev")}
   "coq-bignums" 
 ]

meta.yml

@@ -79,16 +79,13 @@ license:
   identifier: GPL-2.0
 
 supported_coq_versions:
-  text: Coq 8.14 or greater
-  opam: '{(>= "8.14" & < "8.19~") | (= "dev")}'
+  text: Coq 8.18 or greater
+  opam: '{(>= "8.18" & < "8.20~") | (= "dev")}'
 
 tested_coq_opam_versions:
 - version: dev
+- version: "8.19"
 - version: "8.18"
-- version: "8.17"
-- version: "8.16"
-- version: "8.15"
-- version: "8.14"
 
 dependencies:
 - opam:

metric2/Classified.v

@@ -46,12 +46,12 @@ Hint Unfold relation : type_classes.
   Context `{!MetricSpaceBall}.
 
   Class MetricSpaceClass: Prop :=
-    { mspc_ball_proper:> forall (e1 e2 : Qinf) (x y : X),
+    { mspc_ball_proper:: forall (e1 e2 : Qinf) (x y : X),
           equiv e1 e2 -> (mspc_ball e1 x y <-> mspc_ball e2 x y)
     ; mspc_ball_inf: ∀ x y, mspc_ball Qinf.infinite x y
     ; mspc_ball_negative: ∀ (e: Q), (e < 0)%Q → ∀ x y, ~ mspc_ball e x y
-    ; mspc_refl:> ∀ e, (0 <= e)%Qinf → Reflexive (mspc_ball e)
-    ; mspc_sym:> ∀ e, Symmetric (mspc_ball e)
+    ; mspc_refl:: ∀ e, (0 <= e)%Qinf → Reflexive (mspc_ball e)
+    ; mspc_sym:: ∀ e, Symmetric (mspc_ball e)
     ; mspc_triangle: ∀ (e1 e2: Qinf) (a b c: X),
          mspc_ball e1 a b → mspc_ball e2 b c → mspc_ball (e1 + e2) a c
     ; mspc_closed: ∀ (e: Qinf) (a b: X),
@@ -665,7 +665,7 @@ Section local_uniform_continuity.
     := f ∘ @proj1_sig _ _.
 
   Class LocallyUniformlyContinuous_mu (f: X → Y): Type :=
-    luc_mu (b: Ball X Qpos):> UniformlyContinuous_mu (restrict b f).
+    luc_mu (b: Ball X Qpos):: UniformlyContinuous_mu (restrict b f).
 
   Context (f: X → Y) {mu: LocallyUniformlyContinuous_mu f}.
 

metric2/MetricMorphisms.v

@@ -63,7 +63,7 @@ Arguments app_inverse {X Y} f {AppInverse}.
 
 Class DenseEmbedding `{Equiv X} {Y : MetricSpace} (f : X → Y) `{!AppInverse f} := {
   dense_embed_setoid : Setoid X ;
-  dense_injective :> Injective f ;
+  dense_injective :: Injective f ;
   dense_inverse : ∀ x (ε:Qpos), ball (proj1_sig ε) (f (app_inverse f x ε)) x
 }.
 

model/setoids/decsetoid.v

@@ -20,7 +20,7 @@ Class Apartness `{SetoidClass.Setoid} (ap: Crelation A): Type :=
 
 Class CSetoid_class `(Setoid): Type :=
   { apart: Crelation A
-  ; csetoid_apart:> Apartness apart
+  ; csetoid_apart :: Apartness apart
   }.
 
 Definition is_CSetoid_from_class `{Apartness}: is_CSetoid _ equiv ap0.

ode/AbstractIntegration.v

@@ -22,7 +22,6 @@ Require CoRN.reals.fast.CRtrans CoRN.reals.faster.ARtrans. (* This is almost all
 
 Import Qinf.coercions QnonNeg.coercions QnnInf.coercions CoRN.stdlib_omissions.Q.
 
-
 Ltac done :=
   trivial; hnf; intros; solve
    [ repeat (first [solve [trivial | apply: sym_equal; trivial]

ode/FromMetric2.v

@@ -5,7 +5,7 @@ Require Import CoRN.metric2.Complete CoRN.metric2.Metric CoRN.ode.metric.
 
 Require Import
   CoRN.model.totalorder.QposMinMax
-  MathClasses.interfaces.abstract_algebra MathClasses.implementations.stdlib_rationals
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.rationals MathClasses.implementations.stdlib_rationals
   MathClasses.orders.orders MathClasses.orders.semirings MathClasses.orders.rings MathClasses.theory.rings.
 
 Import Qinf.notations Qinf.coercions.
@@ -211,11 +211,13 @@ Lemma nested_balls (x1 x2 : Q) {y1 y2 : Q} {e : Qinf} :
 Proof.
 intros B A1 A2 A3. destruct e as [e |]; [| apply mspc_inf].
 apply mspc_ball_Qabs_flip in B. apply mspc_ball_Qabs_flip.
-assert (x1 ≤ x2) by (transitivity y1; [| transitivity y2]; trivial).
+assert (x1 ≤ x2).
+  now apply (PreOrder_Transitive _ y1); [|apply (PreOrder_Transitive _ y2)].
 rewrite abs.abs_nonneg by now apply rings.flip_nonneg_minus.
 rewrite abs.abs_nonneg in B by now apply rings.flip_nonneg_minus.
 apply rings.flip_le_minus_l. apply rings.flip_le_minus_l in B.
-transitivity x2; [easy |]. transitivity (e + x1); [easy |].
+apply (PreOrder_Transitive _ x2); [easy|].
+apply (PreOrder_Transitive _ (e + x1)); [easy|].
 apply (orders.order_preserving (e +)); easy.
 Qed. (* Too long? *)
 

ode/SimpleIntegration.v

@@ -59,7 +59,7 @@ Section integral_interface.
       (forall x, from <= x <= from+ proj1_sig width -> ball (proj1_sig r) (f x) ('mid)) ->
       ball (proj1_sig (width * r)%Qpos) (∫ f from (from_Qpos width)) (' (proj1_sig width * mid)%Q)
 
-    ; integral_wd:> Proper (Qeq ==> QnonNeg.eq ==> @msp_eq _) (∫ f) }.
+    ; integral_wd:: Proper (Qeq ==> QnonNeg.eq ==> @msp_eq _) (∫ f) }.
 
   (* Todo: Show that the sign function is integrable while not locally uniformly continuous. *)
 

ode/metric.v

@@ -142,8 +142,8 @@ Class ExtMetricSpaceClass (X : Type) `{MetricSpaceBall X} : Prop := {
   mspc_radius_proper : Proper ((=) ==> (≡) ==> (≡) ==> iff) ball;
   mspc_inf: ∀ x y, ball Qinf.infinite x y;
   mspc_negative: ∀ (e: Q), e < 0 → ∀ x y, ~ ball e x y;
-  mspc_refl:> ∀ e : Q, 0 ≤ e → Reflexive (ball e);
-  mspc_symm:> ∀ e, Symmetric (ball e);
+  mspc_refl:: ∀ e : Q, 0 ≤ e → Reflexive (ball e);
+  mspc_symm:: ∀ e, Symmetric (ball e);
   mspc_triangle: ∀ (e1 e2: Q) (a b c: X),
      ball e1 a b → ball e2 b c → ball (e1 + e2) a c;
   mspc_closed: ∀ (e: Q) (a b: X),
@@ -437,7 +437,7 @@ Definition restrict (f : X -> Y) (x : X) (r : Q) : sig (ball r x) -> Y :=
 IsUniformlyContinuous and IsLocallyUniformlyContinuous *)
 
 Class IsLocallyUniformlyContinuous (f : X -> Y) (lmu : X -> Q -> Q -> Qinf) :=
-  luc_prf :> forall (x : X) (r : Q), IsUniformlyContinuous (restrict f x r) (lmu x r).
+  luc_prf :: forall (x : X) (r : Q), IsUniformlyContinuous (restrict f x r) (lmu x r).
 
 Global Arguments luc_prf f lmu {_} x r.
 
@@ -580,7 +580,7 @@ particular, integral_lipschitz in AbstractIntegration.v defines [L] as
 [λ a r, abs (f a) + L' a r * r]. *)
 
 Class IsLocallyLipschitz (f : X -> Y) (L : X -> Q -> Q) :=
-  llip_prf :> forall (x : X) (r : Q), PropHolds (0 ≤ r) -> IsLipschitz (restrict f x r) (L x r).
+  llip_prf :: forall (x : X) (r : Q), PropHolds (0 ≤ r) -> IsLipschitz (restrict f x r) (L x r).
 
 Global Arguments llip_prf f L {_} x r _.
 
@@ -625,7 +625,7 @@ Section Contractions.
 Context `{MetricSpaceBall X, MetricSpaceBall Y}.
 
 Class IsContraction (f : X -> Y) (q : Q) := {
-  contr_prf :> IsLipschitz f q;
+  contr_prf :: IsLipschitz f q;
   contr_lt_1 : q < 1
 }.
 
@@ -815,7 +815,7 @@ Qed.
 
 Class Limit := lim : RegularFunction -> X.
 
-Class CompleteMetricSpaceClass `{Limit} := cmspc :> Surjective reg_unit (inv := lim).
+Class CompleteMetricSpaceClass `{Limit} := cmspc :: Surjective reg_unit (inv := lim).
 
 Definition tends_to (f : RegularFunction) (l : X) :=
   forall e : Q, 0 < e -> ball e (f e) l.

reals/faster/AQmetric.v

@@ -14,6 +14,8 @@ Add Ring AQ : (rings.stdlib_ring_theory AQ).
 
 Local Open Scope uc_scope. 
 
+(* To ensure the definitions below don't use sg_setoid instead *)
+Existing Instance strong_setoids.Setoid_instance_0.
 Definition AQ_as_MetricSpace := Emetric (cast AQ Q_as_MetricSpace).
 Definition AQPrelengthSpace := EPrelengthSpace QPrelengthSpace (cast AQ Q_as_MetricSpace).
 Definition AQLocated : locatedMetric AQ_as_MetricSpace.

reals/faster/ARbigD.v

@@ -6,7 +6,7 @@ Require Import
   CoRN.model.totalorder.QposMinMax 
   CoRN.metric2.MetricMorphisms CoRN.model.metric2.Qmetric CoRN.util.Qdlog CoRN.reals.faster.ARArith
   MathClasses.theory.int_pow MathClasses.theory.nat_pow
-  MathClasses.implementations.stdlib_rationals MathClasses.implementations.stdlib_binary_integers MathClasses.implementations.fast_integers MathClasses.implementations.dyadics.
+  MathClasses.interfaces.rationals MathClasses.implementations.stdlib_rationals MathClasses.interfaces.integers MathClasses.implementations.stdlib_binary_integers MathClasses.implementations.fast_integers MathClasses.implementations.dyadics.
 
 Add Field Q : (dec_fields.stdlib_field_theory Q).
 

reals/faster/ApproximateRationals.v

@@ -25,17 +25,17 @@ Class AppRationals AQ {e plus mult zero one inv} `{Apart AQ} `{Le AQ} `{Lt AQ}
     `{!AppInverse AQtoQ} {ZtoAQ : Cast Z AQ} `{!AppDiv AQ} `{!AppApprox AQ} 
     `{!Abs AQ} `{!Pow AQ N} `{!ShiftL AQ Z} 
     `{∀ x y : AQ, Decision (x = y)} `{∀ x y : AQ, Decision (x ≤ y)} : Prop := {
-  aq_ring :> @Ring AQ e plus mult zero one inv ;
-  aq_trivial_apart :> TrivialApart AQ ;
-  aq_order_embed :> OrderEmbedding AQtoQ ;
-  aq_strict_order_embed :> StrictOrderEmbedding AQtoQ ;
-  aq_ring_morphism :> SemiRing_Morphism AQtoQ ;
-  aq_dense_embedding :> DenseEmbedding AQtoQ ;
+  aq_ring :: @Ring AQ e plus mult zero one inv ;
+  aq_trivial_apart :: TrivialApart AQ ;
+  aq_order_embed :: OrderEmbedding AQtoQ ;
+  aq_strict_order_embed :: StrictOrderEmbedding AQtoQ ;
+  aq_ring_morphism :: SemiRing_Morphism AQtoQ ;
+  aq_dense_embedding :: DenseEmbedding AQtoQ ;
   aq_div : ∀ x y k, ball (2 ^ k) ('app_div x y k) ('x / 'y) ;
   aq_compress : ∀ x k, ball (2 ^ k) ('app_approx x k) ('x) ;
-  aq_shift :> ShiftLSpec AQ Z (≪) ;
-  aq_nat_pow :> NatPowSpec AQ N (^) ;
-  aq_ints_mor :> SemiRing_Morphism ZtoAQ
+  aq_shift :: ShiftLSpec AQ Z (≪) ;
+  aq_nat_pow :: NatPowSpec AQ N (^) ;
+  aq_ints_mor :: SemiRing_Morphism ZtoAQ
 }.
 
 Lemma order_embedding_iff `{OrderEmbedding A B f} x y :