From b1e140fb6a4929e1905baebf6fcb9d684ed775e8 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 31 Jan 2024 15:36:06 +0100 Subject: [PATCH 1/2] Require Coq >= 8.18 --- .github/workflows/docker-action.yml | 8 +------- README.md | 6 +++--- coq-math-classes.opam | 2 +- meta.yml | 12 +++--------- 4 files changed, 8 insertions(+), 20 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 65851c1..2246da3 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -18,14 +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' - - 'coqorg/coq:8.13' - - 'coqorg/coq:8.12' - - 'coqorg/coq:8.11' fail-fast: false steps: - uses: actions/checkout@v3 diff --git a/README.md b/README.md index 9e59e83..fa7bd90 100644 --- a/README.md +++ b/README.md @@ -10,8 +10,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener [![Zulip][zulip-shield]][zulip-link] [![DOI][doi-shield]][doi-link] -[docker-action-shield]: https://github.com/coq-community/math-classes/workflows/Docker%20CI/badge.svg?branch=master -[docker-action-link]: https://github.com/coq-community/math-classes/actions?query=workflow:"Docker%20CI" +[docker-action-shield]: https://github.com/coq-community/math-classes/actions/workflows/docker-action.yml/badge.svg?branch=master +[docker-action-link]: https://github.com/coq-community/math-classes/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 @@ -50,7 +50,7 @@ notations. - Coq-community maintainer(s): - Bas Spitters ([**@spitters**](https://github.com/spitters)) - License: [MIT License](LICENSE) -- Compatible Coq versions: Coq 8.11 or later (use releases for other Coq versions) +- Compatible Coq versions: Coq 8.18 or later (use releases for other Coq versions) - Additional dependencies: - [BigNums](https://github.com/coq/bignums) - Coq namespace: `MathClasses` diff --git a/coq-math-classes.opam b/coq-math-classes.opam index 39c527c..9c5c029 100644 --- a/coq-math-classes.opam +++ b/coq-math-classes.opam @@ -30,7 +30,7 @@ build: [ ] install: [make "install"] depends: [ - "coq" {(>= "8.11" & < "8.19~") | (= "dev")} + "coq" {(>= "8.18" & < "8.20~") | (= "dev")} "coq-bignums" ] diff --git a/meta.yml b/meta.yml index 06487b6..bd0d312 100644 --- a/meta.yml +++ b/meta.yml @@ -49,19 +49,13 @@ license: identifier: MIT supported_coq_versions: - text: Coq 8.11 or later (use releases for other Coq versions) - opam: '{(>= "8.11" & < "8.19~") | (= "dev")}' + text: Coq 8.18 or later (use releases for other Coq versions) + 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" -- version: "8.13" -- version: "8.12" -- version: "8.11" dependencies: - opam: From b295176134cd220714bd894d583cf5d594f871d6 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 31 Jan 2024 15:32:38 +0100 Subject: [PATCH 2/2] Adapt to https://github.com/coq/coq/pull/18590 --- implementations/fast_rationals.v | 3 +- interfaces/abstract_algebra.v | 142 ++++++++++++++--------------- interfaces/additional_operations.v | 4 +- interfaces/canonical_names.v | 10 +- interfaces/finite_sets.v | 12 +-- interfaces/functors.v | 6 +- interfaces/integers.v | 6 +- interfaces/monads.v | 16 ++-- interfaces/naturals.v | 8 +- interfaces/orders.v | 76 +++++++-------- interfaces/rationals.v | 8 +- interfaces/sequences.v | 8 +- interfaces/ua_basic.v | 4 +- interfaces/universal_algebra.v | 2 +- interfaces/vectorspace.v | 38 ++++---- theory/forget_variety.v | 2 +- theory/ring_ideals.v | 4 +- theory/ua_congruence.v | 6 +- theory/ua_homomorphisms.v | 2 +- theory/ua_subalgebra.v | 2 +- theory/ua_subvariety.v | 2 +- 21 files changed, 181 insertions(+), 180 deletions(-) diff --git a/implementations/fast_rationals.v b/implementations/fast_rationals.v index fa07d45..7adb506 100644 --- a/implementations/fast_rationals.v +++ b/implementations/fast_rationals.v @@ -1,8 +1,9 @@ Require + MathClasses.theory.rings MathClasses.theory.shiftl MathClasses.theory.int_pow. Require Import Coq.QArith.QArith Bignums.BigQ.BigQ - MathClasses.interfaces.abstract_algebra + MathClasses.interfaces.orders MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.rationals MathClasses.interfaces.additional_operations MathClasses.implementations.fast_naturals MathClasses.implementations.fast_integers MathClasses.implementations.field_of_fractions MathClasses.implementations.stdlib_rationals. Require Export diff --git a/interfaces/abstract_algebra.v b/interfaces/abstract_algebra.v index b63b504..4c2f61f 100644 --- a/interfaces/abstract_algebra.v +++ b/interfaces/abstract_algebra.v @@ -6,9 +6,9 @@ For various structures we omit declaration of substructures. For example, if we say: Class Setoid_Morphism := - { setoidmor_a :> Setoid A - ; setoidmor_b :> Setoid B - ; sm_proper :> Proper ((=) ==> (=)) f }. + { setoidmor_a :: Setoid A + ; setoidmor_b :: Setoid B + ; sm_proper :: Proper ((=) ==> (=)) f }. then each time a Setoid instance is required, Coq will try to prove that a Setoid_Morphism exists. This obviously results in an enormous blow-up of the @@ -20,14 +20,14 @@ Setoid_Morphism as a substructure, setoid rewriting will become horribly slow. *) (* An unbundled variant of the former CoRN RSetoid *) -Class Setoid A {Ae : Equiv A} : Prop := setoid_eq :> Equivalence (@equiv A Ae). +Class Setoid A {Ae : Equiv A} : Prop := setoid_eq :: Equivalence (@equiv A Ae). (* An unbundled variant of the former CoRN CSetoid. We do not include a proof that A is a Setoid because it can be derived. *) Class StrongSetoid A {Ae : Equiv A} `{Aap : Apart A} : Prop := - { strong_setoid_irreflexive :> Irreflexive (≶) - ; strong_setoid_symmetric :> Symmetric (≶) - ; strong_setoid_cotrans :> CoTransitive (≶) + { strong_setoid_irreflexive :: Irreflexive (≶) + ; strong_setoid_symmetric :: Symmetric (≶) + ; strong_setoid_cotrans :: CoTransitive (≶) ; tight_apart : ∀ x y, ¬x ≶ y ↔ x = y }. Arguments tight_apart {A Ae Aap StrongSetoid} _ _. @@ -38,7 +38,7 @@ Section setoid_morphisms. Class Setoid_Morphism := { setoidmor_a : Setoid A ; setoidmor_b : Setoid B - ; sm_proper :> Proper ((=) ==> (=)) f }. + ; sm_proper :: Proper ((=) ==> (=)) f }. Class StrongSetoid_Morphism := { strong_setoidmor_a : StrongSetoid A @@ -70,55 +70,55 @@ Section upper_classes. Context A {Ae : Equiv A}. Class SemiGroup {Aop: SgOp A} : Prop := - { sg_setoid :> Setoid A - ; sg_ass :> Associative (&) - ; sg_op_proper :> Proper ((=) ==> (=) ==> (=)) (&) }. + { sg_setoid :: Setoid A + ; sg_ass :: Associative (&) + ; sg_op_proper :: Proper ((=) ==> (=) ==> (=)) (&) }. Class CommutativeSemiGroup {Aop : SgOp A} : Prop := - { comsg_setoid :> @SemiGroup Aop - ; comsg_ass :> Commutative (&) }. + { comsg_setoid :: @SemiGroup Aop + ; comsg_ass :: Commutative (&) }. Class SemiLattice {Aop : SgOp A} : Prop := - { semilattice_sg :> @CommutativeSemiGroup Aop - ; semilattice_idempotent :> BinaryIdempotent (&)}. + { semilattice_sg :: @CommutativeSemiGroup Aop + ; semilattice_idempotent :: BinaryIdempotent (&)}. Class Monoid {Aop : SgOp A} {Aunit : MonUnit A} : Prop := - { monoid_semigroup :> SemiGroup - ; monoid_left_id :> LeftIdentity (&) mon_unit - ; monoid_right_id :> RightIdentity (&) mon_unit }. + { monoid_semigroup :: SemiGroup + ; monoid_left_id :: LeftIdentity (&) mon_unit + ; monoid_right_id :: RightIdentity (&) mon_unit }. Class CommutativeMonoid {Aop Aunit} : Prop := - { commonoid_mon :> @Monoid Aop Aunit - ; commonoid_commutative :> Commutative (&) }. + { commonoid_mon :: @Monoid Aop Aunit + ; commonoid_commutative :: Commutative (&) }. Class Group {Aop Aunit} {Anegate : Negate A} : Prop := - { group_monoid :> @Monoid Aop Aunit - ; negate_proper :> Setoid_Morphism (-) - ; negate_l :> LeftInverse (&) (-) mon_unit - ; negate_r :> RightInverse (&) (-) mon_unit }. + { group_monoid :: @Monoid Aop Aunit + ; negate_proper :: Setoid_Morphism (-) + ; negate_l :: LeftInverse (&) (-) mon_unit + ; negate_r :: RightInverse (&) (-) mon_unit }. Class BoundedSemiLattice {Aop Aunit} : Prop := - { bounded_semilattice_mon :> @CommutativeMonoid Aop Aunit - ; bounded_semilattice_idempotent :> BinaryIdempotent (&)}. + { bounded_semilattice_mon :: @CommutativeMonoid Aop Aunit + ; bounded_semilattice_idempotent :: BinaryIdempotent (&)}. Class AbGroup {Aop Aunit Anegate} : Prop := - { abgroup_group :> @Group Aop Aunit Anegate - ; abgroup_commutative :> Commutative (&) }. + { abgroup_group :: @Group Aop Aunit Anegate + ; abgroup_commutative :: Commutative (&) }. Context {Aplus : Plus A} {Amult : Mult A} {Azero : Zero A} {Aone : One A}. Class SemiRing : Prop := - { semiplus_monoid :> @CommutativeMonoid plus_is_sg_op zero_is_mon_unit - ; semimult_monoid :> @CommutativeMonoid mult_is_sg_op one_is_mon_unit - ; semiring_distr :> LeftDistribute (.*.) (+) - ; semiring_left_absorb :> LeftAbsorb (.*.) 0 }. + { semiplus_monoid :: @CommutativeMonoid plus_is_sg_op zero_is_mon_unit + ; semimult_monoid :: @CommutativeMonoid mult_is_sg_op one_is_mon_unit + ; semiring_distr :: LeftDistribute (.*.) (+) + ; semiring_left_absorb :: LeftAbsorb (.*.) 0 }. Context {Anegate : Negate A}. Class Ring : Prop := - { ring_group :> @AbGroup plus_is_sg_op zero_is_mon_unit _ - ; ring_monoid :> @CommutativeMonoid mult_is_sg_op one_is_mon_unit - ; ring_dist :> LeftDistribute (.*.) (+) }. + { ring_group :: @AbGroup plus_is_sg_op zero_is_mon_unit _ + ; ring_monoid :: @CommutativeMonoid mult_is_sg_op one_is_mon_unit + ; ring_dist :: LeftDistribute (.*.) (+) }. (* For now, we follow CoRN/ring_theory's example in having Ring and SemiRing require commutative multiplication. *) @@ -126,24 +126,24 @@ Section upper_classes. Class IntegralDomain : Prop := { intdom_ring : Ring ; intdom_nontrivial : PropHolds (1 ≠ 0) - ; intdom_nozeroes :> NoZeroDivisors A }. + ; intdom_nozeroes :: NoZeroDivisors A }. (* We do not include strong extensionality for (-) and (/) because it can de derived *) Class Field {Aap: Apart A} {Arecip: Recip A} : Prop := - { field_ring :> Ring - ; field_strongsetoid :> StrongSetoid A - ; field_plus_ext :> StrongSetoid_BinaryMorphism (+) - ; field_mult_ext :> StrongSetoid_BinaryMorphism (.*.) + { field_ring :: Ring + ; field_strongsetoid :: StrongSetoid A + ; field_plus_ext :: StrongSetoid_BinaryMorphism (+) + ; field_mult_ext :: StrongSetoid_BinaryMorphism (.*.) ; field_nontrivial : PropHolds (1 ≶ 0) - ; recip_proper :> Setoid_Morphism (//) + ; recip_proper :: Setoid_Morphism (//) ; recip_inverse : ∀ x, `x // x = 1 }. (* We let /0 = 0 so properties as Injective (/), f (/x) = / (f x), / /x = x, /x * /y = /(x * y) hold without any additional assumptions *) Class DecField {Adec_recip : DecRecip A} : Prop := - { decfield_ring :> Ring + { decfield_ring :: Ring ; decfield_nontrivial : PropHolds (1 ≠ 0) - ; dec_recip_proper :> Setoid_Morphism (/) + ; dec_recip_proper :: Setoid_Morphism (/) ; dec_recip_0 : /0 = 0 ; dec_recip_inverse : ∀ x, x ≠ 0 → x / x = 1 }. End upper_classes. @@ -159,7 +159,7 @@ Hint Extern 5 (PropHolds (1 ≠ 0)) => eapply @decfield_nontrivial : typeclass_i (* For a strange reason Ring instances of Integers are sometimes obtained by Integers -> IntegralDomain -> Ring and sometimes directly. Making this an -instance with a low priority instead of using intdom_ring:> Ring forces Coq to +instance with a low priority instead of using intdom_ring:: Ring forces Coq to take the right way *) #[global] @@ -174,29 +174,29 @@ Section lattice. Context A `{Ae: Equiv A} {Ajoin: Join A} {Ameet: Meet A} `{Abottom : Bottom A}. Class JoinSemiLattice : Prop := - join_semilattice :> @SemiLattice A Ae join_is_sg_op. + join_semilattice :: @SemiLattice A Ae join_is_sg_op. Class BoundedJoinSemiLattice : Prop := - bounded_join_semilattice :> @BoundedSemiLattice A Ae join_is_sg_op bottom_is_mon_unit. + bounded_join_semilattice :: @BoundedSemiLattice A Ae join_is_sg_op bottom_is_mon_unit. Class MeetSemiLattice : Prop := - meet_semilattice :> @SemiLattice A Ae meet_is_sg_op. + meet_semilattice :: @SemiLattice A Ae meet_is_sg_op. Class Lattice : Prop := - { lattice_join :> JoinSemiLattice - ; lattice_meet :> MeetSemiLattice - ; join_meet_absorption :> Absorption (⊔) (⊓) - ; meet_join_absorption :> Absorption (⊓) (⊔)}. + { lattice_join :: JoinSemiLattice + ; lattice_meet :: MeetSemiLattice + ; join_meet_absorption :: Absorption (⊔) (⊓) + ; meet_join_absorption :: Absorption (⊓) (⊔)}. Class DistributiveLattice : Prop := - { distr_lattice_lattice :> Lattice - ; join_meet_distr_l :> LeftDistribute (⊔) (⊓) }. + { distr_lattice_lattice :: Lattice + ; join_meet_distr_l :: LeftDistribute (⊔) (⊓) }. End lattice. Class Category O `{!Arrows O} `{∀ x y: O, Equiv (x ⟶ y)} `{!CatId O} `{!CatComp O}: Prop := - { arrow_equiv :> ∀ x y, Setoid (x ⟶ y) - ; comp_proper :> ∀ x y z, Proper ((=) ==> (=) ==> (=)) (comp x y z) - ; comp_assoc :> ArrowsAssociative O - ; id_l :> ∀ x y, LeftIdentity (comp x y y) cat_id - ; id_r :> ∀ x y, RightIdentity (comp x x y) cat_id }. + { arrow_equiv :: ∀ x y, Setoid (x ⟶ y) + ; comp_proper :: ∀ x y z, Proper ((=) ==> (=) ==> (=)) (comp x y z) + ; comp_assoc :: ArrowsAssociative O + ; id_l :: ∀ x y, LeftIdentity (comp x y y) cat_id + ; id_r :: ∀ x y, RightIdentity (comp x x y) cat_id }. (* note: no equality on objects. *) (* todo: use my comp everywhere *) @@ -208,46 +208,46 @@ Section morphism_classes. Class SemiGroup_Morphism {Aop Bop} (f : A → B) := { sgmor_a : @SemiGroup A Ae Aop ; sgmor_b : @SemiGroup B Be Bop - ; sgmor_setmor :> Setoid_Morphism f + ; sgmor_setmor :: Setoid_Morphism f ; preserves_sg_op : ∀ x y, f (x & y) = f x & f y }. Class JoinSemiLattice_Morphism {Ajoin Bjoin} (f : A → B) := { join_slmor_a : @JoinSemiLattice A Ae Ajoin ; join_slmor_b : @JoinSemiLattice B Be Bjoin - ; join_slmor_sgmor :> @SemiGroup_Morphism join_is_sg_op join_is_sg_op f }. + ; join_slmor_sgmor :: @SemiGroup_Morphism join_is_sg_op join_is_sg_op f }. Class MeetSemiLattice_Morphism {Ameet Bmeet} (f : A → B) := { meet_slmor_a : @MeetSemiLattice A Ae Ameet ; meet_slmor_b : @MeetSemiLattice B Be Bmeet - ; meet_slmor_sgmor :> @SemiGroup_Morphism meet_is_sg_op meet_is_sg_op f }. + ; meet_slmor_sgmor :: @SemiGroup_Morphism meet_is_sg_op meet_is_sg_op f }. Class Monoid_Morphism {Aunit Bunit Aop Bop} (f : A → B) := { monmor_a : @Monoid A Ae Aop Aunit ; monmor_b : @Monoid B Be Bop Bunit - ; monmor_sgmor :> SemiGroup_Morphism f + ; monmor_sgmor :: SemiGroup_Morphism f ; preserves_mon_unit : f mon_unit = mon_unit }. Class BoundedJoinSemiLattice_Morphism {Abottom Bbottom Ajoin Bjoin} (f : A → B) := { bounded_join_slmor_a : @BoundedJoinSemiLattice A Ae Ajoin Abottom ; bounded_join_slmor_b : @BoundedJoinSemiLattice B Be Bjoin Bbottom - ; bounded_join_slmor_monmor :> @Monoid_Morphism bottom_is_mon_unit bottom_is_mon_unit join_is_sg_op join_is_sg_op f }. + ; bounded_join_slmor_monmor :: @Monoid_Morphism bottom_is_mon_unit bottom_is_mon_unit join_is_sg_op join_is_sg_op f }. Class SemiRing_Morphism {Aplus Amult Azero Aone Bplus Bmult Bzero Bone} (f : A → B) := { semiringmor_a : @SemiRing A Ae Aplus Amult Azero Aone ; semiringmor_b : @SemiRing B Be Bplus Bmult Bzero Bone - ; semiringmor_plus_mor :> @Monoid_Morphism zero_is_mon_unit zero_is_mon_unit plus_is_sg_op plus_is_sg_op f - ; semiringmor_mult_mor :> @Monoid_Morphism one_is_mon_unit one_is_mon_unit mult_is_sg_op mult_is_sg_op f }. + ; semiringmor_plus_mor :: @Monoid_Morphism zero_is_mon_unit zero_is_mon_unit plus_is_sg_op plus_is_sg_op f + ; semiringmor_mult_mor :: @Monoid_Morphism one_is_mon_unit one_is_mon_unit mult_is_sg_op mult_is_sg_op f }. Class Lattice_Morphism {Ajoin Ameet Bjoin Bmeet} (f : A → B) := { latticemor_a : @Lattice A Ae Ajoin Ameet ; latticemor_b : @Lattice B Be Bjoin Bmeet - ; latticemor_join_mor :> JoinSemiLattice_Morphism f - ; latticemor_meet_mor :> MeetSemiLattice_Morphism f }. + ; latticemor_join_mor :: JoinSemiLattice_Morphism f + ; latticemor_meet_mor :: MeetSemiLattice_Morphism f }. Context {Aap : Apart A} {Bap : Apart B}. Class StrongSemiRing_Morphism {Aplus Amult Azero Aone Bplus Bmult Bzero Bone} (f : A → B) := - { strong_semiringmor_sr_mor :> @SemiRing_Morphism Aplus Amult Azero Aone Bplus Bmult Bzero Bone f - ; strong_semiringmor_strong_mor :> StrongSetoid_Morphism f }. + { strong_semiringmor_sr_mor :: @SemiRing_Morphism Aplus Amult Azero Aone Bplus Bmult Bzero Bone f + ; strong_semiringmor_strong_mor :: StrongSetoid_Morphism f }. End morphism_classes. Section jections. @@ -267,8 +267,8 @@ Section jections. ; surjective_mor : Setoid_Morphism f }. Class Bijective : Prop := - { bijective_injective :> Injective - ; bijective_surjective :> Surjective }. + { bijective_injective :: Injective + ; bijective_surjective :: Surjective }. End jections. #[global] diff --git a/interfaces/additional_operations.v b/interfaces/additional_operations.v index a5c0c5b..7f454bb 100644 --- a/interfaces/additional_operations.v +++ b/interfaces/additional_operations.v @@ -34,7 +34,7 @@ Instance: Params (@shiftl) 3 := {}. Class ShiftLSpec A B (sl : ShiftL A B) `{Equiv A} `{Equiv B} `{One A} `{Plus A} `{Mult A} `{Zero B} `{One B} `{Plus B} := { shiftl_proper : Proper ((=) ==> (=) ==> (=)) (≪) ; - shiftl_0 :> RightIdentity (≪) 0 ; + shiftl_0 :: RightIdentity (≪) 0 ; shiftl_S : ∀ x n, x ≪ (1 + n) = 2 * x ≪ n }. @@ -71,7 +71,7 @@ Instance: Params (@shiftr) 3 := {}. Class ShiftRSpec A B (sl : ShiftR A B) `{Equiv A} `{Equiv B} `{One A} `{Plus A} `{Mult A} `{Zero B} `{One B} `{Plus B} := { shiftr_proper : Proper ((=) ==> (=) ==> (=)) (≫) ; - shiftr_0 :> RightIdentity (≫) 0 ; + shiftr_0 :: RightIdentity (≫) 0 ; shiftr_S : ∀ x n, x ≫ n = 2 * x ≫ (1 + n) ∨ x ≫ n = 2 * x ≫ (1 + n) + 1 }. diff --git a/interfaces/canonical_names.v b/interfaces/canonical_names.v index a41f2c9..bdd3449 100644 --- a/interfaces/canonical_names.v +++ b/interfaces/canonical_names.v @@ -405,12 +405,12 @@ Notation "f ⁻¹" := (inverse f) (at level 30) : mc_scope. Class Idempotent `{ea : Equiv A} (f: A → A → A) (x : A) : Prop := idempotency: f x x = x. Arguments idempotency {A ea} _ _ {Idempotent}. -Class UnaryIdempotent `{Equiv A} (f: A → A) : Prop := unary_idempotent :> Idempotent (@compose A A A) f. +Class UnaryIdempotent `{Equiv A} (f: A → A) : Prop := unary_idempotent :: Idempotent (@compose A A A) f. Lemma unary_idempotency `{Equiv A} `{!Reflexive (=)} `{!UnaryIdempotent f} x : f (f x) = f x. Proof. firstorder. Qed. -Class BinaryIdempotent `{Equiv A} (op: A → A → A) : Prop := binary_idempotent :> ∀ x, Idempotent op x. +Class BinaryIdempotent `{Equiv A} (op: A → A → A) : Prop := binary_idempotent :: ∀ x, Idempotent op x. Class LeftIdentity {A} `{Equiv B} (op : A → B → B) (x : A): Prop := left_identity: ∀ y, op x y = y. Class RightIdentity `{Equiv A} {B} (op : A → B → A) (y : B): Prop := right_identity: ∀ x, op x y = x. @@ -428,7 +428,7 @@ Class Commutative `{Equiv B} `(f : A → A → B) : Prop := commutativity: ∀ x Class HeteroAssociative {A B C AB BC} `{Equiv ABC} (fA_BC: A → BC → ABC) (fBC: B → C → BC) (fAB_C: AB → C → ABC) (fAB : A → B → AB): Prop := associativity : ∀ x y z, fA_BC x (fBC y z) = fAB_C (fAB x y) z. -Class Associative `{Equiv A} f := simple_associativity:> HeteroAssociative f f f f. +Class Associative `{Equiv A} f := simple_associativity:: HeteroAssociative f f f f. Notation ArrowsAssociative C := (∀ {w x y z: C}, HeteroAssociative (◎) (comp z _ _ ) (◎) (comp y x w)). Class Involutive `{Equiv A} (f : A → A) := involutive: ∀ x, f (f x) = x. @@ -451,8 +451,8 @@ Class LeftHeteroDistribute {A B} `{Equiv C} (f : A → B → C) (g_r : B → B := distribute_l : ∀ a b c, f a (g_r b c) = g (f a b) (f a c). Class RightHeteroDistribute {A B} `{Equiv C} (f : A → B → C) (g_l : A → A → A) (g : C → C → C) : Prop := distribute_r: ∀ a b c, f (g_l a b) c = g (f a c) (f b c). -Class LeftDistribute`{Equiv A} (f g: A → A → A) := simple_distribute_l :> LeftHeteroDistribute f g g. -Class RightDistribute `{Equiv A} (f g: A → A → A) := simple_distribute_r :> RightHeteroDistribute f g g. +Class LeftDistribute`{Equiv A} (f g: A → A → A) := simple_distribute_l :: LeftHeteroDistribute f g g. +Class RightDistribute `{Equiv A} (f g: A → A → A) := simple_distribute_r :: RightHeteroDistribute f g g. Class HeteroSymmetric {A} {T : A → A → Type} (R : ∀ {x y}, T x y → T y x → Prop) : Prop := hetero_symmetric `(a : T x y) (b : T y x) : R a b → R b a. diff --git a/interfaces/finite_sets.v b/interfaces/finite_sets.v index 2cda57e..a77b700 100644 --- a/interfaces/finite_sets.v +++ b/interfaces/finite_sets.v @@ -42,9 +42,9 @@ Class FSetExtend A `{t : SetType A} := Class FSet A `{At : SetType A} `{Ae : Equiv A} `{Ate : SetEquiv A} `{Aempty : EmptySet A} `{Ajoin : SetJoin A} `{Asingle : SetSingleton A} `{∀ a₁ a₂ : A, Decision (a₁ = a₂)} `{U : !FSetExtend A} := - { fset_bounded_sl :> BoundedJoinSemiLattice (set_type A) - ; singleton_mor :> Setoid_Morphism singleton - ; fset_extend_mor `{BoundedJoinSemiLattice B} `{!Setoid_Morphism (f : A → B)} :> + { fset_bounded_sl :: BoundedJoinSemiLattice (set_type A) + ; singleton_mor :: Setoid_Morphism singleton + ; fset_extend_mor `{BoundedJoinSemiLattice B} `{!Setoid_Morphism (f : A → B)} :: BoundedJoinSemiLattice_Morphism (fset_extend f) ; fset_extend_correct `{BoundedJoinSemiLattice B} (f : A → B) `{!Setoid_Morphism f} : f = fset_extend f ∘ singleton @@ -63,7 +63,7 @@ freely use orders.lattices.alt_Build_JoinSemiLatticeOrder. Class FSetContainsSpec A `{At : SetType A} `{Ae : Equiv A} `{Ate : SetEquiv A} `{SetLe A} `{SetContains A} `{Ajoin : SetJoin A} `{Asingle : SetSingleton A} := - { fset_join_sl_order :> JoinSemiLatticeOrder (≤) + { fset_join_sl_order :: JoinSemiLatticeOrder (≤) ; fset_in_singleton_le : ∀ x X, x ∈ X ↔ {{ x }} ≤ X }. (* @@ -71,7 +71,7 @@ Unfortunately, properties as meet and the differences cannot be uniquely defined in an algebraic way, therefore we just use set inclusion. *) Class FullFSet A {car Ae conAe conAle Acontains Aempty Ajoin Asingle U Adec} `{Adiff : SetDifference A} `{Ameet : SetMeet A} := - { full_fset_fset :> @FSet A car Ae conAe Aempty Ajoin Asingle U Adec - ; full_fset_contains :> @FSetContainsSpec A car Ae conAe conAle Acontains Ajoin Asingle + { full_fset_fset :: @FSet A car Ae conAe Aempty Ajoin Asingle U Adec + ; full_fset_contains :: @FSetContainsSpec A car Ae conAe conAle Acontains Ajoin Asingle ; fset_in_meet : ∀ X Y x, x ∈ X ⊓ Y ↔ (x ∈ X ∧ x ∈ Y) ; fset_in_difference : ∀ X Y x, x ∈ X∖ Y ↔ (x ∈ X ∧ x ∉ Y) }. diff --git a/interfaces/functors.v b/interfaces/functors.v index b7d1059..d5c7b4c 100644 --- a/interfaces/functors.v +++ b/interfaces/functors.v @@ -9,7 +9,7 @@ Section functor_class. Class Functor `(Fmap): Prop := { functor_from: Category C ; functor_to: Category D - ; functor_morphism:> ∀ a b: C, Setoid_Morphism (@fmap _ a b) + ; functor_morphism:: ∀ a b: C, Setoid_Morphism (@fmap _ a b) ; preserves_id: `(fmap (cat_id: a ⟶ a) = cat_id) ; preserves_comp `(f: y ⟶ z) `(g: x ⟶ y): fmap (f ◎ g) = fmap f ◎ fmap g }. End functor_class. @@ -123,8 +123,8 @@ Class SFmap (M : Type → Type) := sfmap: ∀ `(A → B), (M A → M B). Class SFunctor (M : Type → Type) `{∀ `{Equiv A}, Equiv (M A)} `{SFmap M} : Prop := - { sfunctor_setoid `{Setoid A} :> Setoid (M A) - ; sfmap_proper `{Setoid A} `{Setoid B} :> + { sfunctor_setoid `{Setoid A} :: Setoid (M A) + ; sfmap_proper `{Setoid A} `{Setoid B} :: Proper (((=) ==> (=)) ==> ((=) ==> (=))) (@sfmap M _ A B) ; sfmap_id `{Setoid A} : sfmap id = id ; sfmap_comp `{Equiv A} `{Equiv B} `{Equiv C} `{!Setoid_Morphism (f : B → C)} `{!Setoid_Morphism (g : A → B)} : diff --git a/interfaces/integers.v b/interfaces/integers.v index ae2208d..8a48888 100644 --- a/interfaces/integers.v +++ b/interfaces/integers.v @@ -33,9 +33,9 @@ End initial_maps. Instance: Params (@integers_to_ring) 8 := {}. Class Integers A {e plus mult zero one negate} `{U : IntegersToRing A} := - { integers_ring:> @Ring A e plus mult zero one negate - ; integers_to_ring_mor:> ∀ `{Ring B}, SemiRing_Morphism (integers_to_ring A B) - ; integers_initial:> Initial (rings.object A) }. + { integers_ring:: @Ring A e plus mult zero one negate + ; integers_to_ring_mor:: ∀ `{Ring B}, SemiRing_Morphism (integers_to_ring A B) + ; integers_initial:: Initial (rings.object A) }. Section specializable. Context (Z N : Type) `{Integers Z} `{Naturals N}. diff --git a/interfaces/monads.v b/interfaces/monads.v index f6b637a..2716d90 100644 --- a/interfaces/monads.v +++ b/interfaces/monads.v @@ -21,10 +21,10 @@ Notation "x ← y ; z" := (y ≫= (λ x : _, z)) (at level 65, (*next at level 3 Class Monad (M : Type → Type) `{∀ A, Equiv A → Equiv (M A)} `{MonadReturn M} `{MonadBind M} : Prop := - { mon_ret_proper `{Setoid A} :> Proper ((=) ==> (=)) (@ret _ _ A) - ; mon_bind_proper `{Setoid A} `{Setoid B} :> + { mon_ret_proper `{Setoid A} :: Proper ((=) ==> (=)) (@ret _ _ A) + ; mon_bind_proper `{Setoid A} `{Setoid B} :: Proper (((=) ==> (=)) ==> (=) ==> (=)) (@bind _ _ A B) - ; mon_setoid `{Setoid A} :> Setoid (M A) + ; mon_setoid `{Setoid A} :: Setoid (M A) ; bind_lunit `{Equiv A} `{Setoid B} `{!Setoid_Morphism (f : A → M B)} : bind f ∘ ret = f ; bind_runit `{Setoid A} : bind ret = id ; bind_assoc `{Equiv A} `{Equiv B} `{Setoid C} @@ -33,9 +33,9 @@ Class Monad (M : Type → Type) `{∀ A, Equiv A → Equiv (M A)} Class StrongMonad (M : Type → Type) `{∀ A, Equiv A → Equiv (M A)} `{MonadReturn M} `{SFmap M} `{MonadJoin M} : Prop := - { smon_ret_proper `{Setoid A} :> Proper ((=) ==> (=)) (@ret _ _ A) - ; smon_join_proper `{Setoid A} :> Proper ((=) ==> (=)) (@join _ _ A) - ; smon_sfunctor :> SFunctor M + { smon_ret_proper `{Setoid A} :: Proper ((=) ==> (=)) (@ret _ _ A) + ; smon_join_proper `{Setoid A} :: Proper ((=) ==> (=)) (@join _ _ A) + ; smon_sfunctor :: SFunctor M ; sfmap_ret `{Equiv A} `{Equiv B} `{!Setoid_Morphism (f : A → B)} : sfmap f ∘ ret = ret ∘ f ; sfmap_join `{Equiv A} `{Equiv B} `{!Setoid_Morphism (f : A → B)} : @@ -49,7 +49,7 @@ Class StrongMonad (M : Type → Type) `{∀ A, Equiv A → Equiv (M A)} Class FullMonad (M : Type → Type) `{∀ A, Equiv A → Equiv (M A)} `{MonadReturn M} `{MonadBind M} `{SFmap M} `{MonadJoin M} : Prop := - { full_mon_mon :> Monad M - ; full_smon :> StrongMonad M + { full_mon_mon :: Monad M + ; full_smon :: StrongMonad M ; bind_as_join_sfmap `{Equiv A} `{Setoid B} `{!Setoid_Morphism (f : A → M B)} : bind f = join ∘ sfmap f }. diff --git a/interfaces/naturals.v b/interfaces/naturals.v index 5c1befa..33d5f9f 100644 --- a/interfaces/naturals.v +++ b/interfaces/naturals.v @@ -4,7 +4,7 @@ Require Import Module bad. Class Naturals (A: semirings.Object) `{!InitialArrow A}: Prop := - { naturals_initial:> Initial A }. + { naturals_initial:: Initial A }. End bad. Section initial_maps. @@ -40,9 +40,9 @@ End initial_maps. Instance: Params (@naturals_to_semiring) 7 := {}. Class Naturals A {e plus mult zero one} `{U: NaturalsToSemiRing A} := - { naturals_ring:> @SemiRing A e plus mult zero one - ; naturals_to_semiring_mor:> ∀ `{SemiRing B}, SemiRing_Morphism (naturals_to_semiring A B) - ; naturals_initial:> Initial (semirings.object A) }. + { naturals_ring:: @SemiRing A e plus mult zero one + ; naturals_to_semiring_mor:: ∀ `{SemiRing B}, SemiRing_Morphism (naturals_to_semiring A B) + ; naturals_initial:: Initial (semirings.object A) }. (* Specializable operations: *) Class NatDistance N `{Equiv N} `{Plus N} diff --git a/interfaces/orders.v b/interfaces/orders.v index c6598ec..826d3a2 100644 --- a/interfaces/orders.v +++ b/interfaces/orders.v @@ -19,13 +19,13 @@ usual properties like Trichotomy (<) and TotalRelation (≤). Class PartialOrder `{Ae : Equiv A} (Ale : Le A) : Prop := { po_setoid : Setoid A (* Making this a subclass makes instance search slow *) - ; po_proper:> Proper ((=) ==> (=) ==> iff) (≤) - ; po_preorder:> PreOrder (≤) - ; po_antisym:> AntiSymmetric (≤) }. + ; po_proper:: Proper ((=) ==> (=) ==> iff) (≤) + ; po_preorder:: PreOrder (≤) + ; po_antisym:: AntiSymmetric (≤) }. Class TotalOrder `{Ae : Equiv A} (Ale : Le A) : Prop := - { total_order_po :> PartialOrder (≤) - ; total_order_total :> TotalRelation (≤) }. + { total_order_po :: PartialOrder (≤) + ; total_order_total :: TotalRelation (≤) }. (* We define a variant of the order theoretic definition of meet and join @@ -37,48 +37,48 @@ This is needed to prove equavalence with the algebraic definition. We do this in orders.lattices. *) Class MeetSemiLatticeOrder `{Ae : Equiv A} (Ale : Le A) `{Meet A} : Prop := - { meet_sl_order :> PartialOrder (≤) + { meet_sl_order :: PartialOrder (≤) ; meet_lb_l : ∀ x y, x ⊓ y ≤ x ; meet_lb_r : ∀ x y, x ⊓ y ≤ y ; meet_glb : ∀ x y z, z ≤ x → z ≤ y → z ≤ x ⊓ y }. Class JoinSemiLatticeOrder `{Ae : Equiv A} (Ale : Le A) `{Join A} : Prop := - { join_sl_order :> PartialOrder (≤) + { join_sl_order :: PartialOrder (≤) ; join_ub_l : ∀ x y, x ≤ x ⊔ y ; join_ub_r : ∀ x y, y ≤ x ⊔ y ; join_lub : ∀ x y z, x ≤ z → y ≤ z → x ⊔ y ≤ z }. Class LatticeOrder `{Ae : Equiv A} (Ale : Le A) `{Meet A} `{Join A} : Prop := - { lattice_order_meet :> MeetSemiLatticeOrder (≤) - ; lattice_order_join :> JoinSemiLatticeOrder (≤) }. + { lattice_order_meet :: MeetSemiLatticeOrder (≤) + ; lattice_order_join :: JoinSemiLatticeOrder (≤) }. (* The strict order from the standard library does not include (=) and thus does not require (<) to be Proper. *) Class StrictSetoidOrder `{Ae : Equiv A} (Alt : Lt A) : Prop := { strict_setoid_order_setoid : Setoid A - ; strict_setoid_order_proper :> Proper ((=) ==> (=) ==> iff) (<) - ; strict_setoid_order_strict :> StrictOrder (<) }. + ; strict_setoid_order_proper :: Proper ((=) ==> (=) ==> iff) (<) + ; strict_setoid_order_strict :: StrictOrder (<) }. (* The constructive notion of a total strict total order. Note that we get Proper (<) from cotransitivity. We will prove that (<) is in fact a StrictSetoidOrder. *) Class PseudoOrder `{Ae : Equiv A} `{Aap : Apart A} (Alt : Lt A) : Prop := { pseudo_order_setoid : StrongSetoid A ; pseudo_order_antisym : ∀ x y, ¬(x < y ∧ y < x) - ; pseudo_order_cotrans :> CoTransitive (<) + ; pseudo_order_cotrans :: CoTransitive (<) ; apart_iff_total_lt : ∀ x y, x ≶ y ↔ x < y ∨ y < x }. (* A partial order (≤) with a corresponding (<). We will prove that (<) is in fact a StrictSetoidOrder *) Class FullPartialOrder `{Ae : Equiv A} `{Aap : Apart A} (Ale : Le A) (Alt : Lt A) : Prop := { strict_po_setoid : StrongSetoid A - ; strict_po_po :> PartialOrder (≤) - ; strict_po_trans :> Transitive (<) + ; strict_po_po :: PartialOrder (≤) + ; strict_po_trans :: Transitive (<) ; lt_iff_le_apart : ∀ x y, x < y ↔ x ≤ y ∧ x ≶ y }. (* A pseudo order (<) with a corresponding (≤). We will prove that (≤) is in fact a PartialOrder. *) Class FullPseudoOrder `{Ae : Equiv A} `{Aap : Apart A} (Ale : Le A) (Alt : Lt A) : Prop := - { full_pseudo_order_pseudo :> PseudoOrder Alt + { full_pseudo_order_pseudo :: PseudoOrder Alt ; le_iff_not_lt_flip : ∀ x y, x ≤ y ↔ ¬y < x }. Section order_maps. @@ -97,32 +97,32 @@ Section order_maps. ; strict_order_morphism_so_b : StrictSetoidOrder Blt }. Class OrderPreserving := - { order_preserving_morphism :> Order_Morphism + { order_preserving_morphism :: Order_Morphism ; order_preserving : `(x ≤ y → f x ≤ f y) }. Class OrderReflecting := - { order_reflecting_morphism :> Order_Morphism + { order_reflecting_morphism :: Order_Morphism ; order_reflecting : `(f x ≤ f y → x ≤ y) }. Class OrderEmbedding := - { order_embedding_preserving :> OrderPreserving - ; order_embedding_reflecting :> OrderReflecting }. + { order_embedding_preserving :: OrderPreserving + ; order_embedding_reflecting :: OrderReflecting }. Class OrderIsomorphism `{!Inverse f} := - { order_iso_embedding :> OrderEmbedding - ; order_iso_surjective :> Surjective f }. + { order_iso_embedding :: OrderEmbedding + ; order_iso_surjective :: Surjective f }. Class StrictlyOrderPreserving := - { strictly_order_preserving_morphism :> StrictOrder_Morphism + { strictly_order_preserving_morphism :: StrictOrder_Morphism ; strictly_order_preserving : `(x < y → f x < f y) }. Class StrictlyOrderReflecting := - { strictly_order_reflecting_morphism :> StrictOrder_Morphism + { strictly_order_reflecting_morphism :: StrictOrder_Morphism ; strictly_order_reflecting : `(f x < f y → x < y) }. Class StrictOrderEmbedding := - { strict_order_embedding_preserving :> StrictlyOrderPreserving - ; strict_order_embedding_reflecting :> StrictlyOrderReflecting }. + { strict_order_embedding_preserving :: StrictlyOrderPreserving + ; strict_order_embedding_reflecting :: StrictlyOrderReflecting }. End order_maps. #[global] @@ -139,32 +139,32 @@ Davorin Lešnik's PhD thesis. *) Class SemiRingOrder `{Equiv A} `{Plus A} `{Mult A} `{Zero A} `{One A} (Ale : Le A) := - { srorder_po :> PartialOrder Ale + { srorder_po :: PartialOrder Ale ; srorder_semiring : SemiRing A ; srorder_partial_minus : ∀ x y, x ≤ y → ∃ z, y = x + z - ; srorder_plus :> ∀ z, OrderEmbedding (z +) + ; srorder_plus :: ∀ z, OrderEmbedding (z +) ; nonneg_mult_compat : ∀ x y, PropHolds (0 ≤ x) → PropHolds (0 ≤ y) → PropHolds (0 ≤ x * y) }. Class StrictSemiRingOrder `{Equiv A} `{Plus A} `{Mult A} `{Zero A} `{One A} (Alt : Lt A) := - { strict_srorder_so :> StrictSetoidOrder Alt + { strict_srorder_so :: StrictSetoidOrder Alt ; strict_srorder_semiring : SemiRing A ; strict_srorder_partial_minus : ∀ x y, x < y → ∃ z, y = x + z - ; strict_srorder_plus :> ∀ z, StrictOrderEmbedding (z +) + ; strict_srorder_plus :: ∀ z, StrictOrderEmbedding (z +) ; pos_mult_compat : ∀ x y, PropHolds (0 < x) → PropHolds (0 < y) → PropHolds (0 < x * y) }. Class PseudoSemiRingOrder `{Equiv A} `{Apart A} `{Plus A} `{Mult A} `{Zero A} `{One A} (Alt : Lt A) := - { pseudo_srorder_strict :> PseudoOrder Alt + { pseudo_srorder_strict :: PseudoOrder Alt ; pseudo_srorder_semiring : SemiRing A ; pseudo_srorder_partial_minus : ∀ x y, ¬y < x → ∃ z, y = x + z - ; pseudo_srorder_plus :> ∀ z, StrictOrderEmbedding (z +) - ; pseudo_srorder_mult_ext :> StrongSetoid_BinaryMorphism (.*.) + ; pseudo_srorder_plus :: ∀ z, StrictOrderEmbedding (z +) + ; pseudo_srorder_mult_ext :: StrongSetoid_BinaryMorphism (.*.) ; pseudo_srorder_pos_mult_compat : ∀ x y, PropHolds (0 < x) → PropHolds (0 < y) → PropHolds (0 < x * y) }. Class FullPseudoSemiRingOrder `{Equiv A} `{Apart A} `{Plus A} `{Mult A} `{Zero A} `{One A} (Ale : Le A) (Alt : Lt A) := - { full_pseudo_srorder_pso :> PseudoSemiRingOrder Alt + { full_pseudo_srorder_pso :: PseudoSemiRingOrder Alt ; full_pseudo_srorder_le_iff_not_lt_flip : ∀ x y, x ≤ y ↔ ¬y < x }. (* Due to bug #2528 *) @@ -177,8 +177,8 @@ Hint Extern 7 (PropHolds (0 ≤ _ * _)) => eapply @nonneg_mult_compat : typeclas Alternatively, we could have defined the standard notion of a RingOrder: Class RingOrder `{Equiv A} `{Plus A} `{Mult A} `{Zero A} (Ale : Le A) := - { ringorder_po :> PartialOrder Ale - ; ringorder_plus :> ∀ z, OrderPreserving (z +) + { ringorder_po :: PartialOrder Ale + ; ringorder_plus :: ∀ z, OrderPreserving (z +) ; ringorder_mult : ∀ x y, 0 ≤ x → 0 ≤ y → 0 ≤ x * y }. Unfortunately, this notion is too weak when we consider semirings (e.g. the @@ -190,8 +190,8 @@ Similarly we prove that a FullSemiRingOrder and a FullPseudoRingOrder are equiva Class FullPseudoRingOrder `{Equiv A} `{Apart A} `{Plus A} `{Mult A} `{Zero A} (Ale : Le A) (Alt : Lt A) := - { pseudo_ringorder_spo :> FullPseudoOrder Ale Alt - ; pseudo_ringorder_mult_ext :> StrongSetoid_BinaryMorphism (.*.) - ; pseudo_ringorder_plus :> ∀ z, StrictlyOrderPreserving (z +) + { pseudo_ringorder_spo :: FullPseudoOrder Ale Alt + ; pseudo_ringorder_mult_ext :: StrongSetoid_BinaryMorphism (.*.) + ; pseudo_ringorder_plus :: ∀ z, StrictlyOrderPreserving (z +) ; pseudo_ringorder_mult : ∀ x y, 0 < x → 0 < y → 0 < x * y }. *) diff --git a/interfaces/rationals.v b/interfaces/rationals.v index 3298895..afcdf29 100644 --- a/interfaces/rationals.v +++ b/interfaces/rationals.v @@ -18,7 +18,7 @@ implementation of the integers. *) Class Rationals A {e plus mult zero one neg recip} `{U : !RationalsToFrac A} : Prop := - { rationals_field:> @DecField A e plus mult zero one neg recip - ; rationals_frac :> ∀ `{Integers Z}, Injective (rationals_to_frac A Z) - ; rationals_frac_mor :> ∀ `{Integers Z}, SemiRing_Morphism (rationals_to_frac A Z) - ; rationals_embed_ints :> ∀ `{Integers Z}, Injective (integers_to_ring Z A) }. + { rationals_field:: @DecField A e plus mult zero one neg recip + ; rationals_frac :: ∀ `{Integers Z}, Injective (rationals_to_frac A Z) + ; rationals_frac_mor :: ∀ `{Integers Z}, SemiRing_Morphism (rationals_to_frac A Z) + ; rationals_embed_ints :: ∀ `{Integers Z}, Injective (integers_to_ring Z A) }. diff --git a/interfaces/sequences.v b/interfaces/sequences.v index 720ea29..1829c89 100644 --- a/interfaces/sequences.v +++ b/interfaces/sequences.v @@ -44,15 +44,15 @@ Section practical. `{!InjectToSeq free} `{!ExtendToSeq free}. Class Sequence := - { sequence_makes_monoids:> ∀ `{Setoid a}, Monoid (free a) - ; sequence_inject_morphism:> ∀ `{Setoid a}, Setoid_Morphism (inject a) - ; sequence_map_morphism:> ∀ `{Equiv x} `{Equiv y} (f: x → y), + { sequence_makes_monoids:: ∀ `{Setoid a}, Monoid (free a) + ; sequence_inject_morphism:: ∀ `{Setoid a}, Setoid_Morphism (inject a) + ; sequence_map_morphism:: ∀ `{Equiv x} `{Equiv y} (f: x → y), Setoid_Morphism f → Monoid_Morphism (raw_fmap _ _ f) ; sequence_fmap_proper: ∀ `{Equiv x} `{Equiv y} (f g: x → y), f = g → fmap free f = raw_fmap _ _ g ; sequence_fmap_id: ∀ `{Equiv x}, raw_fmap _ _ (@id x) = id ; sequence_fmap_comp: ∀ `{Equiv x} `{Equiv y} `{Equiv z} (f: y → z) (g: x → y), raw_fmap _ _ (f ∘ g) = raw_fmap _ _ f ∘ raw_fmap _ _ g - ; sequence_extend_makes_morphisms:> ∀ `{Equiv x} `{Monoid y} (f: x → y), + ; sequence_extend_makes_morphisms:: ∀ `{Equiv x} `{Monoid y} (f: x → y), Setoid_Morphism f → Monoid_Morphism (extend f) ; sequence_inject_natural: ∀ `{Setoid A} `{Setoid B} (f: A → B), Setoid_Morphism f → inject B ∘ f = raw_fmap _ _ f ∘ inject A diff --git a/interfaces/ua_basic.v b/interfaces/ua_basic.v index 6281d0a..b78463e 100644 --- a/interfaces/ua_basic.v +++ b/interfaces/ua_basic.v @@ -106,5 +106,5 @@ Class Algebra (carriers: sorts σ → Type) {e: ∀ a, Equiv (carriers a)} `{AlgebraOps σ carriers}: Prop := - { algebra_setoids:> ∀ a, Setoid (carriers a) - ; algebra_propers:> ∀ o: σ, Proper (=) (algebra_op o) }. + { algebra_setoids:: ∀ a, Setoid (carriers a) + ; algebra_propers:: ∀ o: σ, Proper (=) (algebra_op o) }. diff --git a/interfaces/universal_algebra.v b/interfaces/universal_algebra.v index 00af0bf..6701992 100644 --- a/interfaces/universal_algebra.v +++ b/interfaces/universal_algebra.v @@ -265,7 +265,7 @@ Class InVariety (carriers: sorts et → Type) {e: ∀ a, Equiv (carriers a)} `{!AlgebraOps et carriers}: Prop := - { variety_algebra:> Algebra et carriers + { variety_algebra:: Algebra et carriers ; variety_laws: ∀ s, et_laws et s → ∀ vars, eval_stmt et vars s }. Module op_type_notations. diff --git a/interfaces/vectorspace.v b/interfaces/vectorspace.v index 2d8c1f8..038e363 100644 --- a/interfaces/vectorspace.v +++ b/interfaces/vectorspace.v @@ -36,13 +36,13 @@ Class Module (R M : Type) {Me Mop Munit Mnegate} {sm : ScalarMult R M} := - { lm_ring :> @Ring R Re Rplus Rmult Rzero Rone Rnegate - ; lm_group :> @AbGroup M Me Mop Munit Mnegate - ; lm_distr_l :> LeftHeteroDistribute (·) (&) (&) - ; lm_distr_r :> RightHeteroDistribute (·) (+) (&) - ; lm_assoc :> HeteroAssociative (·) (·) (·) (.*.) - ; lm_identity :> LeftIdentity (·) 1 - ; scalar_mult_proper :> Proper ((=) ==> (=) ==> (=)) sm + { lm_ring :: @Ring R Re Rplus Rmult Rzero Rone Rnegate + ; lm_group :: @AbGroup M Me Mop Munit Mnegate + ; lm_distr_l :: LeftHeteroDistribute (·) (&) (&) + ; lm_distr_r :: RightHeteroDistribute (·) (+) (&) + ; lm_assoc :: HeteroAssociative (·) (·) (·) (.*.) + ; lm_identity :: LeftIdentity (·) 1 + ; scalar_mult_proper :: Proper ((=) ==> (=) ==> (=)) sm }. (* TODO K is commutative, so derive right module laws? *) @@ -54,9 +54,9 @@ Class Seminormed `{!Abs R} (n : Norm R M) := (* We have a module *) - { snm_module :> @Module R M Re Rplus Rmult Rzero Rone Rnegate + { snm_module :: @Module R M Re Rplus Rmult Rzero Rone Rnegate Me Mop Munit Mnegate Smult - ; snm_order :> @FullPseudoSemiRingOrder R Re Rapart Rplus Rmult Rzero Rone Rle Rlt + ; snm_order :: @FullPseudoSemiRingOrder R Re Rapart Rplus Rmult Rzero Rone Rle Rlt (* With respect to which our norm preserves the following: *) ; snm_scale : ∀ a v, ∥a · v∥ = (abs a) * ∥v∥ (* positive homgeneity *) @@ -73,9 +73,9 @@ Class VectorSpace (K V : Type) {Ve Vop Vunit Vnegate} (* vector operations *) {sm : ScalarMult K V} := - { vs_field :> @DecField K Ke Kplus Kmult Kzero Kone Knegate Krecip - ; vs_abgroup :> @AbGroup V Ve Vop Vunit Vnegate - ; vs_module :> @Module K V Ke Kplus Kmult Kzero Kone Knegate + { vs_field :: @DecField K Ke Kplus Kmult Kzero Kone Knegate Krecip + ; vs_abgroup :: @AbGroup V Ve Vop Vunit Vnegate + ; vs_module :: @Module K V Ke Kplus Kmult Kzero Kone Knegate Ve Vop Vunit Vnegate sm }. @@ -87,14 +87,14 @@ Class InnerProductSpace (K V : Type) {Ve Vop Vunit Vnegate} (* vector operations *) {sm : ScalarMult K V} {inp: Inproduct K V} {Kle: Le K} := - { in_vectorspace :> @VectorSpace K V Ke Kplus Kmult Kzero Kone Knegate + { in_vectorspace :: @VectorSpace K V Ke Kplus Kmult Kzero Kone Knegate Krecip Ve Vop Vunit Vnegate sm - ; in_srorder :> SemiRingOrder Kle - ; in_comm :> Commutative inprod + ; in_srorder :: SemiRingOrder Kle + ; in_comm :: Commutative inprod ; in_linear_l : ∀ a u v, ⟨a·u,v⟩ = a*⟨u,v⟩ - ; in_nonneg :> ∀ v, PropHolds (0 ≤ ⟨v,v⟩) (* TODO Le to strong? *) - ; in_mon_unit_zero :> ∀ v, 0 = ⟨v,v⟩ <-> v = mon_unit - ; inprod_proper :> Proper ((=) ==> (=) ==> (=)) (⟨⟩) + ; in_nonneg :: ∀ v, PropHolds (0 ≤ ⟨v,v⟩) (* TODO Le to strong? *) + ; in_mon_unit_zero :: ∀ v, 0 = ⟨v,v⟩ <-> v = mon_unit + ; inprod_proper :: Proper ((=) ==> (=) ==> (=)) (⟨⟩) }. (* TODO complex conjugate? @@ -115,7 +115,7 @@ Class SemiNormedSpace (K V : Type) {Ve Vop Vunit Vnegate} (* vector operations *) {sm : ScalarMult K V} := - { sn_vectorspace :> @VectorSpace K V Ke Kplus Kmult Kzero Kone Knegate + { sn_vectorspace :: @VectorSpace K V Ke Kplus Kmult Kzero Kone Knegate Krecip Ve Vop Vunit Vnegate sm ; sn_nonneg : ∀ v, 0 ≤ ∥v∥ (* non-negativity *) ; sn_scale : ∀ a v, ∥a · v∥ = (abs a) * ∥v∥ (* positive homgeneity *) diff --git a/theory/forget_variety.v b/theory/forget_variety.v index 8fdd413..37f5068 100644 --- a/theory/forget_variety.v +++ b/theory/forget_variety.v @@ -1,7 +1,7 @@ (* "Forgetting" a variety's laws (but keeping the algebraic operations) is a trivial functor. *) Require Import - MathClasses.interfaces.canonical_names MathClasses.interfaces.universal_algebra MathClasses.interfaces.functors + MathClasses.interfaces.canonical_names MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.interfaces.functors MathClasses.theory.categories MathClasses.categories.varieties MathClasses.categories.algebras. Section contents. diff --git a/theory/ring_ideals.v b/theory/ring_ideals.v index 2938f67..cd5ecff 100644 --- a/theory/ring_ideals.v +++ b/theory/ring_ideals.v @@ -8,8 +8,8 @@ Require Export (* Require ua_congruence varieties.rings. *) Class RingIdeal A (P : A → Prop) `{Ring A} : Prop := - { ideal_proper :> Proper ((=) ==> iff) P - ; ideal_NonEmpty :> NonEmpty (sig P) + { ideal_proper :: Proper ((=) ==> iff) P + ; ideal_NonEmpty :: NonEmpty (sig P) ; ideal_closed_plus_negate : ∀ x y, P x → P y → P (x - y) ; ideal_closed_mult_r : ∀ x y, P x → P (x * y) ; ideal_closed_mult_l: ∀ x y, P y → P (x * y) }. diff --git a/theory/ua_congruence.v b/theory/ua_congruence.v index ecbf24f..7b84c43 100644 --- a/theory/ua_congruence.v +++ b/theory/ua_congruence.v @@ -1,6 +1,6 @@ Require Import Coq.Classes.Morphisms Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions Coq.Lists.List - MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.interfaces.canonical_names MathClasses.theory.ua_subalgebraT MathClasses.misc.util. + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.interfaces.canonical_names MathClasses.theory.ua_subalgebraT MathClasses.misc.util. Require MathClasses.theory.ua_products. Require MathClasses.theory.categories. @@ -121,8 +121,8 @@ Section contents. (* This justifies the following definition of a congruence: *) Class Congruence: Prop := - { congruence_proper:> ∀ s: sorts σ, Proper ((=) ==> (=) ==> iff) (e s) - ; congruence_quotient:> Algebra σ v (e:=e) }. + { congruence_proper:: ∀ s: sorts σ, Proper ((=) ==> (=) ==> iff) (e s) + ; congruence_quotient:: Algebra σ v (e:=e) }. End contents. diff --git a/theory/ua_homomorphisms.v b/theory/ua_homomorphisms.v index 2f45671..7b527bd 100644 --- a/theory/ua_homomorphisms.v +++ b/theory/ua_homomorphisms.v @@ -23,7 +23,7 @@ Section contents. end. Class HomoMorphism: Prop := - { homo_proper:> ∀ a, Setoid_Morphism (@f a) + { homo_proper:: ∀ a, Setoid_Morphism (@f a) ; preserves: ∀ (o: σ), Preservation (A_ops o) (B_ops o) ; homo_source_algebra: Algebra σ A ; homo_target_algebra: Algebra σ B }. diff --git a/theory/ua_subalgebra.v b/theory/ua_subalgebra.v index 130185a..93c5736 100644 --- a/theory/ua_subalgebra.v +++ b/theory/ua_subalgebra.v @@ -25,7 +25,7 @@ Section subalgebras. Qed. Class ClosedSubset: Prop := - { subset_proper:> ∀ s, Proper ((=) ==> iff) (P s) + { subset_proper:: ∀ s, Proper ((=) ==> iff) (P s) ; subset_closed: ∀ o, op_closed (algebra_op o) }. (* Now suppose P is closed in this way. *) diff --git a/theory/ua_subvariety.v b/theory/ua_subvariety.v index d135add..48045dc 100644 --- a/theory/ua_subvariety.v +++ b/theory/ua_subvariety.v @@ -1,6 +1,6 @@ Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms Coq.Program.Program - MathClasses.interfaces.universal_algebra MathClasses.interfaces.canonical_names MathClasses.theory.ua_subalgebra. + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.interfaces.canonical_names MathClasses.theory.ua_subalgebra. (* In theory/ua_subalgebra.v we defined closed proper subsets and showed that they yield subalgebras. We now expand on this result and show that they