From 964ff97477c4f0df983373eaa9379ceb7fc48d50 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 19 Jan 2023 11:54:25 +0000 Subject: [PATCH 1/8] clean version of ring-op --- CHANGELOG.md | 86 +++----------------- src/Algebra/Construct/Flip/Op.agda | 121 +++++++++++++++++++---------- 2 files changed, 91 insertions(+), 116 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index e56fc6dcd8..935aab10d5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -653,7 +653,7 @@ Non-backwards compatible changes previous implementation using the sum type `a ⟶ b ⊎ b ⟶ a`. * In `Algebra.Morphism.Structures`, `IsNearSemiringHomomorphism`, - `IsSemiringHomomorphism`, and `IsRingHomomorphism` have been redeisgned to + `IsSemiringHomomorphism`, and `IsRingHomomorphism` have been redesigned to build up from `IsMonoidHomomorphism`, `IsNearSemiringHomomorphism`, and `IsSemiringHomomorphism` respectively, adding a single property at each step. This means that they no longer need to have two separate proofs of @@ -1140,26 +1140,6 @@ Deprecated names map₁₂-commute ↦ map₁₂-map₂₁ ``` -* In `Data.Tree.AVL`: - ``` - _∈?_ ↦ member - ``` - -* In `Data.Tree.AVL.IndexedMap`: - ``` - _∈?_ ↦ member - ``` - -* In `Data.Tree.AVL.Map`: - ``` - _∈?_ ↦ member - ``` - -* In `Data.Tree.AVL.Sets`: - ``` - _∈?_ ↦ member - ``` - * In `Data.Tree.Binary.Zipper.Properties`: ``` toTree-#nodes-commute ↦ toTree-#nodes @@ -1342,11 +1322,6 @@ New modules Data.List.Fresh.NonEmpty ``` -* A small library defining a structurally inductive view of lists: - ``` - Data.List.Relation.Unary.Sufficient - ``` - * Combinations and permutations for ℕ. ``` Data.Nat.Combinatorics @@ -1388,14 +1363,6 @@ New modules Data.Rational.Unnormalised.Show ``` -* Membership relations for maps and sets - ``` - Data.Tree.AVL.Map.Membership.Propositional - Data.Tree.AVL.Map.Membership.Propositional.Properties - Data.Tree.AVL.Sets.Membership - Data.Tree.AVL.Sets.Membership.Properties - ``` - * Properties of bijections: ``` Function.Consequences @@ -1620,6 +1587,14 @@ Other minor changes moufangLoop : MoufangLoop a ℓ₁ → MoufangLoop b ℓ₂ → MoufangLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂) ``` +* Added new functions and proofs to `Algebra.Construct.Flip.Op`: + ```agda + zero : Zero ≈ ε ∙ → Zero ≈ ε (flip ∙) + distributes : (≈ DistributesOver ∙) + → (≈ DistributesOver (flip ∙)) + + isRing : IsRing ≈ + * - 0# 1# → IsRing ≈ + (flip *) - 0# 1# + ring : Ring a ℓ → Ring a ℓ + ``` + * Added new definition to `Algebra.Definitions`: ```agda LeftDividesˡ : Op₂ A → Op₂ A → Set _ @@ -1883,18 +1858,6 @@ Other minor changes decide : Π[ P ∪ Q ] → Π[ All {R = R} P ∪ Any Q ] ``` -* Added new proofs to `Data.List.Membership.Propositional.Properties`: - ```agda - mapWith∈-id : mapWith∈ xs (λ {x} _ → x) ≡ xs - map-mapWith∈ : map g (mapWith∈ xs f) ≡ mapWith∈ xs (g ∘′ f) - ``` - -* Added new proofs to `Data.List.Membership.Setoid.Properties`: - ```agda - mapWith∈-id : mapWith∈ xs (λ {x} _ → x) ≡ xs - map-mapWith∈ : map g (mapWith∈ xs f) ≡ mapWith∈ xs (g ∘′ f) - ``` - * Add new proofs in `Data.List.Properties`: ```agda ∈⇒∣product : n ∈ ns → n ∣ product ns @@ -2053,17 +2016,6 @@ Other minor changes pattern `suc x = con (quote ℕ.suc) (x ⟨∷⟩ []) ``` -* Added new proofs in `Data.Parity.Properties`: - ```agda - suc-homo-⁻¹ : (parity (suc n)) ⁻¹ ≡ parity n - +-homo-+ : parity (m ℕ.+ n) ≡ parity m ℙ.+ parity n - *-homo-* : parity (m ℕ.* n) ≡ parity m ℙ.* parity n - parity-isMagmaHomomorphism : IsMagmaHomomorphism ℕ.+-rawMagma ℙ.+-rawMagma parity - parity-isMonoidHomomorphism : IsMonoidHomomorphism ℕ.+-0-rawMonoid ℙ.+-0-rawMonoid parity - parity-isNearSemiringHomomorphism : IsNearSemiringHomomorphism ℕ.+-*-rawNearSemiring ℙ.+-*-rawNearSemiring parity - parity-isSemiringHomomorphism : IsSemiringHomomorphism ℕ.+-*-rawSemiring ℙ.+-*-rawSemiring parity - ``` - * Added new rounding functions in `Data.Rational.Base`: ```agda floor ceiling truncate round ⌊_⌋ ⌈_⌉ [_] : ℚ → ℤ @@ -2143,16 +2095,6 @@ Other minor changes ×-≡,≡←≡ : p₁ ≡ p₂ → (proj₁ p₁ ≡ proj₁ p₂ × proj₂ p₁ ≡ proj₂ p₂) ``` -* Added new proof to `Data.Product.Relation.Binary.Lex.Strict` - ```agda - ×-respectsʳ : Transitive _≈₁_ → - _<₁_ Respectsʳ _≈₁_ → _<₂_ Respectsʳ _≈₂_ → _<ₗₑₓ_ Respectsʳ _≋_ - ×-respectsˡ : Symmetric _≈₁_ → Transitive _≈₁_ → - _<₁_ Respectsˡ _≈₁_ → _<₂_ Respectsˡ _≈₂_ → _<ₗₑₓ_ Respectsˡ _≋_ - ×-wellFounded' : Symmetric _≈₁_ → Transitive _≈₁_ → _<₁_ Respectsʳ _≈₁_ → - WellFounded _<₁_ → WellFounded _<₂_ → WellFounded _<ₗₑₓ_ - ``` - * Added new definitions to `Data.Sign.Base`: ```agda *-rawMagma : RawMagma 0ℓ 0ℓ @@ -2601,16 +2543,6 @@ Other minor changes flip′ : (A → B → C) → (B → A → C) ``` -* Added new proofs to `Data.List.Properties` - ```agda - cartesianProductWith-zeroˡ : cartesianProductWith f [] ys ≡ [] - cartesianProductWith-zeroʳ : cartesianProductWith f xs [] ≡ [] - cartesianProductWith-distribʳ-++ : cartesianProductWith f (xs ++ ys) zs ≡ - cartesianProductWith f xs zs ++ cartesianProductWith f ys zs - foldr-map : foldr f x (map g xs) ≡ foldr (g -⟨ f ∣) x xs - foldl-map : foldl f x (map g xs) ≡ foldl (∣ f ⟩- g) x xs - ``` - NonZero/Positive/Negative changes --------------------------------- diff --git a/src/Algebra/Construct/Flip/Op.agda b/src/Algebra/Construct/Flip/Op.agda index 471722cbd4..1075a1e942 100644 --- a/src/Algebra/Construct/Flip/Op.agda +++ b/src/Algebra/Construct/Flip/Op.agda @@ -9,7 +9,10 @@ module Algebra.Construct.Flip.Op where -open import Algebra +open import Algebra.Core +open import Algebra.Bundles +import Algebra.Definitions as Def +import Algebra.Structures as Str import Data.Product as Prod import Data.Sum as Sum open import Function.Base using (flip) @@ -33,136 +36,171 @@ preserves₂ : (∼ ≈ ≋ : Rel A ℓ) → ∙ Preserves₂ ∼ ⟶ ≈ ⟶ ≋ → (flip ∙) Preserves₂ ≈ ⟶ ∼ ⟶ ≋ preserves₂ _ _ _ pres = flip pres -module _ (≈ : Rel A ℓ) (∙ : Op₂ A) where +module ∙-Properties (≈ : Rel A ℓ) (∙ : Op₂ A) where - associative : Symmetric ≈ → Associative ≈ ∙ → Associative ≈ (flip ∙) + open Def ≈ + + associative : Symmetric ≈ → Associative ∙ → Associative (flip ∙) associative sym assoc x y z = sym (assoc z y x) - identity : Identity ≈ ε ∙ → Identity ≈ ε (flip ∙) + identity : Identity ε ∙ → Identity ε (flip ∙) identity id = Prod.swap id - commutative : Commutative ≈ ∙ → Commutative ≈ (flip ∙) + commutative : Commutative ∙ → Commutative (flip ∙) commutative comm = flip comm - selective : Selective ≈ ∙ → Selective ≈ (flip ∙) + selective : Selective ∙ → Selective (flip ∙) selective sel x y = Sum.swap (sel y x) - idempotent : Idempotent ≈ ∙ → Idempotent ≈ (flip ∙) + idempotent : Idempotent ∙ → Idempotent (flip ∙) idempotent idem = idem - inverse : Inverse ≈ ε ⁻¹ ∙ → Inverse ≈ ε ⁻¹ (flip ∙) + inverse : Inverse ε ⁻¹ ∙ → Inverse ε ⁻¹ (flip ∙) inverse inv = Prod.swap inv + zero : Zero ε ∙ → Zero ε (flip ∙) + zero zer = Prod.swap zer + +module *-Properties (≈ : Rel A ℓ) (* + : Op₂ A) where + + open Def ≈ + + distributes : * DistributesOver + → (flip *) DistributesOver + + distributes distrib = Prod.swap distrib + ------------------------------------------------------------------------ -- Structures module _ {≈ : Rel A ℓ} {∙ : Op₂ A} where - isMagma : IsMagma ≈ ∙ → IsMagma ≈ (flip ∙) + open Def ≈ + open Str ≈ + open ∙-Properties ≈ ∙ + + isMagma : IsMagma ∙ → IsMagma (flip ∙) isMagma m = record { isEquivalence = isEquivalence ; ∙-cong = preserves₂ ≈ ≈ ≈ ∙-cong } where open IsMagma m - isSelectiveMagma : IsSelectiveMagma ≈ ∙ → IsSelectiveMagma ≈ (flip ∙) + isSelectiveMagma : IsSelectiveMagma ∙ → IsSelectiveMagma (flip ∙) isSelectiveMagma m = record { isMagma = isMagma m.isMagma - ; sel = selective ≈ ∙ m.sel + ; sel = selective m.sel } where module m = IsSelectiveMagma m - isCommutativeMagma : IsCommutativeMagma ≈ ∙ → IsCommutativeMagma ≈ (flip ∙) + isCommutativeMagma : IsCommutativeMagma ∙ → IsCommutativeMagma (flip ∙) isCommutativeMagma m = record { isMagma = isMagma m.isMagma - ; comm = commutative ≈ ∙ m.comm + ; comm = commutative m.comm } where module m = IsCommutativeMagma m - isSemigroup : IsSemigroup ≈ ∙ → IsSemigroup ≈ (flip ∙) + isSemigroup : IsSemigroup ∙ → IsSemigroup (flip ∙) isSemigroup s = record { isMagma = isMagma s.isMagma - ; assoc = associative ≈ ∙ s.sym s.assoc + ; assoc = associative s.sym s.assoc } where module s = IsSemigroup s - isBand : IsBand ≈ ∙ → IsBand ≈ (flip ∙) + isBand : IsBand ∙ → IsBand (flip ∙) isBand b = record { isSemigroup = isSemigroup b.isSemigroup ; idem = b.idem } where module b = IsBand b - isCommutativeSemigroup : IsCommutativeSemigroup ≈ ∙ → - IsCommutativeSemigroup ≈ (flip ∙) + isCommutativeSemigroup : IsCommutativeSemigroup ∙ → + IsCommutativeSemigroup (flip ∙) isCommutativeSemigroup s = record { isSemigroup = isSemigroup s.isSemigroup - ; comm = commutative ≈ ∙ s.comm + ; comm = commutative s.comm } where module s = IsCommutativeSemigroup s - isUnitalMagma : IsUnitalMagma ≈ ∙ ε → IsUnitalMagma ≈ (flip ∙) ε + isUnitalMagma : IsUnitalMagma ∙ ε → IsUnitalMagma (flip ∙) ε isUnitalMagma m = record { isMagma = isMagma m.isMagma - ; identity = identity ≈ ∙ m.identity + ; identity = identity m.identity } where module m = IsUnitalMagma m - isMonoid : IsMonoid ≈ ∙ ε → IsMonoid ≈ (flip ∙) ε + isMonoid : IsMonoid ∙ ε → IsMonoid (flip ∙) ε isMonoid m = record { isSemigroup = isSemigroup m.isSemigroup - ; identity = identity ≈ ∙ m.identity + ; identity = identity m.identity } where module m = IsMonoid m - isCommutativeMonoid : IsCommutativeMonoid ≈ ∙ ε → - IsCommutativeMonoid ≈ (flip ∙) ε + isCommutativeMonoid : IsCommutativeMonoid ∙ ε → + IsCommutativeMonoid (flip ∙) ε isCommutativeMonoid m = record { isMonoid = isMonoid m.isMonoid - ; comm = commutative ≈ ∙ m.comm + ; comm = commutative m.comm } where module m = IsCommutativeMonoid m - isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid ≈ ∙ ε → - IsIdempotentCommutativeMonoid ≈ (flip ∙) ε + isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid ∙ ε → + IsIdempotentCommutativeMonoid (flip ∙) ε isIdempotentCommutativeMonoid m = record { isCommutativeMonoid = isCommutativeMonoid m.isCommutativeMonoid - ; idem = idempotent ≈ ∙ m.idem + ; idem = idempotent m.idem } where module m = IsIdempotentCommutativeMonoid m - isInvertibleMagma : IsInvertibleMagma ≈ ∙ ε ⁻¹ → - IsInvertibleMagma ≈ (flip ∙) ε ⁻¹ + isInvertibleMagma : IsInvertibleMagma ∙ ε ⁻¹ → + IsInvertibleMagma (flip ∙) ε ⁻¹ isInvertibleMagma m = record { isMagma = isMagma m.isMagma - ; inverse = inverse ≈ ∙ m.inverse + ; inverse = inverse m.inverse ; ⁻¹-cong = m.⁻¹-cong } where module m = IsInvertibleMagma m - isInvertibleUnitalMagma : IsInvertibleUnitalMagma ≈ ∙ ε ⁻¹ → - IsInvertibleUnitalMagma ≈ (flip ∙) ε ⁻¹ + isInvertibleUnitalMagma : IsInvertibleUnitalMagma ∙ ε ⁻¹ → + IsInvertibleUnitalMagma (flip ∙) ε ⁻¹ isInvertibleUnitalMagma m = record { isInvertibleMagma = isInvertibleMagma m.isInvertibleMagma - ; identity = identity ≈ ∙ m.identity + ; identity = identity m.identity } where module m = IsInvertibleUnitalMagma m - isGroup : IsGroup ≈ ∙ ε ⁻¹ → IsGroup ≈ (flip ∙) ε ⁻¹ + isGroup : IsGroup ∙ ε ⁻¹ → IsGroup (flip ∙) ε ⁻¹ isGroup g = record { isMonoid = isMonoid g.isMonoid - ; inverse = inverse ≈ ∙ g.inverse + ; inverse = inverse g.inverse ; ⁻¹-cong = g.⁻¹-cong } where module g = IsGroup g - isAbelianGroup : IsAbelianGroup ≈ ∙ ε ⁻¹ → IsAbelianGroup ≈ (flip ∙) ε ⁻¹ + isAbelianGroup : IsAbelianGroup ∙ ε ⁻¹ → IsAbelianGroup (flip ∙) ε ⁻¹ isAbelianGroup g = record { isGroup = isGroup g.isGroup - ; comm = commutative ≈ ∙ g.comm + ; comm = commutative g.comm } where module g = IsAbelianGroup g +module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where + + open Str ≈ + open ∙-Properties ≈ * + open *-Properties ≈ * + + + isRing : IsRing + * - 0# 1# → IsRing + (flip *) - 0# 1# + isRing r = record + { +-isAbelianGroup = r.+-isAbelianGroup + ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong + ; *-assoc = associative r.sym r.*-assoc + ; *-identity = identity r.*-identity + ; distrib = distributes r.distrib + ; zero = zero r.zero + } + where + module r = IsRing r + + ------------------------------------------------------------------------ -- Bundles @@ -239,3 +277,8 @@ group g = record { isGroup = isGroup g.isGroup } abelianGroup : AbelianGroup a ℓ → AbelianGroup a ℓ abelianGroup g = record { isAbelianGroup = isAbelianGroup g.isAbelianGroup } where module g = AbelianGroup g + +ring : Ring a ℓ → Ring a ℓ +ring r = record { isRing = isRing r.isRing } + where module r = Ring r + From e34ef1f5ffe2cc8bc2cf1984d0ef53e497ea878a Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 19 Jan 2023 11:58:05 +0000 Subject: [PATCH 2/8] tweak whitespace --- src/Algebra/Construct/Flip/Op.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Algebra/Construct/Flip/Op.agda b/src/Algebra/Construct/Flip/Op.agda index 1075a1e942..0ba10a871e 100644 --- a/src/Algebra/Construct/Flip/Op.agda +++ b/src/Algebra/Construct/Flip/Op.agda @@ -197,8 +197,7 @@ module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where ; distrib = distributes r.distrib ; zero = zero r.zero } - where - module r = IsRing r + where module r = IsRing r ------------------------------------------------------------------------ From 5b1aa77bf8a88dcd31dbccb4dc69b31c6c99209d Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 19 Jan 2023 14:28:26 +0000 Subject: [PATCH 3/8] added remaining structures/bundles --- CHANGELOG.md | 23 +++++ src/Algebra/Construct/Flip/Op.agda | 135 +++++++++++++++++++++++++++++ 2 files changed, 158 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 935aab10d5..4474e567bf 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1591,8 +1591,31 @@ Other minor changes ```agda zero : Zero ≈ ε ∙ → Zero ≈ ε (flip ∙) distributes : (≈ DistributesOver ∙) + → (≈ DistributesOver (flip ∙)) + + isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero + * 0# 1# → + IsSemiringWithoutAnnihilatingZero + (flip *) 0# 1# + isSemiring : IsSemiring + * 0# 1# → IsSemiring + (flip *) 0# 1# + isCommutativeSemiring : IsCommutativeSemiring + * 0# 1# → + IsCommutativeSemiring + (flip *) 0# 1# + isIdempotentSemiring : IsIdempotentSemiring + * 0# 1# → + IsIdempotentSemiring + (flip *) 0# 1# + isQuasiring : IsQuasiring + * 0# 1# → IsQuasiring + (flip *) 0# 1# + isRingWithoutOne : IsRingWithoutOne + * - 0# → IsRingWithoutOne + (flip *) - 0# + isNonAssociativeRing : IsNonAssociativeRing + * - 0# 1# → + IsNonAssociativeRing + (flip *) - 0# 1# isRing : IsRing ≈ + * - 0# 1# → IsRing ≈ + (flip *) - 0# 1# + isNearring : IsNearring + * 0# 1# - → IsNearring + (flip *) 0# 1# - + isCommutativeRing : IsCommutativeRing + * - 0# 1# → + IsCommutativeRing + (flip *) - 0# 1# + semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero a ℓ → + SemiringWithoutAnnihilatingZero a ℓ + commutativeSemiring : CommutativeSemiring a ℓ → CommutativeSemiring a ℓ + idempotentSemiring : IdempotentSemiring a ℓ → IdempotentSemiring a ℓ + quasiring : Quasiring a ℓ → Quasiring a ℓ + ringWithoutOne : RingWithoutOne a ℓ → RingWithoutOne a ℓ + nonAssociativeRing : NonAssociativeRing a ℓ → NonAssociativeRing a ℓ + nearring : Nearring a ℓ → Nearring a ℓ ring : Ring a ℓ → Ring a ℓ + commutativeRing : CommutativeRing a ℓ → CommutativeRing a ℓ ``` * Added new definition to `Algebra.Definitions`: diff --git a/src/Algebra/Construct/Flip/Op.agda b/src/Algebra/Construct/Flip/Op.agda index 0ba10a871e..295556e70f 100644 --- a/src/Algebra/Construct/Flip/Op.agda +++ b/src/Algebra/Construct/Flip/Op.agda @@ -182,12 +182,99 @@ module _ {≈ : Rel A ℓ} {∙ : Op₂ A} where } where module g = IsAbelianGroup g +module _ {≈ : Rel A ℓ} {+ * : Op₂ A} {0# 1# : A} where + + open Str ≈ + open ∙-Properties ≈ * + open *-Properties ≈ * + + + isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero + * 0# 1# → + IsSemiringWithoutAnnihilatingZero + (flip *) 0# 1# + isSemiringWithoutAnnihilatingZero r = record + { +-isCommutativeMonoid = r.+-isCommutativeMonoid + ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong + ; *-assoc = associative r.sym r.*-assoc + ; *-identity = identity r.*-identity + ; distrib = distributes r.distrib + } + where module r = IsSemiringWithoutAnnihilatingZero r + + isSemiring : IsSemiring + * 0# 1# → IsSemiring + (flip *) 0# 1# + isSemiring r = record + { isSemiringWithoutAnnihilatingZero = isSemiringWithoutAnnihilatingZero r.isSemiringWithoutAnnihilatingZero + ; zero = zero r.zero + } + where module r = IsSemiring r + + isCommutativeSemiring : IsCommutativeSemiring + * 0# 1# → + IsCommutativeSemiring + (flip *) 0# 1# + isCommutativeSemiring r = record + { isSemiring = isSemiring r.isSemiring + ; *-comm = commutative r.*-comm + } + where module r = IsCommutativeSemiring r + + isIdempotentSemiring : IsIdempotentSemiring + * 0# 1# → + IsIdempotentSemiring + (flip *) 0# 1# + isIdempotentSemiring r = record + { isSemiring = isSemiring r.isSemiring + ; +-idem = r.+-idem + } + where module r = IsIdempotentSemiring r + + isQuasiring : IsQuasiring + * 0# 1# → IsQuasiring + (flip *) 0# 1# + isQuasiring r = record + { +-isMonoid = r.+-isMonoid + ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong + ; *-assoc = associative r.sym r.*-assoc + ; *-identity = identity r.*-identity + ; distrib = distributes r.distrib + ; zero = zero r.zero + } + where module r = IsQuasiring r + +module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# : A} where + + open Str ≈ + open ∙-Properties ≈ * + open *-Properties ≈ * + + + isRingWithoutOne : IsRingWithoutOne + * - 0# → IsRingWithoutOne + (flip *) - 0# + isRingWithoutOne r = record + { +-isAbelianGroup = r.+-isAbelianGroup + ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong + ; *-assoc = associative r.sym r.*-assoc + ; distrib = distributes r.distrib + ; zero = zero r.zero + } + where module r = IsRingWithoutOne r + module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where open Str ≈ open ∙-Properties ≈ * open *-Properties ≈ * + + isNonAssociativeRing : IsNonAssociativeRing + * - 0# 1# → + IsNonAssociativeRing + (flip *) - 0# 1# + isNonAssociativeRing r = record + { +-isAbelianGroup = r.+-isAbelianGroup + ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong + --; *-assoc = associative r.sym r.*-assoc + ; identity = identity r.identity + ; distrib = distributes r.distrib + ; zero = zero r.zero + } + where module r = IsNonAssociativeRing r + + isNearring : IsNearring + * 0# 1# - → IsNearring + (flip *) 0# 1# - + isNearring r = record + { isQuasiring = isQuasiring r.isQuasiring -- + ; +-inverse = r.+-inverse + ; ⁻¹-cong = r.⁻¹-cong + } + where module r = IsNearring r + isRing : IsRing + * - 0# 1# → IsRing + (flip *) - 0# 1# isRing r = record { +-isAbelianGroup = r.+-isAbelianGroup @@ -199,6 +286,14 @@ module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where } where module r = IsRing r + isCommutativeRing : IsCommutativeRing + * - 0# 1# → + IsCommutativeRing + (flip *) - 0# 1# + isCommutativeRing r = record + { isRing = isRing r.isRing + ; *-comm = commutative r.*-comm + } + where module r = IsCommutativeRing r + ------------------------------------------------------------------------ -- Bundles @@ -277,7 +372,47 @@ abelianGroup : AbelianGroup a ℓ → AbelianGroup a ℓ abelianGroup g = record { isAbelianGroup = isAbelianGroup g.isAbelianGroup } where module g = AbelianGroup g +semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero a ℓ → + SemiringWithoutAnnihilatingZero a ℓ +semiringWithoutAnnihilatingZero r = record + { isSemiringWithoutAnnihilatingZero = isSemiringWithoutAnnihilatingZero r.isSemiringWithoutAnnihilatingZero } + where module r = SemiringWithoutAnnihilatingZero r + +semiring : Semiring a ℓ → Semiring a ℓ +semiring r = record { isSemiring = isSemiring r.isSemiring } + where module r = Semiring r + +commutativeSemiring : CommutativeSemiring a ℓ → CommutativeSemiring a ℓ +commutativeSemiring r = record + { isCommutativeSemiring = isCommutativeSemiring r.isCommutativeSemiring } + where module r = CommutativeSemiring r + +idempotentSemiring : IdempotentSemiring a ℓ → IdempotentSemiring a ℓ +idempotentSemiring r = record + { isIdempotentSemiring = isIdempotentSemiring r.isIdempotentSemiring } + where module r = IdempotentSemiring r + +quasiring : Quasiring a ℓ → Quasiring a ℓ +quasiring r = record { isQuasiring = isQuasiring r.isQuasiring } + where module r = Quasiring r + +ringWithoutOne : RingWithoutOne a ℓ → RingWithoutOne a ℓ +ringWithoutOne r = record { isRingWithoutOne = isRingWithoutOne r.isRingWithoutOne } + where module r = RingWithoutOne r + +nonAssociativeRing : NonAssociativeRing a ℓ → NonAssociativeRing a ℓ +nonAssociativeRing r = record + { isNonAssociativeRing = isNonAssociativeRing r.isNonAssociativeRing } + where module r = NonAssociativeRing r + +nearring : Nearring a ℓ → Nearring a ℓ +nearring r = record { isNearring = isNearring r.isNearring } + where module r = Nearring r + ring : Ring a ℓ → Ring a ℓ ring r = record { isRing = isRing r.isRing } where module r = Ring r +commutativeRing : CommutativeRing a ℓ → CommutativeRing a ℓ +commutativeRing r = record { isCommutativeRing = isCommutativeRing r.isCommutativeRing } + where module r = CommutativeRing r From 9c6291f2881ea41a3091c9ff960979bd8a67c8e1 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 19 Jan 2023 14:37:16 +0000 Subject: [PATCH 4/8] fix-whitespace --- src/Algebra/Construct/Flip/Op.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Construct/Flip/Op.agda b/src/Algebra/Construct/Flip/Op.agda index 295556e70f..3a6d031d42 100644 --- a/src/Algebra/Construct/Flip/Op.agda +++ b/src/Algebra/Construct/Flip/Op.agda @@ -269,7 +269,7 @@ module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where isNearring : IsNearring + * 0# 1# - → IsNearring + (flip *) 0# 1# - isNearring r = record - { isQuasiring = isQuasiring r.isQuasiring -- + { isQuasiring = isQuasiring r.isQuasiring -- ; +-inverse = r.+-inverse ; ⁻¹-cong = r.⁻¹-cong } From 9c4787ae20b7cd51be7906e96858453c44e9876e Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 19 Jan 2023 23:18:27 +0000 Subject: [PATCH 5/8] removed stray -- comment --- src/Algebra/Construct/Flip/Op.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Construct/Flip/Op.agda b/src/Algebra/Construct/Flip/Op.agda index 3a6d031d42..e93e504cfa 100644 --- a/src/Algebra/Construct/Flip/Op.agda +++ b/src/Algebra/Construct/Flip/Op.agda @@ -269,7 +269,7 @@ module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where isNearring : IsNearring + * 0# 1# - → IsNearring + (flip *) 0# 1# - isNearring r = record - { isQuasiring = isQuasiring r.isQuasiring -- + { isQuasiring = isQuasiring r.isQuasiring ; +-inverse = r.+-inverse ; ⁻¹-cong = r.⁻¹-cong } From ea33b16ee50f251e13ee281d70845607781438a5 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 19 Jan 2023 23:20:51 +0000 Subject: [PATCH 6/8] removed stray -- commented out field --- src/Algebra/Construct/Flip/Op.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Algebra/Construct/Flip/Op.agda b/src/Algebra/Construct/Flip/Op.agda index e93e504cfa..f7a51bdd87 100644 --- a/src/Algebra/Construct/Flip/Op.agda +++ b/src/Algebra/Construct/Flip/Op.agda @@ -260,7 +260,6 @@ module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where isNonAssociativeRing r = record { +-isAbelianGroup = r.+-isAbelianGroup ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong - --; *-assoc = associative r.sym r.*-assoc ; identity = identity r.identity ; distrib = distributes r.distrib ; zero = zero r.zero From d359243437fe19ec89c235b1c37a0d871f77186b Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 20 Jan 2023 01:02:10 +0000 Subject: [PATCH 7/8] cleaned up `CHANGELOG` I hope --- CHANGELOG.md | 78 +++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 77 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4474e567bf..a42555ea31 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -653,7 +653,7 @@ Non-backwards compatible changes previous implementation using the sum type `a ⟶ b ⊎ b ⟶ a`. * In `Algebra.Morphism.Structures`, `IsNearSemiringHomomorphism`, - `IsSemiringHomomorphism`, and `IsRingHomomorphism` have been redesigned to + `IsSemiringHomomorphism`, and `IsRingHomomorphism` have been redeisgned to build up from `IsMonoidHomomorphism`, `IsNearSemiringHomomorphism`, and `IsSemiringHomomorphism` respectively, adding a single property at each step. This means that they no longer need to have two separate proofs of @@ -1140,6 +1140,26 @@ Deprecated names map₁₂-commute ↦ map₁₂-map₂₁ ``` +* In `Data.Tree.AVL`: + ``` + _∈?_ ↦ member + ``` + +* In `Data.Tree.AVL.IndexedMap`: + ``` + _∈?_ ↦ member + ``` + +* In `Data.Tree.AVL.Map`: + ``` + _∈?_ ↦ member + ``` + +* In `Data.Tree.AVL.Sets`: + ``` + _∈?_ ↦ member + ``` + * In `Data.Tree.Binary.Zipper.Properties`: ``` toTree-#nodes-commute ↦ toTree-#nodes @@ -1322,6 +1342,11 @@ New modules Data.List.Fresh.NonEmpty ``` +* A small library defining a structurally inductive view of lists: + ``` + Data.List.Relation.Unary.Sufficient + ``` + * Combinations and permutations for ℕ. ``` Data.Nat.Combinatorics @@ -1363,6 +1388,14 @@ New modules Data.Rational.Unnormalised.Show ``` +* Membership relations for maps and sets + ``` + Data.Tree.AVL.Map.Membership.Propositional + Data.Tree.AVL.Map.Membership.Propositional.Properties + Data.Tree.AVL.Sets.Membership + Data.Tree.AVL.Sets.Membership.Properties + ``` + * Properties of bijections: ``` Function.Consequences @@ -1881,6 +1914,18 @@ Other minor changes decide : Π[ P ∪ Q ] → Π[ All {R = R} P ∪ Any Q ] ``` +* Added new proofs to `Data.List.Membership.Propositional.Properties`: + ```agda + mapWith∈-id : mapWith∈ xs (λ {x} _ → x) ≡ xs + map-mapWith∈ : map g (mapWith∈ xs f) ≡ mapWith∈ xs (g ∘′ f) + ``` + +* Added new proofs to `Data.List.Membership.Setoid.Properties`: + ```agda + mapWith∈-id : mapWith∈ xs (λ {x} _ → x) ≡ xs + map-mapWith∈ : map g (mapWith∈ xs f) ≡ mapWith∈ xs (g ∘′ f) + ``` + * Add new proofs in `Data.List.Properties`: ```agda ∈⇒∣product : n ∈ ns → n ∣ product ns @@ -2039,6 +2084,17 @@ Other minor changes pattern `suc x = con (quote ℕ.suc) (x ⟨∷⟩ []) ``` +* Added new proofs in `Data.Parity.Properties`: + ```agda + suc-homo-⁻¹ : (parity (suc n)) ⁻¹ ≡ parity n + +-homo-+ : parity (m ℕ.+ n) ≡ parity m ℙ.+ parity n + *-homo-* : parity (m ℕ.* n) ≡ parity m ℙ.* parity n + parity-isMagmaHomomorphism : IsMagmaHomomorphism ℕ.+-rawMagma ℙ.+-rawMagma parity + parity-isMonoidHomomorphism : IsMonoidHomomorphism ℕ.+-0-rawMonoid ℙ.+-0-rawMonoid parity + parity-isNearSemiringHomomorphism : IsNearSemiringHomomorphism ℕ.+-*-rawNearSemiring ℙ.+-*-rawNearSemiring parity + parity-isSemiringHomomorphism : IsSemiringHomomorphism ℕ.+-*-rawSemiring ℙ.+-*-rawSemiring parity + ``` + * Added new rounding functions in `Data.Rational.Base`: ```agda floor ceiling truncate round ⌊_⌋ ⌈_⌉ [_] : ℚ → ℤ @@ -2118,6 +2174,16 @@ Other minor changes ×-≡,≡←≡ : p₁ ≡ p₂ → (proj₁ p₁ ≡ proj₁ p₂ × proj₂ p₁ ≡ proj₂ p₂) ``` +* Added new proof to `Data.Product.Relation.Binary.Lex.Strict` + ```agda + ×-respectsʳ : Transitive _≈₁_ → + _<₁_ Respectsʳ _≈₁_ → _<₂_ Respectsʳ _≈₂_ → _<ₗₑₓ_ Respectsʳ _≋_ + ×-respectsˡ : Symmetric _≈₁_ → Transitive _≈₁_ → + _<₁_ Respectsˡ _≈₁_ → _<₂_ Respectsˡ _≈₂_ → _<ₗₑₓ_ Respectsˡ _≋_ + ×-wellFounded' : Symmetric _≈₁_ → Transitive _≈₁_ → _<₁_ Respectsʳ _≈₁_ → + WellFounded _<₁_ → WellFounded _<₂_ → WellFounded _<ₗₑₓ_ + ``` + * Added new definitions to `Data.Sign.Base`: ```agda *-rawMagma : RawMagma 0ℓ 0ℓ @@ -2566,6 +2632,16 @@ Other minor changes flip′ : (A → B → C) → (B → A → C) ``` +* Added new proofs to `Data.List.Properties` + ```agda + cartesianProductWith-zeroˡ : cartesianProductWith f [] ys ≡ [] + cartesianProductWith-zeroʳ : cartesianProductWith f xs [] ≡ [] + cartesianProductWith-distribʳ-++ : cartesianProductWith f (xs ++ ys) zs ≡ + cartesianProductWith f xs zs ++ cartesianProductWith f ys zs + foldr-map : foldr f x (map g xs) ≡ foldr (g -⟨ f ∣) x xs + foldl-map : foldl f x (map g xs) ≡ foldl (∣ f ⟩- g) x xs + ``` + NonZero/Positive/Negative changes --------------------------------- From 9265fa224a1919406cf5a19fd37698e84a2943ce Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 23 Jan 2023 14:10:20 +0000 Subject: [PATCH 8/8] last structure/bundle remaining --- CHANGELOG.md | 4 ++++ src/Algebra/Construct/Flip/Op.agda | 15 +++++++++++++++ 2 files changed, 19 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index a42555ea31..f5ea56b431 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1629,6 +1629,8 @@ Other minor changes isSemiring : IsSemiring + * 0# 1# → IsSemiring + (flip *) 0# 1# isCommutativeSemiring : IsCommutativeSemiring + * 0# 1# → IsCommutativeSemiring + (flip *) 0# 1# + isCancellativeCommutativeSemiring : IsCancellativeCommutativeSemiring + * 0# 1# → + IsCancellativeCommutativeSemiring + (flip *) 0# 1# isIdempotentSemiring : IsIdempotentSemiring + * 0# 1# → IsIdempotentSemiring + (flip *) 0# 1# isQuasiring : IsQuasiring + * 0# 1# → IsQuasiring + (flip *) 0# 1# @@ -1642,6 +1644,8 @@ Other minor changes semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero a ℓ → SemiringWithoutAnnihilatingZero a ℓ commutativeSemiring : CommutativeSemiring a ℓ → CommutativeSemiring a ℓ + cancellativeCommutativeSemiring : CancellativeCommutativeSemiring a ℓ → + CancellativeCommutativeSemiring a ℓ idempotentSemiring : IdempotentSemiring a ℓ → IdempotentSemiring a ℓ quasiring : Quasiring a ℓ → Quasiring a ℓ ringWithoutOne : RingWithoutOne a ℓ → RingWithoutOne a ℓ diff --git a/src/Algebra/Construct/Flip/Op.agda b/src/Algebra/Construct/Flip/Op.agda index f7a51bdd87..f693b03ab9 100644 --- a/src/Algebra/Construct/Flip/Op.agda +++ b/src/Algebra/Construct/Flip/Op.agda @@ -13,6 +13,7 @@ open import Algebra.Core open import Algebra.Bundles import Algebra.Definitions as Def import Algebra.Structures as Str +import Algebra.Consequences.Setoid as Consequences import Data.Product as Prod import Data.Sum as Sum open import Function.Base using (flip) @@ -214,6 +215,14 @@ module _ {≈ : Rel A ℓ} {+ * : Op₂ A} {0# 1# : A} where } where module r = IsCommutativeSemiring r + isCancellativeCommutativeSemiring : IsCancellativeCommutativeSemiring + * 0# 1# → + IsCancellativeCommutativeSemiring + (flip *) 0# 1# + isCancellativeCommutativeSemiring r = record + { isCommutativeSemiring = isCommutativeSemiring r.isCommutativeSemiring + ; *-cancelˡ-nonZero = Consequences.comm+almostCancelˡ⇒almostCancelʳ r.setoid r.*-comm r.*-cancelˡ-nonZero + } + where module r = IsCancellativeCommutativeSemiring r + isIdempotentSemiring : IsIdempotentSemiring + * 0# 1# → IsIdempotentSemiring + (flip *) 0# 1# isIdempotentSemiring r = record @@ -386,6 +395,12 @@ commutativeSemiring r = record { isCommutativeSemiring = isCommutativeSemiring r.isCommutativeSemiring } where module r = CommutativeSemiring r +cancellativeCommutativeSemiring : CancellativeCommutativeSemiring a ℓ → + CancellativeCommutativeSemiring a ℓ +cancellativeCommutativeSemiring r = record + { isCancellativeCommutativeSemiring = isCancellativeCommutativeSemiring r.isCancellativeCommutativeSemiring } + where module r = CancellativeCommutativeSemiring r + idempotentSemiring : IdempotentSemiring a ℓ → IdempotentSemiring a ℓ idempotentSemiring r = record { isIdempotentSemiring = isIdempotentSemiring r.isIdempotentSemiring }