From 9ed2c9fde8e7a370fed031ec10ffcc4faa962769 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 1 Feb 2024 11:14:17 +0100 Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/18590 --- .github/workflows/docker-action.yml | 5 +---- README.md | 6 +++--- algebra/RSetoid.v | 2 ++ classes/Qclasses.v | 1 + coq-corn.opam | 2 +- meta.yml | 9 +++------ metric2/Classified.v | 8 ++++---- metric2/MetricMorphisms.v | 2 +- model/setoids/decsetoid.v | 2 +- ode/AbstractIntegration.v | 1 - ode/FromMetric2.v | 8 +++++--- ode/SimpleIntegration.v | 2 +- ode/metric.v | 12 ++++++------ reals/faster/AQmetric.v | 2 ++ reals/faster/ARbigD.v | 2 +- reals/faster/ApproximateRationals.v | 18 +++++++++--------- 16 files changed, 41 insertions(+), 41 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 89be8f499..0a4530480 100644 --- a/.github/workflows/docker-action.yml +++ b/.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 diff --git a/README.md b/README.md index c8d59bd49..da435b575 100644 --- a/README.md +++ b/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 diff --git a/algebra/RSetoid.v b/algebra/RSetoid.v index d83061e26..af9b0a31d 100644 --- a/algebra/RSetoid.v +++ b/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. diff --git a/classes/Qclasses.v b/classes/Qclasses.v index 0a6b22167..e8f574fa3 100644 --- a/classes/Qclasses.v +++ b/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 diff --git a/coq-corn.opam b/coq-corn.opam index 7212f989a..0b0ddf60d 100644 --- a/coq-corn.opam +++ b/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" ] diff --git a/meta.yml b/meta.yml index b4306df24..c75d8f095 100644 --- a/meta.yml +++ b/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: diff --git a/metric2/Classified.v b/metric2/Classified.v index 01316493b..a2f6606eb 100644 --- a/metric2/Classified.v +++ b/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}. diff --git a/metric2/MetricMorphisms.v b/metric2/MetricMorphisms.v index aa6307d51..0f6a408d3 100644 --- a/metric2/MetricMorphisms.v +++ b/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 }. diff --git a/model/setoids/decsetoid.v b/model/setoids/decsetoid.v index 96cd858f2..fa6dc5a58 100644 --- a/model/setoids/decsetoid.v +++ b/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. diff --git a/ode/AbstractIntegration.v b/ode/AbstractIntegration.v index a9bb95c29..dd93194ba 100644 --- a/ode/AbstractIntegration.v +++ b/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] diff --git a/ode/FromMetric2.v b/ode/FromMetric2.v index 4b57995b8..d9e0911e7 100644 --- a/ode/FromMetric2.v +++ b/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? *) diff --git a/ode/SimpleIntegration.v b/ode/SimpleIntegration.v index 1314f123c..8bff113b2 100644 --- a/ode/SimpleIntegration.v +++ b/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. *) diff --git a/ode/metric.v b/ode/metric.v index 80e269267..3c122e3b4 100644 --- a/ode/metric.v +++ b/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. diff --git a/reals/faster/AQmetric.v b/reals/faster/AQmetric.v index a3c301819..f9a5a2299 100644 --- a/reals/faster/AQmetric.v +++ b/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. diff --git a/reals/faster/ARbigD.v b/reals/faster/ARbigD.v index ff4abc926..976ee2454 100644 --- a/reals/faster/ARbigD.v +++ b/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). diff --git a/reals/faster/ApproximateRationals.v b/reals/faster/ApproximateRationals.v index c25230ee1..c3a1b3cb7 100644 --- a/reals/faster/ApproximateRationals.v +++ b/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 :