From f6c36b5d4deb00d5b7f0fd318547af9e2fabc555 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 31 Jan 2024 16:51:07 +0100 Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/18590 --- theories/Classes.v | 18 +++++++++--------- theories/DKA_DFA_Equiv.v | 2 +- theories/Functors.v | 10 +++++----- theories/StrictKleeneAlgebra.v | 4 ++-- 4 files changed, 17 insertions(+), 17 deletions(-) diff --git a/theories/Classes.v b/theories/Classes.v index 117bc72..0ceeae3 100644 --- a/theories/Classes.v +++ b/theories/Classes.v @@ -25,7 +25,7 @@ Class Graph := { T: Type; X: T -> T -> Type; equal: forall A B, relation (X A B); - equal_:> forall A B, Equivalence (equal A B) + equal_:: forall A B, Equivalence (equal A B) }. (*Arguments equal : simpl never.*) @@ -91,14 +91,14 @@ Section Structures. Context {Mo: Monoid_Ops G} {SLo: SemiLattice_Ops G} {Ko: Star_Op G} {Co: Converse_Op G}. Class Monoid := { - dot_compat:> forall A B C, Proper (equal A B ==> equal B C ==> equal A C) (dot A B C); + dot_compat:: forall A B C, Proper (equal A B ==> equal B C ==> equal A C) (dot A B C); dot_assoc: forall A B C D (x: X A B) y (z: X C D), x*(y*z) == (x*y)*z; dot_neutral_left: forall A B (x: X A B), 1*x == x; dot_neutral_right: forall A B (x: X B A), x*1 == x }. Class SemiLattice := { - plus_compat:> forall A B, Proper (equal A B ==> equal A B ==> equal A B) (plus A B); + plus_compat:: forall A B, Proper (equal A B ==> equal A B ==> equal A B) (plus A B); plus_neutral_left: forall A B (x: X A B), 0+x == x; plus_idem: forall A B (x: X A B), x+x == x; plus_assoc: forall A B (x y z: X A B), x+(y+z) == (x+y)+z; @@ -106,8 +106,8 @@ Section Structures. }. Class IdemSemiRing := { - ISR_Monoid :> Monoid; - ISR_SemiLattice :> SemiLattice; + ISR_Monoid :: Monoid; + ISR_SemiLattice :: SemiLattice; dot_ann_left: forall A B C (x: X B C), zero A B * x == 0; dot_ann_right: forall A B C (x: X C B), x * zero B A == 0; dot_distr_left: forall A B C (x y: X A B) (z: X B C), (x+y)*z == x*z + y*z; @@ -115,7 +115,7 @@ Section Structures. }. Class KleeneAlgebra := { - KA_ISR :> IdemSemiRing; + KA_ISR :: IdemSemiRing; star_make_left: forall A (a:X A A), 1 + a#*a == a#; star_destruct_left: forall A B (a: X A A) (c: X A B), a*c <== c -> a#*c <== c; star_destruct_right: forall A B (a: X A A) (c: X B A), c*a <== c -> c*a# <== c @@ -127,12 +127,12 @@ Section Structures. (* TODO: introduce an intermediate ConverseMonoid class *) Class ConverseIdemSemiRing := { - CISR_SL :> SemiLattice; + CISR_SL :: SemiLattice; dot_compat_c: forall A B C, Proper (equal A B ==> equal B C ==> equal A C) (dot A B C); dot_assoc_c: forall A B C D (x: X A B) y (z: X C D), x*(y*z) == (x*y)*z; dot_neutral_left_c: forall A B (x: X A B), 1*x == x; - conv_compat:> forall A B, Proper (equal A B ==> equal B A) (conv A B); + conv_compat:: forall A B, Proper (equal A B ==> equal B A) (conv A B); conv_invol: forall A B (x: X A B), x`` == x; conv_dot: forall A B C (x: X A B) (y: X B C), (x*y)` == y`*x`; conv_plus: forall A B (x y: X A B), (x+y)` == y`+x`; @@ -141,7 +141,7 @@ Section Structures. }. Class ConverseKleeneAlgebra := { - CKA_CISR :> ConverseIdemSemiRing; + CKA_CISR :: ConverseIdemSemiRing; star_make_left_c: forall A (a:X A A), 1 + a#*a == a#; star_destruct_left_c: forall A B (a: X A A) (c: X A B), a*c <== c -> a#*c <== c }. diff --git a/theories/DKA_DFA_Equiv.v b/theories/DKA_DFA_Equiv.v index 61c5a44..00ce60c 100644 --- a/theories/DKA_DFA_Equiv.v +++ b/theories/DKA_DFA_Equiv.v @@ -182,7 +182,7 @@ Section correctness. Class invariant tarjan : Prop := { - i_wf_tarjan :> DS.WF tarjan ; + i_wf_tarjan :: DS.WF tarjan ; i_final : forall x y, {{tarjan}} x y -> final x = final y }. diff --git a/theories/Functors.v b/theories/Functors.v index 3c41c3d..8763d48 100644 --- a/theories/Functors.v +++ b/theories/Functors.v @@ -36,13 +36,13 @@ Section Defs. forall A B y, exists x, F A B x == y. Class monoid_functor {Mo1: Monoid_Ops G1} {Mo2: Monoid_Ops G2} (F: functor G1 G2) := { - monoid_graph_functor :> graph_functor F; + monoid_graph_functor :: graph_functor F; functor_dot : forall A B C x y, F A C (x*y) == F A B x * F B C y; functor_one : forall A, F A A 1 == 1 }. Class semilattice_functor {SLo1: SemiLattice_Ops G1} {SL2: SemiLattice_Ops G2} (F: functor G1 G2) := { - semilattice_graph_functor :> graph_functor F; + semilattice_graph_functor :: graph_functor F; functor_plus : forall A B x y, F A B (x+y) == F A B x + F A B y; functor_zero : forall A B, F A B 0 == 0 }. @@ -71,8 +71,8 @@ Section Defs. {Ko1: Star_Op G1} {Ko2: Star_Op G2}. Class semiring_functor (F: functor G1 G2) := { - semiring_monoid_functor :> monoid_functor F; - semiring_semilattice_functor :> semilattice_functor F + semiring_monoid_functor :: monoid_functor F; + semiring_semilattice_functor :: semilattice_functor F }. Lemma functor_star_leq {KA1: KleeneAlgebra G1} {KA2: KleeneAlgebra G2} @@ -88,7 +88,7 @@ Section Defs. Qed. Class kleene_functor (F: functor G1 G2) := { - kleene_semiring :> semiring_functor F; + kleene_semiring :: semiring_functor F; functor_star: forall A a, F A A (a#) == (F A A a) # }. diff --git a/theories/StrictKleeneAlgebra.v b/theories/StrictKleeneAlgebra.v index 30e57fc..8fbacf8 100644 --- a/theories/StrictKleeneAlgebra.v +++ b/theories/StrictKleeneAlgebra.v @@ -41,9 +41,9 @@ Delimit Scope SA_scope with SA. (** Strict Kleene Algebras axioms *) Class StrictKleeneAlgebra {G: Graph} {Ops: SKA_Ops G} := { - dot_compat:> + dot_compat:: forall A B C, Proper (equal A B ==> equal B C ==> equal A C) (dot A B C); - plus_compat:> + plus_compat:: forall A B, Proper (equal A B ==> equal A B ==> equal A B) (plus A B); dot_assoc: forall A B C D (x: X A B) y (z: X C D), x*(y*z) == (x*y)*z; dot_neutral_left: forall A B (x: X A B), 1*x == x;