From 7c198cc36581dd07c7ca4d60c7b7aa71b01d0e2b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 10 Jul 2025 14:56:22 +0100 Subject: [PATCH 01/27] add: `BooleanRing` plus `Properties` --- CHANGELOG.md | 22 ++++++- src/Algebra/Bundles.agda | 22 +++++++ src/Algebra/Properties/BooleanRing.agda | 85 +++++++++++++++++++++++++ src/Algebra/Structures.agda | 12 ++++ 4 files changed, 138 insertions(+), 3 deletions(-) create mode 100644 src/Algebra/Properties/BooleanRing.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 4b10f1a54e..a1199d8c4b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -163,6 +163,8 @@ New modules * `Algebra.Morphism.Construct.DirectProduct`. +* `Algebra.Properties.BooleanRing`. + * `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`. * `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`. @@ -186,6 +188,11 @@ New modules Additions to existing modules ----------------------------- +* In `Algebra.Bundles`: + ```agda + record BooleanRing _ _ : Set _ + ``` + * In `Algebra.Consequences.Base`: ```agda module Congruence (_≈_ : Rel A ℓ) (cong : Congruent₂ _≈_ _∙_) (refl : Reflexive _≈_) @@ -254,9 +261,13 @@ Additions to existing modules ∣ˡ-preorder : Preorder a ℓ _ ``` -* In `Algebra.Properties.Semigroup` adding consequences for associativity for semigroups +* In `Algebra.Properties.RingWithoutOne`: + ```agda + [-x][-y]≈xy : ∀ x y → - x * - y ≈ x * y + ``` -``` +* In `Algebra.Properties.Semigroup`, consequences for associativity for semigroups: + ``` uv≈w⇒xu∙v≈xw : ∀ x → (x ∙ u) ∙ v ≈ x ∙ w uv≈w⇒u∙vx≈wx : ∀ x → u ∙ (v ∙ x) ≈ w ∙ x uv≈w⇒u[vx∙y]≈w∙xy : ∀ x y → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ (x ∙ y) @@ -275,7 +286,7 @@ Additions to existing modules uv≈wx⇒yu∙v≈yw∙x : ∀ y → (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x uv≈wx⇒u∙vy≈w∙xy : ∀ y → u ∙ (v ∙ y) ≈ w ∙ (x ∙ y) uv≈wx⇒yu∙vz≈yw∙xz : ∀ y z → (y ∙ u) ∙ (v ∙ z) ≈ (y ∙ w) ∙ (x ∙ z) -``` + ``` * In `Algebra.Properties.Semigroup.Divisibility`: ```agda @@ -291,6 +302,11 @@ Additions to existing modules ∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b ``` +* In `Algebra.Structures`: + ```agda + record IsBooleanRing + * - 0# 1# : Set _ + ``` + * In `Data.Bool.Properties`: ```agda if-eta : ∀ b → (if b then x else x) ≡ x diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 88b195ec7d..9cec9731a3 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -1124,6 +1124,28 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where ; commutativeSemiringWithoutOne ) + +record BooleanRing c ℓ : Set (suc (c ⊔ ℓ)) where + infix 8 -_ + infixl 7 _*_ + infixl 6 _+_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _+_ : Op₂ Carrier + _*_ : Op₂ Carrier + -_ : Op₁ Carrier + 0# : Carrier + 1# : Carrier + isBooleanRing : IsBooleanRing _≈_ _+_ _*_ -_ 0# 1# + + open IsBooleanRing isBooleanRing public + + ring : Ring _ _ + ring = record { isRing = isRing } + + ------------------------------------------------------------------------ -- Bundles with 3 binary operations ------------------------------------------------------------------------ diff --git a/src/Algebra/Properties/BooleanRing.agda b/src/Algebra/Properties/BooleanRing.agda new file mode 100644 index 0000000000..b5822bef57 --- /dev/null +++ b/src/Algebra/Properties/BooleanRing.agda @@ -0,0 +1,85 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Some basic properties of Rings +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles + using (BooleanRing; CommutativeMonoid; IdempotentCommutativeMonoid; CommutativeRing) + +module Algebra.Properties.BooleanRing {r₁ r₂} (R : BooleanRing r₁ r₂) where + +open import Function.Base using (_$_) + +open BooleanRing R +open import Algebra.Definitions _≈_ +open import Algebra.Structures _≈_ + using (IsCommutativeMonoid; IsIdempotentCommutativeMonoid; IsCommutativeRing) +open import Relation.Binary.Reasoning.Setoid setoid + +------------------------------------------------------------------------ +-- Export properties of rings + +open import Algebra.Properties.Ring ring public + +------------------------------------------------------------------------ +-- Extra properties of Boolean rings + +xy+yx≈0 : ∀ x y → x * y + y * x ≈ 0# +xy+yx≈0 x y = +-cancelˡ (x * x) _ _ $ +-cancelʳ (y * y) _ _ $ begin + x * x + ((x * y) + (y * x)) + y * y ≈⟨ +-congʳ (+-assoc _ _ _) ⟨ + x * x + x * y + y * x + y * y ≈⟨ +-assoc _ _ _ ⟩ + (x * x + x * y) + (y * x + y * y) ≈⟨ +-cong (distribˡ x x y) (distribˡ y x y) ⟨ + x * (x + y) + y * (x + y) ≈⟨ distribʳ (x + y) x y ⟨ + (x + y) * (x + y) ≈⟨ *-idem (x + y) ⟩ + x + y ≈⟨ +-congˡ (*-idem y) ⟨ + x + y * y ≈⟨ +-congʳ (*-idem x) ⟨ + x * x + y * y ≈⟨ +-congʳ (+-identityʳ (x * x)) ⟨ + x * x + 0# + y * y ∎ + +x+x≈0 : ∀ x → x + x ≈ 0# +x+x≈0 x = begin + x + x ≈⟨ +-cong (*-idem x) (*-idem x) ⟨ + x * x + x * x ≈⟨ xy+yx≈0 x x ⟩ + 0# ∎ + +-x≈x : ∀ x → - x ≈ x +-x≈x x = begin + - x ≈⟨ +-inverseˡ-unique x x (x+x≈0 x) ⟨ + x ∎ + +*-comm : Commutative _*_ +*-comm x y = begin + x * y ≈⟨ +-inverseˡ-unique _ _ (xy+yx≈0 x y) ⟩ + - (y * x) ≈⟨ -x≈x _ ⟩ + y * x ∎ + +------------------------------------------------------------------------ +-- Additional structures + +*-isCommutativeMonoid : IsCommutativeMonoid _*_ 1# +*-isCommutativeMonoid = record { isMonoid = *-isMonoid ; comm = *-comm } + +*-isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _*_ 1# +*-isIdempotentCommutativeMonoid = record + { isCommutativeMonoid = *-isCommutativeMonoid + ; idem = *-idem + } + +isCommutativeRing : IsCommutativeRing _+_ _*_ -_ 0# 1# +isCommutativeRing = record { isRing = isRing ; *-comm = *-comm } + +------------------------------------------------------------------------ +-- Additional bundles + +*-commutativeMonoid : CommutativeMonoid _ _ +*-commutativeMonoid = record { isCommutativeMonoid = *-isCommutativeMonoid } + +*-idempotentCommutativeMonoid : IdempotentCommutativeMonoid _ _ +*-idempotentCommutativeMonoid = record + { isIdempotentCommutativeMonoid = *-isIdempotentCommutativeMonoid } + +commutativeRing : CommutativeRing _ _ +commutativeRing = record { isCommutativeRing = isCommutativeRing } diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 1b465c6d0f..8f6629f583 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -962,6 +962,18 @@ record IsCommutativeRing ; *-isCommutativeMonoid ) +record IsBooleanRing + (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where + field + isRing : IsRing + * - 0# 1# + *-idem : Idempotent * + + open IsRing isRing public + + isIdempotentMonoid : IsIdempotentMonoid * 1# + isIdempotentMonoid = record { isMonoid = *-isMonoid ; idem = *-idem } + + ------------------------------------------------------------------------ -- Structures with 3 binary operations ------------------------------------------------------------------------ From b219c5e24ac0b2e120e59db2ddfcb6bee0db245b Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Thu, 10 Jul 2025 15:09:20 +0100 Subject: [PATCH 02/27] Update CHANGELOG.md Removed spurious entry --- CHANGELOG.md | 4 ---- 1 file changed, 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a1199d8c4b..ac3976a093 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -261,10 +261,6 @@ Additions to existing modules ∣ˡ-preorder : Preorder a ℓ _ ``` -* In `Algebra.Properties.RingWithoutOne`: - ```agda - [-x][-y]≈xy : ∀ x y → - x * - y ≈ x * y - ``` * In `Algebra.Properties.Semigroup`, consequences for associativity for semigroups: ``` From 3e5cc883e8171f0baaa9f60db06587e989a15829 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 11 Jul 2025 07:01:32 +0100 Subject: [PATCH 03/27] refactor: more general API --- src/Algebra/Properties/BooleanRing.agda | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) diff --git a/src/Algebra/Properties/BooleanRing.agda b/src/Algebra/Properties/BooleanRing.agda index b5822bef57..398e60ba37 100644 --- a/src/Algebra/Properties/BooleanRing.agda +++ b/src/Algebra/Properties/BooleanRing.agda @@ -11,7 +11,7 @@ open import Algebra.Bundles module Algebra.Properties.BooleanRing {r₁ r₂} (R : BooleanRing r₁ r₂) where -open import Function.Base using (_$_) +open import Function.Base using (_∘_; _$_) open BooleanRing R open import Algebra.Definitions _≈_ @@ -39,17 +39,25 @@ xy+yx≈0 x y = +-cancelˡ (x * x) _ _ $ +-cancelʳ (y * y) _ _ $ begin x * x + y * y ≈⟨ +-congʳ (+-identityʳ (x * x)) ⟨ x * x + 0# + y * y ∎ -x+x≈0 : ∀ x → x + x ≈ 0# -x+x≈0 x = begin - x + x ≈⟨ +-cong (*-idem x) (*-idem x) ⟨ - x * x + x * x ≈⟨ xy+yx≈0 x x ⟩ +y≈x⇒x+y≈0 : ∀ {x y} → y ≈ x → x + y ≈ 0# +y≈x⇒x+y≈0 {x = x} {y = y} y≈x = begin + x + y ≈⟨ +-cong (*-idem x) (*-idem y) ⟨ + x * x + y * y ≈⟨ +-cong (*-congˡ (sym y≈x)) (*-congˡ y≈x) ⟩ + x * y + y * x ≈⟨ xy+yx≈0 x y ⟩ 0# ∎ --x≈x : ∀ x → - x ≈ x --x≈x x = begin +x+x≈0 : ∀ x → x + x ≈ 0# +x+x≈0 x = y≈x⇒x+y≈0 refl + +x+y≈0⇒y≈x : ∀ {x y} → x + y ≈ 0# → y ≈ x +x+y≈0⇒y≈x {x = x} {y = y} x+y≈0 = begin + y ≈⟨ +-inverseʳ-unique x y x+y≈0 ⟩ - x ≈⟨ +-inverseˡ-unique x x (x+x≈0 x) ⟨ x ∎ +-x≈x : ∀ x → - x ≈ x +-x≈x = x+y≈0⇒y≈x ∘ -‿inverseʳ + *-comm : Commutative _*_ *-comm x y = begin x * y ≈⟨ +-inverseˡ-unique _ _ (xy+yx≈0 x y) ⟩ From 9684d715248e71e677686ec03ab16957db03bb62 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 11 Jul 2025 07:05:31 +0100 Subject: [PATCH 04/27] fix: added note to `CHANGELOG` --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index ac3976a093..fe7f0e6104 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -302,6 +302,7 @@ Additions to existing modules ```agda record IsBooleanRing + * - 0# 1# : Set _ ``` + NB. based on `IsRing`, rather than `IsRingWithoutOne`. * In `Data.Bool.Properties`: ```agda From 0f2f44e3d4d0b0d7b18357f051753ccb7fabd18a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 11 Jul 2025 13:24:45 +0100 Subject: [PATCH 05/27] refactor: make binomial expansion an explicit step --- CHANGELOG.md | 8 ++++++++ src/Algebra/Consequences/Propositional.agda | 10 ++++++++++ src/Algebra/Consequences/Setoid.agda | 15 +++++++++++++++ src/Algebra/Properties/BooleanRing.agda | 6 +++--- 4 files changed, 36 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index fe7f0e6104..ac1d43b001 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -201,11 +201,19 @@ Additions to existing modules ∙-congʳ : RightCongruent _≈_ _∙_ ``` +* In `Algebra.Consequences.Propositional`: + ```agda + binomial-expansion : Associative _∙_ → _◦_ DistributesOver _∙_ → + ∀ w x y z → ((w ∙ x) ◦ (y ∙ z)) ≡ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z)) + ``` + * In `Algebra.Consequences.Setoid`: ```agda module Congruence (cong : Congruent₂ _≈_ _∙_) where ∙-congˡ : LeftCongruent _≈_ _∙_ ∙-congʳ : RightCongruent _≈_ _∙_ + binomial-expansion : Congruent₂ _∙_ → Associative _∙_ → _◦_ DistributesOver _∙_ → + ∀ w x y z → ((w ∙ x) ◦ (y ∙ z)) ≈ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z)) ``` * In `Algebra.Construct.Pointwise`: diff --git a/src/Algebra/Consequences/Propositional.agda b/src/Algebra/Consequences/Propositional.agda index 42892f4aa9..f975cdef5e 100644 --- a/src/Algebra/Consequences/Propositional.agda +++ b/src/Algebra/Consequences/Propositional.agda @@ -42,6 +42,7 @@ open Base public ; subst∧comm⇒sym ; wlog ; sel⇒idem + ; binomial-expansion -- plus all the deprecated versions of the above ; comm+assoc⇒middleFour ; identity+middleFour⇒assoc @@ -101,6 +102,15 @@ module _ {_∙_ _◦_ : Op₂ A} (∙-comm : Commutative _∙_) where comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y ∙ z)) ≡ ((x ◦ y) ∙ (x ◦ z))) comm⇒sym[distribˡ] = Base.comm⇒sym[distribˡ] (cong₂ _◦_) ∙-comm +module _ {_∙_ _◦_ : Op₂ A} + (∙-assoc : Associative _∙_) + (distrib : _◦_ DistributesOver _∙_) + where + + binomial-expansion : ∀ w x y z → + ((w ∙ x) ◦ (y ∙ z)) ≡ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z)) + binomial-expansion = Base.binomial-expansion {_∙_} {_◦_} (cong₂ _) ∙-assoc distrib + ------------------------------------------------------------------------ -- Selectivity diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda index 244470231c..4d6bb4dbba 100644 --- a/src/Algebra/Consequences/Setoid.agda +++ b/src/Algebra/Consequences/Setoid.agda @@ -292,6 +292,21 @@ module _ {_∙_ _◦_ : Op₂ A} (x ◦ (x ∙ z)) ∙ (y ◦ (x ∙ z)) ≈⟨ ◦-distribʳ-∙ _ _ _ ⟨ (x ∙ y) ◦ (x ∙ z) ∎ +module _ {_∙_ _◦_ : Op₂ A} + (∙-cong : Congruent₂ _∙_) + (∙-assoc : Associative _∙_) + (distrib@(distribˡ , distribʳ) : _◦_ DistributesOver _∙_) + where + + binomial-expansion : ∀ w x y z → + ((w ∙ x) ◦ (y ∙ z)) ≈ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z)) + binomial-expansion w x y z = begin + (w ∙ x) ◦ (y ∙ z) ≈⟨ distribʳ _ _ _ ⟩ + (w ◦ (y ∙ z)) ∙ (x ◦ (y ∙ z)) ≈⟨ ∙-cong (distribˡ _ _ _) (distribˡ _ _ _) ⟩ + ((w ◦ y) ∙ (w ◦ z)) ∙ ((x ◦ y) ∙ (x ◦ z)) ≈⟨ ∙-assoc _ _ _ ⟨ + (((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z) ∎ + + ------------------------------------------------------------------------ -- Ring-like structures diff --git a/src/Algebra/Properties/BooleanRing.agda b/src/Algebra/Properties/BooleanRing.agda index 398e60ba37..8a0505ad8a 100644 --- a/src/Algebra/Properties/BooleanRing.agda +++ b/src/Algebra/Properties/BooleanRing.agda @@ -14,6 +14,7 @@ module Algebra.Properties.BooleanRing {r₁ r₂} (R : BooleanRing r₁ r₂) wh open import Function.Base using (_∘_; _$_) open BooleanRing R +open import Algebra.Consequences.Setoid setoid using (binomial-expansion) open import Algebra.Definitions _≈_ open import Algebra.Structures _≈_ using (IsCommutativeMonoid; IsIdempotentCommutativeMonoid; IsCommutativeRing) @@ -30,14 +31,13 @@ open import Algebra.Properties.Ring ring public xy+yx≈0 : ∀ x y → x * y + y * x ≈ 0# xy+yx≈0 x y = +-cancelˡ (x * x) _ _ $ +-cancelʳ (y * y) _ _ $ begin x * x + ((x * y) + (y * x)) + y * y ≈⟨ +-congʳ (+-assoc _ _ _) ⟨ - x * x + x * y + y * x + y * y ≈⟨ +-assoc _ _ _ ⟩ - (x * x + x * y) + (y * x + y * y) ≈⟨ +-cong (distribˡ x x y) (distribˡ y x y) ⟨ - x * (x + y) + y * (x + y) ≈⟨ distribʳ (x + y) x y ⟨ + x * x + x * y + y * x + y * y ≈⟨ expand x y x y ⟨ (x + y) * (x + y) ≈⟨ *-idem (x + y) ⟩ x + y ≈⟨ +-congˡ (*-idem y) ⟨ x + y * y ≈⟨ +-congʳ (*-idem x) ⟨ x * x + y * y ≈⟨ +-congʳ (+-identityʳ (x * x)) ⟨ x * x + 0# + y * y ∎ + where expand = binomial-expansion +-cong +-assoc distrib y≈x⇒x+y≈0 : ∀ {x y} → y ≈ x → x + y ≈ 0# y≈x⇒x+y≈0 {x = x} {y = y} y≈x = begin From 0aff0d93659e17ef05522ee31971b2f945f1874e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Jul 2025 13:36:03 +0100 Subject: [PATCH 06/27] rename: `*-isIdempotentMonoid` --- src/Algebra/Structures.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 8f6629f583..d4ffd601af 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -970,8 +970,8 @@ record IsBooleanRing open IsRing isRing public - isIdempotentMonoid : IsIdempotentMonoid * 1# - isIdempotentMonoid = record { isMonoid = *-isMonoid ; idem = *-idem } + *-isIdempotentMonoid : IsIdempotentMonoid * 1# + *-isIdempotentMonoid = record { isMonoid = *-isMonoid ; idem = *-idem } ------------------------------------------------------------------------ From ca6aff1b31a76e34d0a5b03192dcbb54cacddbb8 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Jul 2025 13:36:39 +0100 Subject: [PATCH 07/27] add: `*-idempotentMonoid` --- src/Algebra/Bundles.agda | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 9cec9731a3..7598fe8b8f 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -1145,6 +1145,9 @@ record BooleanRing c ℓ : Set (suc (c ⊔ ℓ)) where ring : Ring _ _ ring = record { isRing = isRing } + *-idempotentMonoid : IdempotentMonoid c ℓ + *-idempotentMonoid = record { isIdempotentMonoid = *-isIdempotentMonoid } + ------------------------------------------------------------------------ -- Bundles with 3 binary operations From a4b6010b162308341fb91cea8bd2bebefebbfeff Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Jul 2025 13:37:15 +0100 Subject: [PATCH 08/27] refactor: use `Cancellative` properties only --- src/Algebra/Properties/BooleanRing.agda | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/Algebra/Properties/BooleanRing.agda b/src/Algebra/Properties/BooleanRing.agda index 8a0505ad8a..3770e4520e 100644 --- a/src/Algebra/Properties/BooleanRing.agda +++ b/src/Algebra/Properties/BooleanRing.agda @@ -50,19 +50,19 @@ x+x≈0 : ∀ x → x + x ≈ 0# x+x≈0 x = y≈x⇒x+y≈0 refl x+y≈0⇒y≈x : ∀ {x y} → x + y ≈ 0# → y ≈ x -x+y≈0⇒y≈x {x = x} {y = y} x+y≈0 = begin - y ≈⟨ +-inverseʳ-unique x y x+y≈0 ⟩ - - x ≈⟨ +-inverseˡ-unique x x (x+x≈0 x) ⟨ - x ∎ +x+y≈0⇒y≈x {x = x} {y = y} x+y≈0 = +-cancelˡ x _ _ $ begin + x + y ≈⟨ x+y≈0 ⟩ + 0# ≈⟨ x+x≈0 x ⟨ + x + x ∎ -x≈x : ∀ x → - x ≈ x -x≈x = x+y≈0⇒y≈x ∘ -‿inverseʳ *-comm : Commutative _*_ -*-comm x y = begin - x * y ≈⟨ +-inverseˡ-unique _ _ (xy+yx≈0 x y) ⟩ - - (y * x) ≈⟨ -x≈x _ ⟩ - y * x ∎ +*-comm x y = +-cancelʳ (y * x) _ _ $ begin + x * y + y * x ≈⟨ xy+yx≈0 x y ⟩ + 0# ≈⟨ x+x≈0 (y * x) ⟨ + y * x + y * x ∎ ------------------------------------------------------------------------ -- Additional structures From 9e3d63bc82bb46fea61c7c53b8a39ac7573e35b6 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 15 Jul 2025 10:42:13 +0100 Subject: [PATCH 09/27] add: stub properties for `CommutativeRing` --- CHANGELOG.md | 8 +- src/Algebra/Bundles.agda | 36 +++++- src/Algebra/Properties/BooleanSemiring.agda | 124 ++++++++++++++++++++ src/Algebra/Properties/CommutativeRing.agda | 24 ++++ src/Algebra/Structures.agda | 58 ++++++++- 5 files changed, 238 insertions(+), 12 deletions(-) create mode 100644 src/Algebra/Properties/BooleanSemiring.agda create mode 100644 src/Algebra/Properties/CommutativeRing.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index ac1d43b001..a4546cc246 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -165,6 +165,8 @@ New modules * `Algebra.Properties.BooleanRing`. +* `Algebra.Properties.BooleanSemiring`. + * `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`. * `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`. @@ -190,7 +192,8 @@ Additions to existing modules * In `Algebra.Bundles`: ```agda - record BooleanRing _ _ : Set _ + record BooleanSemiring _ _ : Set _ + record BooleanRing _ _ : Set _ ``` * In `Algebra.Consequences.Base`: @@ -308,9 +311,10 @@ Additions to existing modules * In `Algebra.Structures`: ```agda + record IsBooleanSemiring + * 0# 1# : Set _ record IsBooleanRing + * - 0# 1# : Set _ ``` - NB. based on `IsRing`, rather than `IsRingWithoutOne`. + NB. the latter is based on `IsCommutativeRing`, with the former on `IsSemiring`. * In `Data.Bool.Properties`: ```agda diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 7598fe8b8f..38ff46d8a8 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -921,6 +921,31 @@ record Quasiring c ℓ : Set (suc (c ⊔ ℓ)) where ; rawMonoid to *-rawMonoid ) +record BooleanSemiring c ℓ : Set (suc (c ⊔ ℓ)) where + infixl 7 _*_ + infixl 6 _+_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _+_ : Op₂ Carrier + _*_ : Op₂ Carrier + 0# : Carrier + 1# : Carrier + isBooleanSemiring : IsBooleanSemiring _≈_ _+_ _*_ 0# 1# + + open IsBooleanSemiring isBooleanSemiring public + + semiring : Semiring _ _ + semiring = record { isSemiring = isSemiring } + + *-idempotentMonoid : IdempotentMonoid c ℓ + *-idempotentMonoid = record { isIdempotentMonoid = *-isIdempotentMonoid } + + open IdempotentMonoid *-idempotentMonoid public + using () renaming (band to *-band) + + ------------------------------------------------------------------------ -- Bundles with 2 binary operations, 1 unary operation & 1 element ------------------------------------------------------------------------ @@ -1142,11 +1167,14 @@ record BooleanRing c ℓ : Set (suc (c ⊔ ℓ)) where open IsBooleanRing isBooleanRing public - ring : Ring _ _ - ring = record { isRing = isRing } + commutativeRing : CommutativeRing _ _ + commutativeRing = record { isCommutativeRing = isCommutativeRing } - *-idempotentMonoid : IdempotentMonoid c ℓ - *-idempotentMonoid = record { isIdempotentMonoid = *-isIdempotentMonoid } + booleanSemiring : BooleanSemiring _ _ + booleanSemiring = record { isBooleanSemiring = isBooleanSemiring } + + open BooleanSemiring booleanSemiring public + using (*-idempotentMonoid) ------------------------------------------------------------------------ diff --git a/src/Algebra/Properties/BooleanSemiring.agda b/src/Algebra/Properties/BooleanSemiring.agda new file mode 100644 index 0000000000..5f381b9226 --- /dev/null +++ b/src/Algebra/Properties/BooleanSemiring.agda @@ -0,0 +1,124 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Some basic properties of Rings +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles + using (BooleanSemiring; BooleanRing + ; CommutativeMonoid; IdempotentCommutativeMonoid + ; Ring; CommutativeRing) + +module Algebra.Properties.BooleanSemiring + {c ℓ} (booleanSemiring : BooleanSemiring c ℓ) where + +open import Data.Product.Base using (_,_) +open import Function.Base using (id; _∘_; _$_) + +open BooleanSemiring booleanSemiring +open import Algebra.Consequences.Setoid setoid using (binomial-expansion) +open import Algebra.Definitions _≈_ +open import Algebra.Structures _≈_ + using (IsCommutativeMonoid; IsIdempotentCommutativeMonoid + ; IsGroup; IsAbelianGroup + ; IsRing; IsCommutativeRing; IsBooleanRing + ) +open import Relation.Binary.Reasoning.Setoid setoid + +------------------------------------------------------------------------ +-- Export properties of rings +{- +open import Algebra.Properties.Semiring semiring public +-} +------------------------------------------------------------------------ +-- Extra properties of Boolean rings + +xy+yx≈0 : ∀ x y → x * y + y * x ≈ 0# +xy+yx≈0 x y = +-cancelˡ (x * x) _ _ $ +-cancelʳ (y * y) _ _ $ begin + x * x + ((x * y) + (y * x)) + y * y ≈⟨ +-congʳ (+-assoc _ _ _) ⟨ + x * x + x * y + y * x + y * y ≈⟨ expand x y x y ⟨ + (x + y) * (x + y) ≈⟨ *-idem (x + y) ⟩ + x + y ≈⟨ +-congˡ (*-idem y) ⟨ + x + y * y ≈⟨ +-congʳ (*-idem x) ⟨ + x * x + y * y ≈⟨ +-congʳ (+-identityʳ (x * x)) ⟨ + x * x + 0# + y * y ∎ + where expand = binomial-expansion +-cong +-assoc distrib + +y≈x⇒x+y≈0 : ∀ {x y} → y ≈ x → x + y ≈ 0# +y≈x⇒x+y≈0 {x = x} {y = y} y≈x = begin + x + y ≈⟨ +-cong (*-idem x) (*-idem y) ⟨ + x * x + y * y ≈⟨ +-cong (*-congˡ (sym y≈x)) (*-congˡ y≈x) ⟩ + x * y + y * x ≈⟨ xy+yx≈0 x y ⟩ + 0# ∎ + +x+x≈0 : ∀ x → x + x ≈ 0# +x+x≈0 x = y≈x⇒x+y≈0 refl + +x+y≈0⇒y≈x : ∀ {x y} → x + y ≈ 0# → y ≈ x +x+y≈0⇒y≈x {x = x} {y = y} x+y≈0 = +-cancelˡ x _ _ $ begin + x + y ≈⟨ x+y≈0 ⟩ + 0# ≈⟨ x+x≈0 x ⟨ + x + x ∎ + +*-comm : Commutative _*_ +*-comm x y = +-cancelʳ (y * x) _ _ $ begin + x * y + y * x ≈⟨ xy+yx≈0 x y ⟩ + 0# ≈⟨ x+x≈0 (y * x) ⟨ + y * x + y * x ∎ + +------------------------------------------------------------------------ +-- Additional structures + ++-isGroup : IsGroup _+_ 0# id ++-isGroup = record { isMonoid = +-isMonoid ; inverse = x+x≈0 , x+x≈0 ; ⁻¹-cong = id } + ++-isAbelianGroup : IsAbelianGroup _+_ 0# id ++-isAbelianGroup = record { isGroup = +-isGroup ; comm = +-comm } + +*-isCommutativeMonoid : IsCommutativeMonoid _*_ 1# +*-isCommutativeMonoid = record { isMonoid = *-isMonoid ; comm = *-comm } + +*-isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _*_ 1# +*-isIdempotentCommutativeMonoid = record + { isCommutativeMonoid = *-isCommutativeMonoid + ; idem = *-idem + } + +open IsIdempotentCommutativeMonoid *-isIdempotentCommutativeMonoid public + using () renaming (isCommutativeBand to *-isCommutativeBand) + +isRing : IsRing _+_ _*_ id 0# 1# +isRing = record + { +-isAbelianGroup = +-isAbelianGroup + ; *-cong = *-cong + ; *-assoc = *-assoc + ; *-identity = *-identity + ; distrib = distrib + } + +isCommutativeRing : IsCommutativeRing _+_ _*_ id 0# 1# +isCommutativeRing = record { isRing = isRing ; *-comm = *-comm } + +isBooleanRing : IsBooleanRing _+_ _*_ id 0# 1# +isBooleanRing = record { isCommutativeRing = isCommutativeRing ; *-idem = *-idem } + +------------------------------------------------------------------------ +-- Additional bundles + +*-commutativeMonoid : CommutativeMonoid _ _ +*-commutativeMonoid = record { isCommutativeMonoid = *-isCommutativeMonoid } + +*-idempotentCommutativeMonoid : IdempotentCommutativeMonoid _ _ +*-idempotentCommutativeMonoid = record + { isIdempotentCommutativeMonoid = *-isIdempotentCommutativeMonoid } + +open IdempotentCommutativeMonoid *-idempotentCommutativeMonoid public + using () renaming (commutativeBand to *-commutativeBand) + +commutativeRing : CommutativeRing _ _ +commutativeRing = record { isCommutativeRing = isCommutativeRing } + +booleanRing : BooleanRing _ _ +booleanRing = record { isBooleanRing = isBooleanRing } diff --git a/src/Algebra/Properties/CommutativeRing.agda b/src/Algebra/Properties/CommutativeRing.agda new file mode 100644 index 0000000000..02a09f1891 --- /dev/null +++ b/src/Algebra/Properties/CommutativeRing.agda @@ -0,0 +1,24 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Some basic properties of Commutative Rings +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra using (CommutativeRing) + +module Algebra.Properties.CommutativeRing + {c ℓ} (commutativeRing : CommutativeRing c ℓ) where + +open CommutativeRing commutativeRing + + +------------------------------------------------------------------------ +-- Export properties of rings + +open import Algebra.Properties.Ring ring public + +------------------------------------------------------------------------ +-- Properties arising from commutativity + diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index d4ffd601af..5d8ee56b09 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -26,6 +26,7 @@ open import Algebra.Definitions _≈_ import Algebra.Consequences.Setoid as Consequences open import Data.Product.Base using (_,_; proj₁; proj₂) open import Level using (_⊔_) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning ------------------------------------------------------------------------ -- Structures with 1 unary operation & 1 element @@ -732,6 +733,27 @@ record IsQuasiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where ; identityʳ to *-identityʳ ) +record IsBooleanSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where + field + isSemiring : IsSemiring + * 0# 1# + +-cancel : Cancellative + + *-idem : Idempotent * + + open IsSemiring isSemiring public + + +-cancelˡ : LeftCancellative + + +-cancelˡ = proj₁ +-cancel + + +-cancelʳ : RightCancellative + + +-cancelʳ = proj₂ +-cancel + + *-isIdempotentMonoid : IsIdempotentMonoid * 1# + *-isIdempotentMonoid = record { isMonoid = *-isMonoid ; idem = *-idem } + + open IsIdempotentMonoid *-isIdempotentMonoid public + using () renaming (isBand to *-isBand) + + ------------------------------------------------------------------------ -- Structures with 2 binary operations, 1 unary operation & 1 element ------------------------------------------------------------------------ @@ -962,16 +984,40 @@ record IsCommutativeRing ; *-isCommutativeMonoid ) + record IsBooleanRing (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where field - isRing : IsRing + * - 0# 1# - *-idem : Idempotent * - - open IsRing isRing public + isCommutativeRing : IsCommutativeRing + * - 0# 1# + *-idem : Idempotent * + + open IsCommutativeRing isCommutativeRing public + + +-cancelˡ : LeftCancellative + + +-cancelˡ x y z x+y≈x+z = begin + y ≈⟨ +-identityˡ y ⟨ + + 0# y ≈⟨ +-congʳ (-‿inverseˡ x) ⟨ + + (+ (- x) x) y ≈⟨ +-assoc (- x) x y ⟩ + + (- x) (+ x y) ≈⟨ +-congˡ x+y≈x+z ⟩ + + (- x) (+ x z) ≈⟨ +-assoc (- x) x z ⟨ + + (+ (- x) x) z ≈⟨ +-congʳ (-‿inverseˡ x) ⟩ + + 0# z ≈⟨ +-identityˡ z ⟩ + z ∎ + where open ≈-Reasoning setoid + + +-cancelʳ : RightCancellative + + +-cancelʳ x y z y+x≈z+x = + Consequences.comm∧cancelˡ⇒cancelʳ setoid +-comm +-cancelˡ x y z y+x≈z+x + + isBooleanSemiring : IsBooleanSemiring + * 0# 1# + isBooleanSemiring = record + { isSemiring = isSemiring + ; +-cancel = +-cancelˡ , +-cancelʳ + ; *-idem = *-idem + } - *-isIdempotentMonoid : IsIdempotentMonoid * 1# - *-isIdempotentMonoid = record { isMonoid = *-isMonoid ; idem = *-idem } + open IsBooleanSemiring isBooleanSemiring public + using (*-isIdempotentMonoid) ------------------------------------------------------------------------ From 0e266690bd2d728f9359503fb9d20df09e10b2f4 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 15 Jul 2025 10:43:35 +0100 Subject: [PATCH 10/27] refactor: `BooleanRing` properties in terms of `CommutativeRing` and `BooleanSemiring` --- src/Algebra/Properties/BooleanSemiring.agda | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Properties/BooleanSemiring.agda b/src/Algebra/Properties/BooleanSemiring.agda index 5f381b9226..d7ee1dcbd3 100644 --- a/src/Algebra/Properties/BooleanSemiring.agda +++ b/src/Algebra/Properties/BooleanSemiring.agda @@ -28,12 +28,12 @@ open import Algebra.Structures _≈_ open import Relation.Binary.Reasoning.Setoid setoid ------------------------------------------------------------------------ --- Export properties of rings +-- Export properties of semirings {- open import Algebra.Properties.Semiring semiring public -} ------------------------------------------------------------------------ --- Extra properties of Boolean rings +-- Extra properties of Boolean semirings xy+yx≈0 : ∀ x y → x * y + y * x ≈ 0# xy+yx≈0 x y = +-cancelˡ (x * x) _ _ $ +-cancelʳ (y * y) _ _ $ begin @@ -120,5 +120,8 @@ open IdempotentCommutativeMonoid *-idempotentCommutativeMonoid public commutativeRing : CommutativeRing _ _ commutativeRing = record { isCommutativeRing = isCommutativeRing } +open CommutativeRing commutativeRing public + using (ring) + booleanRing : BooleanRing _ _ booleanRing = record { isBooleanRing = isBooleanRing } From 57928874dd250f5fa247be9d2c7ce65af7e94cdc Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 15 Jul 2025 10:44:08 +0100 Subject: [PATCH 11/27] refactor: put everything together --- src/Algebra/Bundles.agda | 25 +++++-- src/Algebra/Properties/BooleanRing.agda | 91 +++++++------------------ src/Algebra/Structures.agda | 26 ------- 3 files changed, 45 insertions(+), 97 deletions(-) diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 38ff46d8a8..5bc6a497b8 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -1131,7 +1131,10 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where ring : Ring _ _ ring = record { isRing = isRing } - open Ring ring public using (_≉_; rawRing; +-invertibleMagma; +-invertibleUnitalMagma; +-group; +-abelianGroup) + open Ring ring public + using (_≉_; rawRing + ; +-invertibleMagma; +-invertibleUnitalMagma + ; +-group; +-abelianGroup) commutativeSemiring : CommutativeSemiring _ _ commutativeSemiring = @@ -1166,15 +1169,27 @@ record BooleanRing c ℓ : Set (suc (c ⊔ ℓ)) where isBooleanRing : IsBooleanRing _≈_ _+_ _*_ -_ 0# 1# open IsBooleanRing isBooleanRing public + using (isCommutativeRing; isSemiring; *-idem) commutativeRing : CommutativeRing _ _ commutativeRing = record { isCommutativeRing = isCommutativeRing } - booleanSemiring : BooleanSemiring _ _ - booleanSemiring = record { isBooleanSemiring = isBooleanSemiring } + open CommutativeRing commutativeRing public + using + (_≉_; rawRing; setoid + ; +-invertibleMagma; +-invertibleUnitalMagma + ; +-group; +-abelianGroup + ; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma + ; +-semigroup; +-commutativeSemigroup + ; *-rawMagma; *-magma; *-commutativeMagma; *-semigroup; *-commutativeSemigroup + ; +-rawMonoid; +-monoid; +-commutativeMonoid + ; *-rawMonoid; *-monoid; *-commutativeMonoid + ; nearSemiring; semiringWithoutOne + ; semiringWithoutAnnihilatingZero; semiring + ; commutativeSemiringWithoutOne; commutativeSemiring + ; ring + ) - open BooleanSemiring booleanSemiring public - using (*-idempotentMonoid) ------------------------------------------------------------------------ diff --git a/src/Algebra/Properties/BooleanRing.agda b/src/Algebra/Properties/BooleanRing.agda index 3770e4520e..0af8e5c862 100644 --- a/src/Algebra/Properties/BooleanRing.agda +++ b/src/Algebra/Properties/BooleanRing.agda @@ -1,93 +1,52 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Some basic properties of Rings +-- Some basic properties of Boolean Rings ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra.Bundles - using (BooleanRing; CommutativeMonoid; IdempotentCommutativeMonoid; CommutativeRing) + using (CommutativeRing; BooleanSemiring; BooleanRing) -module Algebra.Properties.BooleanRing {r₁ r₂} (R : BooleanRing r₁ r₂) where +module Algebra.Properties.BooleanRing + {c ℓ} (booleanRing : BooleanRing c ℓ) where -open import Function.Base using (_∘_; _$_) +open import Data.Product.Base using (_,_) -open BooleanRing R -open import Algebra.Consequences.Setoid setoid using (binomial-expansion) -open import Algebra.Definitions _≈_ +open BooleanRing booleanRing open import Algebra.Structures _≈_ - using (IsCommutativeMonoid; IsIdempotentCommutativeMonoid; IsCommutativeRing) + using (IsBooleanSemiring) open import Relation.Binary.Reasoning.Setoid setoid ------------------------------------------------------------------------ --- Export properties of rings +-- Re-export properties of Commutative Rings -open import Algebra.Properties.Ring ring public +open import Algebra.Properties.CommutativeRing commutativeRing public ------------------------------------------------------------------------ --- Extra properties of Boolean rings +-- Structures -xy+yx≈0 : ∀ x y → x * y + y * x ≈ 0# -xy+yx≈0 x y = +-cancelˡ (x * x) _ _ $ +-cancelʳ (y * y) _ _ $ begin - x * x + ((x * y) + (y * x)) + y * y ≈⟨ +-congʳ (+-assoc _ _ _) ⟨ - x * x + x * y + y * x + y * y ≈⟨ expand x y x y ⟨ - (x + y) * (x + y) ≈⟨ *-idem (x + y) ⟩ - x + y ≈⟨ +-congˡ (*-idem y) ⟨ - x + y * y ≈⟨ +-congʳ (*-idem x) ⟨ - x * x + y * y ≈⟨ +-congʳ (+-identityʳ (x * x)) ⟨ - x * x + 0# + y * y ∎ - where expand = binomial-expansion +-cong +-assoc distrib - -y≈x⇒x+y≈0 : ∀ {x y} → y ≈ x → x + y ≈ 0# -y≈x⇒x+y≈0 {x = x} {y = y} y≈x = begin - x + y ≈⟨ +-cong (*-idem x) (*-idem y) ⟨ - x * x + y * y ≈⟨ +-cong (*-congˡ (sym y≈x)) (*-congˡ y≈x) ⟩ - x * y + y * x ≈⟨ xy+yx≈0 x y ⟩ - 0# ∎ - -x+x≈0 : ∀ x → x + x ≈ 0# -x+x≈0 x = y≈x⇒x+y≈0 refl - -x+y≈0⇒y≈x : ∀ {x y} → x + y ≈ 0# → y ≈ x -x+y≈0⇒y≈x {x = x} {y = y} x+y≈0 = +-cancelˡ x _ _ $ begin - x + y ≈⟨ x+y≈0 ⟩ - 0# ≈⟨ x+x≈0 x ⟨ - x + x ∎ - --x≈x : ∀ x → - x ≈ x --x≈x = x+y≈0⇒y≈x ∘ -‿inverseʳ +isBooleanSemiring : IsBooleanSemiring _+_ _*_ 0# 1# +isBooleanSemiring = record + { isSemiring = isSemiring + ; +-cancel = +-cancel + ; *-idem = *-idem + } -*-comm : Commutative _*_ -*-comm x y = +-cancelʳ (y * x) _ _ $ begin - x * y + y * x ≈⟨ xy+yx≈0 x y ⟩ - 0# ≈⟨ x+x≈0 (y * x) ⟨ - y * x + y * x ∎ +open IsBooleanSemiring isBooleanSemiring public + using (*-isIdempotentMonoid) ------------------------------------------------------------------------ --- Additional structures +-- Bundles -*-isCommutativeMonoid : IsCommutativeMonoid _*_ 1# -*-isCommutativeMonoid = record { isMonoid = *-isMonoid ; comm = *-comm } +booleanSemiring : BooleanSemiring _ _ +booleanSemiring = record { isBooleanSemiring = isBooleanSemiring } -*-isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _*_ 1# -*-isIdempotentCommutativeMonoid = record - { isCommutativeMonoid = *-isCommutativeMonoid - ; idem = *-idem - } - -isCommutativeRing : IsCommutativeRing _+_ _*_ -_ 0# 1# -isCommutativeRing = record { isRing = isRing ; *-comm = *-comm } +open BooleanSemiring booleanSemiring public + using (*-idempotentMonoid) ------------------------------------------------------------------------ --- Additional bundles - -*-commutativeMonoid : CommutativeMonoid _ _ -*-commutativeMonoid = record { isCommutativeMonoid = *-isCommutativeMonoid } - -*-idempotentCommutativeMonoid : IdempotentCommutativeMonoid _ _ -*-idempotentCommutativeMonoid = record - { isIdempotentCommutativeMonoid = *-isIdempotentCommutativeMonoid } +-- Export properties of Boolean semirings -commutativeRing : CommutativeRing _ _ -commutativeRing = record { isCommutativeRing = isCommutativeRing } +open import Algebra.Properties.BooleanSemiring booleanSemiring public diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 5d8ee56b09..a92d24f8d2 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -993,32 +993,6 @@ record IsBooleanRing open IsCommutativeRing isCommutativeRing public - +-cancelˡ : LeftCancellative + - +-cancelˡ x y z x+y≈x+z = begin - y ≈⟨ +-identityˡ y ⟨ - + 0# y ≈⟨ +-congʳ (-‿inverseˡ x) ⟨ - + (+ (- x) x) y ≈⟨ +-assoc (- x) x y ⟩ - + (- x) (+ x y) ≈⟨ +-congˡ x+y≈x+z ⟩ - + (- x) (+ x z) ≈⟨ +-assoc (- x) x z ⟨ - + (+ (- x) x) z ≈⟨ +-congʳ (-‿inverseˡ x) ⟩ - + 0# z ≈⟨ +-identityˡ z ⟩ - z ∎ - where open ≈-Reasoning setoid - - +-cancelʳ : RightCancellative + - +-cancelʳ x y z y+x≈z+x = - Consequences.comm∧cancelˡ⇒cancelʳ setoid +-comm +-cancelˡ x y z y+x≈z+x - - isBooleanSemiring : IsBooleanSemiring + * 0# 1# - isBooleanSemiring = record - { isSemiring = isSemiring - ; +-cancel = +-cancelˡ , +-cancelʳ - ; *-idem = *-idem - } - - open IsBooleanSemiring isBooleanSemiring public - using (*-isIdempotentMonoid) - ------------------------------------------------------------------------ -- Structures with 3 binary operations From e355a3f15a366f30a2c5dc28462a1dd6d20fcf1d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 15 Jul 2025 10:45:06 +0100 Subject: [PATCH 12/27] add: stub properties for `CommutativeRing` --- CHANGELOG.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index a4546cc246..42f2f1a4e9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -167,6 +167,8 @@ New modules * `Algebra.Properties.BooleanSemiring`. +* `Algebra.Properties.CommutativeRing`. + * `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`. * `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`. From 81d140cce55bc794cbb805aad516672bce3cfda4 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 15 Jul 2025 11:08:15 +0100 Subject: [PATCH 13/27] refactor: adjust re-exports --- src/Algebra/Bundles.agda | 7 ++++--- src/Algebra/Properties/BooleanRing.agda | 8 ++++++++ src/Algebra/Properties/Ring.agda | 10 +++------- 3 files changed, 15 insertions(+), 10 deletions(-) diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 5bc6a497b8..adeb87752b 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -1169,14 +1169,16 @@ record BooleanRing c ℓ : Set (suc (c ⊔ ℓ)) where isBooleanRing : IsBooleanRing _≈_ _+_ _*_ -_ 0# 1# open IsBooleanRing isBooleanRing public - using (isCommutativeRing; isSemiring; *-idem) + using (isCommutativeRing; *-idem) + + open IsCommutativeRing isCommutativeRing public commutativeRing : CommutativeRing _ _ commutativeRing = record { isCommutativeRing = isCommutativeRing } open CommutativeRing commutativeRing public using - (_≉_; rawRing; setoid + (_≉_; rawRing ; +-invertibleMagma; +-invertibleUnitalMagma ; +-group; +-abelianGroup ; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma @@ -1191,7 +1193,6 @@ record BooleanRing c ℓ : Set (suc (c ⊔ ℓ)) where ) - ------------------------------------------------------------------------ -- Bundles with 3 binary operations ------------------------------------------------------------------------ diff --git a/src/Algebra/Properties/BooleanRing.agda b/src/Algebra/Properties/BooleanRing.agda index 0af8e5c862..48262f26fc 100644 --- a/src/Algebra/Properties/BooleanRing.agda +++ b/src/Algebra/Properties/BooleanRing.agda @@ -12,6 +12,7 @@ open import Algebra.Bundles module Algebra.Properties.BooleanRing {c ℓ} (booleanRing : BooleanRing c ℓ) where +open import Function.Base using (_∘_) open import Data.Product.Base using (_,_) open BooleanRing booleanRing @@ -50,3 +51,10 @@ open BooleanSemiring booleanSemiring public -- Export properties of Boolean semirings open import Algebra.Properties.BooleanSemiring booleanSemiring public + +------------------------------------------------------------------------ +-- Further consequences + +-x≈x : ∀ x → - x ≈ x +-x≈x = x+y≈0⇒y≈x ∘ -‿inverseʳ + diff --git a/src/Algebra/Properties/Ring.agda b/src/Algebra/Properties/Ring.agda index 461a9a040b..4f8eb31a14 100644 --- a/src/Algebra/Properties/Ring.agda +++ b/src/Algebra/Properties/Ring.agda @@ -8,19 +8,15 @@ open import Algebra using (Ring) -module Algebra.Properties.Ring {r₁ r₂} (R : Ring r₁ r₂) where +module Algebra.Properties.Ring {c ℓ} (ring : Ring c ℓ) where -open Ring R - -import Algebra.Properties.RingWithoutOne as RingWithoutOneProperties -open import Function.Base using (_$_) +open Ring ring open import Relation.Binary.Reasoning.Setoid setoid -open import Algebra.Definitions _≈_ ------------------------------------------------------------------------ -- Export properties of rings without a 1#. -open RingWithoutOneProperties ringWithoutOne public +open import Algebra.Properties.RingWithoutOne ringWithoutOne public ------------------------------------------------------------------------ -- Extra properties of 1# From a1b4086aa93a0786e794c9b76f4557664e9fbef7 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 16 Jul 2025 14:54:05 +0100 Subject: [PATCH 14/27] add: `BooleanAlgebra` yields `BooleanRing` etc. --- CHANGELOG.md | 6 +++++ .../Lattice/Properties/BooleanAlgebra.agda | 27 ++++++++++++------- 2 files changed, 23 insertions(+), 10 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 42f2f1a4e9..3ae2fa358a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -250,6 +250,12 @@ Additions to existing modules commutativeRing : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ) ``` +* In `Algebra.Lattice.Properties.BooleanAlgebra.XorRing`: + ```agda + ⊕-∧-isBooleanRing : IsBooleanRing _⊕_ _∧_ id ⊥ ⊤ + ⊕-∧-booleanRing : BooleanRing _ _ + ``` + * In `Algebra.Modules.Properties`: ```agda inverseˡ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → x ≈ -ᴹ y diff --git a/src/Algebra/Lattice/Properties/BooleanAlgebra.agda b/src/Algebra/Lattice/Properties/BooleanAlgebra.agda index 43a05cb2ba..b3d236bb74 100644 --- a/src/Algebra/Lattice/Properties/BooleanAlgebra.agda +++ b/src/Algebra/Lattice/Properties/BooleanAlgebra.agda @@ -6,30 +6,31 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Algebra.Lattice.Bundles +open import Algebra.Lattice.Bundles using (BooleanAlgebra) module Algebra.Lattice.Properties.BooleanAlgebra - {b₁ b₂} (B : BooleanAlgebra b₁ b₂) + {c ℓ} (booleanAlgebra : BooleanAlgebra c ℓ) where -open BooleanAlgebra B +open import Algebra.Bundles + using (CommutativeSemiring; CommutativeRing; BooleanRing) +open import Algebra.Core using (Op₂) +open import Data.Product.Base using (_,_) +open import Function.Base using (id; _$_; _⟨_⟩_) +open import Function.Bundles using (_⇔_; module Equivalence) -import Algebra.Lattice.Properties.DistributiveLattice as DistribLatticeProperties -open import Algebra.Core using (Op₁; Op₂) +open BooleanAlgebra booleanAlgebra open import Algebra.Structures _≈_ open import Algebra.Definitions _≈_ open import Algebra.Consequences.Setoid setoid -open import Algebra.Bundles using (CommutativeSemiring; CommutativeRing) open import Algebra.Lattice.Structures _≈_ open import Relation.Binary.Reasoning.Setoid setoid -open import Function.Base using (id; _$_; _⟨_⟩_) -open import Function.Bundles using (_⇔_; module Equivalence) -open import Data.Product.Base using (_,_) + ------------------------------------------------------------------------ -- Export properties from distributive lattices -open DistribLatticeProperties distributiveLattice public +open import Algebra.Lattice.Properties.DistributiveLattice distributiveLattice public ------------------------------------------------------------------------ -- The dual construction is also a boolean algebra @@ -529,6 +530,12 @@ module XorRing { isCommutativeRing = ⊕-∧-isCommutativeRing } + ⊕-∧-isBooleanRing : IsBooleanRing _⊕_ _∧_ id ⊥ ⊤ + ⊕-∧-isBooleanRing = record + { isCommutativeRing = ⊕-∧-isCommutativeRing ; *-idem = ∧-idem } + + ⊕-∧-booleanRing : BooleanRing _ _ + ⊕-∧-booleanRing = record { isBooleanRing = ⊕-∧-isBooleanRing } infixl 6 _⊕_ From 6a675c01d55d73eb0b8d676dd756594c213772c7 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 17 Jul 2025 10:59:57 +0100 Subject: [PATCH 15/27] add: more re-exports --- src/Algebra/Bundles.agda | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index adeb87752b..bc66a893f4 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -939,6 +939,16 @@ record BooleanSemiring c ℓ : Set (suc (c ⊔ ℓ)) where semiring : Semiring _ _ semiring = record { isSemiring = isSemiring } + open Semiring semiring public + using ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma + ; +-semigroup; +-commutativeSemigroup + ; *-rawMagma; *-magma; *-semigroup + ; +-rawMonoid; +-monoid; +-commutativeMonoid + ; *-rawMonoid; *-monoid + ; rawNearSemiring ; rawSemiring; nearSemiring + ; semiringWithoutOne; semiringWithoutAnnihilatingZero + ) + *-idempotentMonoid : IdempotentMonoid c ℓ *-idempotentMonoid = record { isIdempotentMonoid = *-isIdempotentMonoid } From a7f4c45a13ad58a7ab2c50b4dfe36ad31654ae8b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 17 Jul 2025 11:00:47 +0100 Subject: [PATCH 16/27] add: more inherited properties --- src/Algebra/Properties/CommutativeMonoid.agda | 25 +++++++++++++------ 1 file changed, 18 insertions(+), 7 deletions(-) diff --git a/src/Algebra/Properties/CommutativeMonoid.agda b/src/Algebra/Properties/CommutativeMonoid.agda index 4bb8f372dd..840155cd69 100644 --- a/src/Algebra/Properties/CommutativeMonoid.agda +++ b/src/Algebra/Properties/CommutativeMonoid.agda @@ -9,13 +9,12 @@ open import Algebra.Bundles using (CommutativeMonoid) module Algebra.Properties.CommutativeMonoid - {g₁ g₂} (M : CommutativeMonoid g₁ g₂) + {c ℓ} (commutativeMonoid : CommutativeMonoid c ℓ) where -open import Algebra.Definitions using (LeftInvertible; RightInvertible; Invertible) open import Data.Product.Base using (_,_; proj₂) -open CommutativeMonoid M +open CommutativeMonoid commutativeMonoid renaming ( ε to 0# ; _∙_ to _+_ @@ -28,17 +27,29 @@ open CommutativeMonoid M ; comm to +-comm ) +open import Algebra.Definitions _≈_ + using (LeftInvertible; RightInvertible; Invertible) + private variable x : Carrier -invertibleˡ⇒invertibleʳ : LeftInvertible _≈_ 0# _+_ x → RightInvertible _≈_ 0# _+_ x + +------------------------------------------------------------------------ +-- Re-export properties of commutative semigroups + +open import Algebra.Properties.CommutativeSemigroup commutativeSemigroup public + +------------------------------------------------------------------------ +-- Additional properties + +invertibleˡ⇒invertibleʳ : LeftInvertible 0# _+_ x → RightInvertible 0# _+_ x invertibleˡ⇒invertibleʳ {x} (-x , -x+x≈1) = -x , trans (+-comm x -x) -x+x≈1 -invertibleʳ⇒invertibleˡ : RightInvertible _≈_ 0# _+_ x → LeftInvertible _≈_ 0# _+_ x +invertibleʳ⇒invertibleˡ : RightInvertible 0# _+_ x → LeftInvertible 0# _+_ x invertibleʳ⇒invertibleˡ {x} (-x , x+-x≈1) = -x , trans (+-comm -x x) x+-x≈1 -invertibleˡ⇒invertible : LeftInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x +invertibleˡ⇒invertible : LeftInvertible 0# _+_ x → Invertible 0# _+_ x invertibleˡ⇒invertible left@(-x , -x+x≈1) = -x , -x+x≈1 , invertibleˡ⇒invertibleʳ left .proj₂ -invertibleʳ⇒invertible : RightInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x +invertibleʳ⇒invertible : RightInvertible 0# _+_ x → Invertible 0# _+_ x invertibleʳ⇒invertible right@(-x , x+-x≈1) = -x , invertibleʳ⇒invertibleˡ right .proj₂ , x+-x≈1 From fa284070032722fb638f12cf05372f3e27018128 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 17 Jul 2025 11:13:55 +0100 Subject: [PATCH 17/27] add: more properties towards `IsBooleanAlgebra` --- src/Algebra/Properties/BooleanSemiring.agda | 88 ++++++++++++++++++++- 1 file changed, 84 insertions(+), 4 deletions(-) diff --git a/src/Algebra/Properties/BooleanSemiring.agda b/src/Algebra/Properties/BooleanSemiring.agda index d7ee1dcbd3..f7add9d1e4 100644 --- a/src/Algebra/Properties/BooleanSemiring.agda +++ b/src/Algebra/Properties/BooleanSemiring.agda @@ -14,12 +14,22 @@ open import Algebra.Bundles module Algebra.Properties.BooleanSemiring {c ℓ} (booleanSemiring : BooleanSemiring c ℓ) where +open import Algebra.Core using (Op₁; Op₂) +open import Algebra.Lattice.Bundles + using (BooleanAlgebra) open import Data.Product.Base using (_,_) open import Function.Base using (id; _∘_; _$_) open BooleanSemiring booleanSemiring open import Algebra.Consequences.Setoid setoid using (binomial-expansion) open import Algebra.Definitions _≈_ +open import Algebra.Lattice.Structures.Biased _≈_ + using (IsLattice₂; isLattice₂ + ; IsDistributiveLatticeʳʲᵐ; isDistributiveLatticeʳʲᵐ + ; IsBooleanAlgebraʳ; isBooleanAlgebraʳ + ) +open import Algebra.Lattice.Structures _≈_ + using (IsLattice; IsDistributiveLattice; IsBooleanAlgebra) open import Algebra.Structures _≈_ using (IsCommutativeMonoid; IsIdempotentCommutativeMonoid ; IsGroup; IsAbelianGroup @@ -28,10 +38,10 @@ open import Algebra.Structures _≈_ open import Relation.Binary.Reasoning.Setoid setoid ------------------------------------------------------------------------ --- Export properties of semirings -{- -open import Algebra.Properties.Semiring semiring public --} +-- Export properties of additive submonoid + +open import Algebra.Properties.CommutativeMonoid +-commutativeMonoid public + ------------------------------------------------------------------------ -- Extra properties of Boolean semirings @@ -125,3 +135,73 @@ open CommutativeRing commutativeRing public booleanRing : BooleanRing _ _ booleanRing = record { isBooleanRing = isBooleanRing } + +------------------------------------------------------------------------ +-- Boolean Semirings yield Boolean Algebras + +-- Definitions + +infix 8 ¬_ +¬_ : Op₁ Carrier +¬ x = 1# + x + +infixr 6 _∨_ +_∨_ : Op₂ Carrier +x ∨ y = x + y + x * y + +-- Properties + +∨-absorbs-* : _∨_ Absorbs _*_ +∨-absorbs-* = {!!} + +*-absorbs-∨ : _*_ Absorbs _∨_ +*-absorbs-∨ = {!!} + +absorptive : Absorptive _∨_ _*_ +absorptive = ∨-absorbs-* , *-absorbs-∨ + +∨-distribʳ-∧ : _∨_ DistributesOverʳ _*_ +∨-distribʳ-∧ = {!!} + +∧-complementʳ : RightInverse 0# ¬_ _*_ +∧-complementʳ x = begin + x * (¬ x) ≈⟨ distribˡ x 1# x ⟩ + x * 1# + x * x ≈⟨ +-cong (*-identityʳ x) (*-idem x) ⟩ + x + x ≈⟨ x+x≈0 x ⟩ + 0# ∎ + +∨-complementʳ : RightInverse 1# ¬_ _∨_ +∨-complementʳ x = begin + x ∨ ¬ x ≈⟨ +-cong (x∙yz≈y∙xz x 1# x) (∧-complementʳ x) ⟩ + 1# + (x + x) + 0# ≈⟨ +-identityʳ _ ⟩ + 1# + (x + x) ≈⟨ +-congˡ (x+x≈0 x) ⟩ + 1# + 0# ≈⟨ +-identityʳ _ ⟩ + 1# ∎ + +-- Structures + +isLattice : IsLattice _∨_ _*_ +isLattice = isLattice₂ $ record + { isJoinSemilattice = {!!} + ; isMeetSemilattice = {!!} + ; absorptive = absorptive + } + +isDistributiveLattice : IsDistributiveLattice _∨_ _*_ +isDistributiveLattice = isDistributiveLatticeʳʲᵐ $ record + { isLattice = isLattice + ; ∨-distribʳ-∧ = ∨-distribʳ-∧ + } + +isBooleanAlgebra : IsBooleanAlgebra _∨_ _*_ ¬_ 1# 0# +isBooleanAlgebra = isBooleanAlgebraʳ $ record + { isDistributiveLattice = isDistributiveLattice + ; ∨-complementʳ = ∨-complementʳ + ; ∧-complementʳ = ∧-complementʳ + ; ¬-cong = +-congˡ + } + +-- Bundle + +booleanAlgebra : BooleanAlgebra _ _ +booleanAlgebra = record { isBooleanAlgebra = isBooleanAlgebra } From 4c1fbc0b2684e6a1e2c59646d181bb557bc318f3 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 17 Jul 2025 13:57:13 +0100 Subject: [PATCH 18/27] add: yet more properties towards `IsBooleanAlgebra` --- src/Algebra/Properties/BooleanSemiring.agda | 96 +++++++++++++++------ 1 file changed, 70 insertions(+), 26 deletions(-) diff --git a/src/Algebra/Properties/BooleanSemiring.agda b/src/Algebra/Properties/BooleanSemiring.agda index f7add9d1e4..9e4886ca78 100644 --- a/src/Algebra/Properties/BooleanSemiring.agda +++ b/src/Algebra/Properties/BooleanSemiring.agda @@ -17,6 +17,7 @@ module Algebra.Properties.BooleanSemiring open import Algebra.Core using (Op₁; Op₂) open import Algebra.Lattice.Bundles using (BooleanAlgebra) +import Algebra.Properties.CommutativeMonoid as CommutativeMonoidProperties open import Data.Product.Base using (_,_) open import Function.Base using (id; _∘_; _$_) @@ -31,17 +32,13 @@ open import Algebra.Lattice.Structures.Biased _≈_ open import Algebra.Lattice.Structures _≈_ using (IsLattice; IsDistributiveLattice; IsBooleanAlgebra) open import Algebra.Structures _≈_ - using (IsCommutativeMonoid; IsIdempotentCommutativeMonoid + using (IsMagma; IsSemigroup; IsBand + ; IsCommutativeMonoid; IsIdempotentCommutativeMonoid ; IsGroup; IsAbelianGroup ; IsRing; IsCommutativeRing; IsBooleanRing ) open import Relation.Binary.Reasoning.Setoid setoid ------------------------------------------------------------------------- --- Export properties of additive submonoid - -open import Algebra.Properties.CommutativeMonoid +-commutativeMonoid public - ------------------------------------------------------------------------ -- Extra properties of Boolean semirings @@ -145,45 +142,92 @@ infix 8 ¬_ ¬_ : Op₁ Carrier ¬ x = 1# + x +¬-cong : Congruent₁ ¬_ +¬-cong = +-congˡ + +∧-complementʳ : RightInverse 0# ¬_ _*_ +∧-complementʳ x = begin + x * (¬ x) ≈⟨ distribˡ x 1# x ⟩ + x * 1# + x * x ≈⟨ +-cong (*-identityʳ x) (*-idem x) ⟩ + x + x ≈⟨ x+x≈0 x ⟩ + 0# ∎ + infixr 6 _∨_ _∨_ : Op₂ Carrier -x ∨ y = x + y + x * y +x ∨ y = x + y * ¬ x + +-- Basic properties + +∨-def : ∀ x y → x ∨ y ≈ x + y + x * y +∨-def x y = begin + x ∨ y ≈⟨ +-congˡ (distribˡ y 1# x) ⟩ + x + (y * 1# + y * x) ≈⟨ +-assoc x (y * 1#) (y * x) ⟨ + x + y * 1# + y * x ≈⟨ +-cong (+-congˡ (*-identityʳ y)) (*-comm y x) ⟩ + x + y + x * y ∎ + +∨-cong : Congruent₂ _∨_ +∨-cong x≈x′ y≈y′ = +-cong x≈x′ (*-cong y≈y′ (¬-cong x≈x′)) --- Properties +∨-comm : Commutative _∨_ +∨-comm x y = begin + x ∨ y ≈⟨ ∨-def x y ⟩ + x + y + x * y ≈⟨ +-cong (+-comm x y) (*-comm x y) ⟩ + y + x + y * x ≈⟨ ∨-def y x ⟨ + y ∨ x ∎ + +∨-idem : Idempotent _∨_ +∨-idem x = begin + x ∨ x ≈⟨ +-congˡ (∧-complementʳ x) ⟩ + x + 0# ≈⟨ +-identityʳ x ⟩ + x ∎ + +∨-assoc : Associative _∨_ +∨-assoc x y z = {!!} + +-- Lattice properties ∨-absorbs-* : _∨_ Absorbs _*_ -∨-absorbs-* = {!!} +∨-absorbs-* x y = begin + x ∨ x * y ≈⟨ +-congˡ (xy∙z≈xz∙y x y (¬ x)) ⟩ + x + (x * ¬ x) * y ≈⟨ +-congˡ (*-congʳ (∧-complementʳ x)) ⟩ + x + 0# * y ≈⟨ +-congˡ (zeroˡ y) ⟩ + x + 0# ≈⟨ +-identityʳ _ ⟩ + x ∎ + where open CommutativeMonoidProperties *-commutativeMonoid *-absorbs-∨ : _*_ Absorbs _∨_ -*-absorbs-∨ = {!!} +*-absorbs-∨ x y = {!!} absorptive : Absorptive _∨_ _*_ absorptive = ∨-absorbs-* , *-absorbs-∨ ∨-distribʳ-∧ : _∨_ DistributesOverʳ _*_ -∨-distribʳ-∧ = {!!} - -∧-complementʳ : RightInverse 0# ¬_ _*_ -∧-complementʳ x = begin - x * (¬ x) ≈⟨ distribˡ x 1# x ⟩ - x * 1# + x * x ≈⟨ +-cong (*-identityʳ x) (*-idem x) ⟩ - x + x ≈⟨ x+x≈0 x ⟩ - 0# ∎ +∨-distribʳ-∧ x y z = {!(y ∨ x) * (z ∨ x)!} ∨-complementʳ : RightInverse 1# ¬_ _∨_ ∨-complementʳ x = begin - x ∨ ¬ x ≈⟨ +-cong (x∙yz≈y∙xz x 1# x) (∧-complementʳ x) ⟩ - 1# + (x + x) + 0# ≈⟨ +-identityʳ _ ⟩ - 1# + (x + x) ≈⟨ +-congˡ (x+x≈0 x) ⟩ - 1# + 0# ≈⟨ +-identityʳ _ ⟩ - 1# ∎ + x ∨ ¬ x ≈⟨ +-congˡ (*-idem (¬ x)) ⟩ + x + ¬ x ≈⟨ x∙yz≈y∙xz x 1# x ⟩ + 1# + (x + x) ≈⟨ +-congˡ (x+x≈0 x) ⟩ + 1# + 0# ≈⟨ +-identityʳ _ ⟩ + 1# ∎ + where open CommutativeMonoidProperties +-commutativeMonoid -- Structures +∨-isMagma : IsMagma _∨_ +∨-isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∨-cong } + +∨-isSemigroup : IsSemigroup _∨_ +∨-isSemigroup = record { isMagma = ∨-isMagma ; assoc = ∨-assoc } + +∨-isBand : IsBand _∨_ +∨-isBand = record { isSemigroup = ∨-isSemigroup ; idem = ∨-idem } + isLattice : IsLattice _∨_ _*_ isLattice = isLattice₂ $ record - { isJoinSemilattice = {!!} - ; isMeetSemilattice = {!!} + { isJoinSemilattice = record { isBand = ∨-isBand ; comm = ∨-comm } + ; isMeetSemilattice = record { isBand = *-isBand ; comm = *-comm } ; absorptive = absorptive } @@ -198,7 +242,7 @@ isBooleanAlgebra = isBooleanAlgebraʳ $ record { isDistributiveLattice = isDistributiveLattice ; ∨-complementʳ = ∨-complementʳ ; ∧-complementʳ = ∧-complementʳ - ; ¬-cong = +-congˡ + ; ¬-cong = ¬-cong } -- Bundle From 763cac5b185dd84bd0ef4f8faeb88f0000c9826f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 17 Jul 2025 14:59:31 +0100 Subject: [PATCH 19/27] add: grinding towards `IsBooleanAlgebra` --- src/Algebra/Properties/BooleanSemiring.agda | 55 +++++++++++++++------ 1 file changed, 41 insertions(+), 14 deletions(-) diff --git a/src/Algebra/Properties/BooleanSemiring.agda b/src/Algebra/Properties/BooleanSemiring.agda index 9e4886ca78..faf7107ca1 100644 --- a/src/Algebra/Properties/BooleanSemiring.agda +++ b/src/Algebra/Properties/BooleanSemiring.agda @@ -18,6 +18,7 @@ open import Algebra.Core using (Op₁; Op₂) open import Algebra.Lattice.Bundles using (BooleanAlgebra) import Algebra.Properties.CommutativeMonoid as CommutativeMonoidProperties +import Algebra.Properties.IdempotentCommutativeMonoid as IdempotentCommutativeMonoidProperties open import Data.Product.Base using (_,_) open import Function.Base using (id; _∘_; _$_) @@ -152,12 +153,29 @@ infix 8 ¬_ x + x ≈⟨ x+x≈0 x ⟩ 0# ∎ +private + *-lemma : ∀ x y → x + (x * ¬ x) * y ≈ x + *-lemma x y = begin + x + (x * ¬ x) * y ≈⟨ +-congˡ (*-congʳ (∧-complementʳ x)) ⟩ + x + 0# * y ≈⟨ +-congˡ (zeroˡ y) ⟩ + x + 0# ≈⟨ +-identityʳ _ ⟩ + x ∎ + infixr 6 _∨_ _∨_ : Op₂ Carrier x ∨ y = x + y * ¬ x -- Basic properties +∨-complementʳ : RightInverse 1# ¬_ _∨_ +∨-complementʳ x = begin + x ∨ ¬ x ≈⟨ +-congˡ (*-idem (¬ x)) ⟩ + x + ¬ x ≈⟨ x∙yz≈y∙xz x 1# x ⟩ + 1# + (x + x) ≈⟨ +-congˡ (x+x≈0 x) ⟩ + 1# + 0# ≈⟨ +-identityʳ _ ⟩ + 1# ∎ + where open CommutativeMonoidProperties +-commutativeMonoid + ∨-def : ∀ x y → x ∨ y ≈ x + y + x * y ∨-def x y = begin x ∨ y ≈⟨ +-congˡ (distribˡ y 1# x) ⟩ @@ -189,29 +207,38 @@ x ∨ y = x + y * ¬ x ∨-absorbs-* : _∨_ Absorbs _*_ ∨-absorbs-* x y = begin x ∨ x * y ≈⟨ +-congˡ (xy∙z≈xz∙y x y (¬ x)) ⟩ - x + (x * ¬ x) * y ≈⟨ +-congˡ (*-congʳ (∧-complementʳ x)) ⟩ - x + 0# * y ≈⟨ +-congˡ (zeroˡ y) ⟩ - x + 0# ≈⟨ +-identityʳ _ ⟩ + x + (x * ¬ x) * y ≈⟨ *-lemma x y ⟩ x ∎ where open CommutativeMonoidProperties *-commutativeMonoid *-absorbs-∨ : _*_ Absorbs _∨_ -*-absorbs-∨ x y = {!!} +*-absorbs-∨ x y = begin + x * (x ∨ y) ≈⟨ distribˡ x x (y * ¬ x) ⟩ + x * x + x * (y * ¬ x) ≈⟨ +-cong (*-idem x) (x∙yz≈xz∙y x y (¬ x)) ⟩ + x + (x * ¬ x) * y ≈⟨ *-lemma x y ⟩ + x ∎ + where open CommutativeMonoidProperties *-commutativeMonoid absorptive : Absorptive _∨_ _*_ absorptive = ∨-absorbs-* , *-absorbs-∨ ∨-distribʳ-∧ : _∨_ DistributesOverʳ _*_ -∨-distribʳ-∧ x y z = {!(y ∨ x) * (z ∨ x)!} - -∨-complementʳ : RightInverse 1# ¬_ _∨_ -∨-complementʳ x = begin - x ∨ ¬ x ≈⟨ +-congˡ (*-idem (¬ x)) ⟩ - x + ¬ x ≈⟨ x∙yz≈y∙xz x 1# x ⟩ - 1# + (x + x) ≈⟨ +-congˡ (x+x≈0 x) ⟩ - 1# + 0# ≈⟨ +-identityʳ _ ⟩ - 1# ∎ - where open CommutativeMonoidProperties +-commutativeMonoid +∨-distribʳ-∧ x y z = begin + y * z ∨ x ≡⟨⟩ + y * z + x * (1# + y * z) ≈⟨ +-congˡ (distribˡ x 1# (y * z)) ⟩ + y * z + (x * 1# + x * (y * z)) ≈⟨ +-congˡ (+-congʳ (*-identityʳ x)) ⟩ + y * z + (x + x * (y * z)) ≈⟨ {!!} ⟩ + {!!} ≈⟨ {!!} ⟩ + {!!} ≈⟨ {!!} ⟩ + {!!} ≈⟨ {!!} ⟩ + {!!} ≈⟨ {!!} ⟩ + y * z + y * (x * ¬ z) + x * ¬ y * z + x * (¬ y * ¬ z) ≈⟨ +-congˡ (∙-distrˡ-∙ x (¬ y) (¬ z)) ⟩ + y * z + y * (x * ¬ z) + x * ¬ y * z + x * ¬ y * (x * ¬ z) ≈⟨ expand y (x * ¬ y) z (x * ¬ z) ⟨ + (y + x * ¬ y) * (z + x * ¬ z) ≡⟨⟩ + (y ∨ x) * (z ∨ x) ∎ + where + open IdempotentCommutativeMonoidProperties *-idempotentCommutativeMonoid + expand = binomial-expansion +-cong +-assoc distrib -- Structures From f10a36bb0336a47cf7ed73348399bcd2ec7fe8a7 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 18 Jul 2025 03:39:16 +0100 Subject: [PATCH 20/27] add: `deMorgan` laws --- src/Algebra/Properties/BooleanSemiring.agda | 55 +++++++++++++++++++-- 1 file changed, 50 insertions(+), 5 deletions(-) diff --git a/src/Algebra/Properties/BooleanSemiring.agda b/src/Algebra/Properties/BooleanSemiring.agda index faf7107ca1..cb73483564 100644 --- a/src/Algebra/Properties/BooleanSemiring.agda +++ b/src/Algebra/Properties/BooleanSemiring.agda @@ -146,6 +146,14 @@ infix 8 ¬_ ¬-cong : Congruent₁ ¬_ ¬-cong = +-congˡ +¬-involutive : Involutive ¬_ +¬-involutive x = begin + ¬ ¬ x ≡⟨⟩ + 1# + (1# + x) ≈⟨ +-assoc 1# 1# x ⟨ + 1# + 1# + x ≈⟨ +-congʳ (x+x≈0 1#) ⟩ + 0# + x ≈⟨ +-identityˡ x ⟩ + x ∎ + ∧-complementʳ : RightInverse 0# ¬_ _*_ ∧-complementʳ x = begin x * (¬ x) ≈⟨ distribˡ x 1# x ⟩ @@ -195,12 +203,46 @@ x ∨ y = x + y * ¬ x ∨-idem : Idempotent _∨_ ∨-idem x = begin - x ∨ x ≈⟨ +-congˡ (∧-complementʳ x) ⟩ - x + 0# ≈⟨ +-identityʳ x ⟩ - x ∎ + x ∨ x ≈⟨ +-congˡ (∧-complementʳ x) ⟩ + x + 0# ≈⟨ +-identityʳ x ⟩ + x ∎ + +deMorgan₁ : ∀ x y → ¬ (x * y) ≈ ¬ x ∨ ¬ y +deMorgan₁ x y = begin + ¬ (x * y) ≡⟨⟩ + 1# + x * y ≈⟨ +-cong (+-identityʳ 1#) (*-comm y x) ⟨ + 1# + 0# + y * x ≈⟨ +-congʳ (+-congˡ (x+x≈0 x)) ⟨ + 1# + (x + x) + y * x ≈⟨ +-congʳ (+-assoc 1# x x) ⟨ + 1# + x + x + y * x ≈⟨ +-congʳ (+-congˡ (*-identityˡ x)) ⟨ + 1# + x + 1# * x + y * x ≈⟨ +-assoc (1# + x) (1# * x) (y * x) ⟩ + 1# + x + (1# * x + y * x) ≈⟨ +-congˡ (distribʳ x 1# y) ⟨ + 1# + x + ¬ y * x ≈⟨ +-congˡ (*-congˡ (¬-involutive x)) ⟨ + ¬ x + ¬ y * ¬ ¬ x ≡⟨⟩ + ¬ x ∨ ¬ y ∎ + +deMorgan₂ : ∀ x y → ¬ (x ∨ y) ≈ ¬ x * ¬ y +deMorgan₂ x y = begin + ¬ (x ∨ y) ≈⟨ +-congˡ (∨-def x y) ⟩ + 1# + (x + y + x * y) ≈⟨ +-assoc _ _ _ ⟨ + 1# + (x + y) + x * y ≈⟨ +-congʳ (x∙yz≈xz∙y 1# x y) ⟩ + 1# + y + x + x * y ≈⟨ +-congʳ (+-cong (+-cong (*-idem _) (*-identityˡ y)) (*-identityʳ x)) ⟨ + 1# * 1# + 1# * y + x * 1# + x * y ≈⟨ expand 1# x 1# y ⟨ + (1# + x) * (1# + y) ≡⟨⟩ + ¬ x * ¬ y ∎ + where -- +-congˡ (+-congʳ (+-comm x y)) + open CommutativeMonoidProperties +-commutativeMonoid + expand = binomial-expansion +-cong +-assoc distrib ∨-assoc : Associative _∨_ -∨-assoc x y z = {!!} +∨-assoc x y z = begin + (x ∨ y) ∨ z ≈⟨ ¬-involutive ((x ∨ y) ∨ z) ⟨ + ¬ ¬ ((x ∨ y) ∨ z) ≈⟨ ¬-cong (deMorgan₂ (x ∨ y) z) ⟩ + ¬ (¬ (x ∨ y) * ¬ z) ≈⟨ ¬-cong (*-congʳ (deMorgan₂ x y)) ⟩ + ¬ ((¬ x * ¬ y) * ¬ z) ≈⟨ ¬-cong (*-assoc (¬ x) (¬ y) (¬ z)) ⟩ + ¬ (¬ x * (¬ y * ¬ z)) ≈⟨ ¬-cong (*-congˡ (deMorgan₂ y z)) ⟨ + ¬ (¬ x * ¬ (y ∨ z)) ≈⟨ ¬-cong (deMorgan₂ x (y ∨ z)) ⟨ + ¬ ¬ (x ∨ y ∨ z) ≈⟨ ¬-involutive (x ∨ y ∨ z) ⟩ + x ∨ y ∨ z ∎ -- Lattice properties @@ -225,6 +267,8 @@ absorptive = ∨-absorbs-* , *-absorbs-∨ ∨-distribʳ-∧ : _∨_ DistributesOverʳ _*_ ∨-distribʳ-∧ x y z = begin y * z ∨ x ≡⟨⟩ + y * z + x * (1# + y * z) ≈⟨ {!!} ⟩ +{- y * z + x * (1# + y * z) ≈⟨ +-congˡ (distribˡ x 1# (y * z)) ⟩ y * z + (x * 1# + x * (y * z)) ≈⟨ +-congˡ (+-congʳ (*-identityʳ x)) ⟩ y * z + (x + x * (y * z)) ≈⟨ {!!} ⟩ @@ -234,7 +278,8 @@ absorptive = ∨-absorbs-* , *-absorbs-∨ {!!} ≈⟨ {!!} ⟩ y * z + y * (x * ¬ z) + x * ¬ y * z + x * (¬ y * ¬ z) ≈⟨ +-congˡ (∙-distrˡ-∙ x (¬ y) (¬ z)) ⟩ y * z + y * (x * ¬ z) + x * ¬ y * z + x * ¬ y * (x * ¬ z) ≈⟨ expand y (x * ¬ y) z (x * ¬ z) ⟨ - (y + x * ¬ y) * (z + x * ¬ z) ≡⟨⟩ +-} + (y + x * (1# + y)) * (z + x * (1# + z)) ≡⟨⟩ (y ∨ x) * (z ∨ x) ∎ where open IdempotentCommutativeMonoidProperties *-idempotentCommutativeMonoid From e082ea79c03cd6ab4daf7eb58d359786a81684ca Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 18 Jul 2025 08:16:47 +0100 Subject: [PATCH 21/27] add: `Semiring` properties as home for `binomial-expansion` --- CHANGELOG.md | 2 ++ src/Algebra/Properties/BooleanSemiring.agda | 20 ++++++++--------- src/Algebra/Properties/Semiring.agda | 25 +++++++++++++++++++++ 3 files changed, 37 insertions(+), 10 deletions(-) create mode 100644 src/Algebra/Properties/Semiring.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 3ae2fa358a..eb90ddb777 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -169,6 +169,8 @@ New modules * `Algebra.Properties.CommutativeRing`. +* `Algebra.Properties.Semiring`. + * `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`. * `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`. diff --git a/src/Algebra/Properties/BooleanSemiring.agda b/src/Algebra/Properties/BooleanSemiring.agda index cb73483564..22e06b4a5c 100644 --- a/src/Algebra/Properties/BooleanSemiring.agda +++ b/src/Algebra/Properties/BooleanSemiring.agda @@ -23,7 +23,6 @@ open import Data.Product.Base using (_,_) open import Function.Base using (id; _∘_; _$_) open BooleanSemiring booleanSemiring -open import Algebra.Consequences.Setoid setoid using (binomial-expansion) open import Algebra.Definitions _≈_ open import Algebra.Lattice.Structures.Biased _≈_ using (IsLattice₂; isLattice₂ @@ -40,19 +39,24 @@ open import Algebra.Structures _≈_ ) open import Relation.Binary.Reasoning.Setoid setoid + +------------------------------------------------------------------------ +-- Re-export Semiring properties + +open import Algebra.Properties.Semiring semiring public + ------------------------------------------------------------------------ -- Extra properties of Boolean semirings xy+yx≈0 : ∀ x y → x * y + y * x ≈ 0# xy+yx≈0 x y = +-cancelˡ (x * x) _ _ $ +-cancelʳ (y * y) _ _ $ begin x * x + ((x * y) + (y * x)) + y * y ≈⟨ +-congʳ (+-assoc _ _ _) ⟨ - x * x + x * y + y * x + y * y ≈⟨ expand x y x y ⟨ + x * x + x * y + y * x + y * y ≈⟨ binomial-expansion x y x y ⟨ (x + y) * (x + y) ≈⟨ *-idem (x + y) ⟩ x + y ≈⟨ +-congˡ (*-idem y) ⟨ x + y * y ≈⟨ +-congʳ (*-idem x) ⟨ x * x + y * y ≈⟨ +-congʳ (+-identityʳ (x * x)) ⟨ x * x + 0# + y * y ∎ - where expand = binomial-expansion +-cong +-assoc distrib y≈x⇒x+y≈0 : ∀ {x y} → y ≈ x → x + y ≈ 0# y≈x⇒x+y≈0 {x = x} {y = y} y≈x = begin @@ -226,12 +230,10 @@ deMorgan₂ x y = begin 1# + (x + y + x * y) ≈⟨ +-assoc _ _ _ ⟨ 1# + (x + y) + x * y ≈⟨ +-congʳ (x∙yz≈xz∙y 1# x y) ⟩ 1# + y + x + x * y ≈⟨ +-congʳ (+-cong (+-cong (*-idem _) (*-identityˡ y)) (*-identityʳ x)) ⟨ - 1# * 1# + 1# * y + x * 1# + x * y ≈⟨ expand 1# x 1# y ⟨ + 1# * 1# + 1# * y + x * 1# + x * y ≈⟨ binomial-expansion 1# x 1# y ⟨ (1# + x) * (1# + y) ≡⟨⟩ ¬ x * ¬ y ∎ - where -- +-congˡ (+-congʳ (+-comm x y)) - open CommutativeMonoidProperties +-commutativeMonoid - expand = binomial-expansion +-cong +-assoc distrib + where open CommutativeMonoidProperties +-commutativeMonoid ∨-assoc : Associative _∨_ ∨-assoc x y z = begin @@ -281,9 +283,7 @@ absorptive = ∨-absorbs-* , *-absorbs-∨ -} (y + x * (1# + y)) * (z + x * (1# + z)) ≡⟨⟩ (y ∨ x) * (z ∨ x) ∎ - where - open IdempotentCommutativeMonoidProperties *-idempotentCommutativeMonoid - expand = binomial-expansion +-cong +-assoc distrib + where open IdempotentCommutativeMonoidProperties *-idempotentCommutativeMonoid -- Structures diff --git a/src/Algebra/Properties/Semiring.agda b/src/Algebra/Properties/Semiring.agda new file mode 100644 index 0000000000..1db1076689 --- /dev/null +++ b/src/Algebra/Properties/Semiring.agda @@ -0,0 +1,25 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Some basic properties of Semirings +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles + using (Semiring) + +module Algebra.Properties.Semiring + {c ℓ} (semiring : Semiring c ℓ) where + +open Semiring semiring +import Algebra.Consequences.Setoid setoid as Consequences +open import Relation.Binary.Reasoning.Setoid setoid + +------------------------------------------------------------------------ +-- Re-export binomial expansion + +binomial-expansion : ∀ w x y z → + (w + x) * (y + z) ≈ w * y + w * z + x * y + x * z +binomial-expansion = Consequences.binomial-expansion +-cong +-assoc distrib + From 2d59a88181d35a006f446e1e1b283771b4443623 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 18 Jul 2025 09:37:02 +0100 Subject: [PATCH 22/27] more fiddling --- src/Algebra/Properties/BooleanSemiring.agda | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/Algebra/Properties/BooleanSemiring.agda b/src/Algebra/Properties/BooleanSemiring.agda index 22e06b4a5c..d43c75f13c 100644 --- a/src/Algebra/Properties/BooleanSemiring.agda +++ b/src/Algebra/Properties/BooleanSemiring.agda @@ -23,6 +23,7 @@ open import Data.Product.Base using (_,_) open import Function.Base using (id; _∘_; _$_) open BooleanSemiring booleanSemiring +import Algebra.Consequences.Setoid setoid as Consequences open import Algebra.Definitions _≈_ open import Algebra.Lattice.Structures.Biased _≈_ using (IsLattice₂; isLattice₂ @@ -267,9 +268,16 @@ absorptive : Absorptive _∨_ _*_ absorptive = ∨-absorbs-* , *-absorbs-∨ ∨-distribʳ-∧ : _∨_ DistributesOverʳ _*_ -∨-distribʳ-∧ x y z = begin +∨-distribʳ-∧ = {!!} +{- begin y * z ∨ x ≡⟨⟩ y * z + x * (1# + y * z) ≈⟨ {!!} ⟩ + (y + x * (1# + y)) * (z + x * (1# + z)) ≡⟨⟩ + (y ∨ x) * (z ∨ x) ∎ +-} +{- comm∧distrˡ⇒distrʳ *-cong ∨-comm (distrib∧absorbs⇒distribˡ {_∙_ = _+_} {!*-cong!} {!!} {!*-comm!} ∨-absorbs-* *-absorbs-∨ {!!}) + where open Consequences +-} {- y * z + x * (1# + y * z) ≈⟨ +-congˡ (distribˡ x 1# (y * z)) ⟩ y * z + (x * 1# + x * (y * z)) ≈⟨ +-congˡ (+-congʳ (*-identityʳ x)) ⟩ @@ -281,9 +289,6 @@ absorptive = ∨-absorbs-* , *-absorbs-∨ y * z + y * (x * ¬ z) + x * ¬ y * z + x * (¬ y * ¬ z) ≈⟨ +-congˡ (∙-distrˡ-∙ x (¬ y) (¬ z)) ⟩ y * z + y * (x * ¬ z) + x * ¬ y * z + x * ¬ y * (x * ¬ z) ≈⟨ expand y (x * ¬ y) z (x * ¬ z) ⟨ -} - (y + x * (1# + y)) * (z + x * (1# + z)) ≡⟨⟩ - (y ∨ x) * (z ∨ x) ∎ - where open IdempotentCommutativeMonoidProperties *-idempotentCommutativeMonoid -- Structures From bfc54b2167e5bc611195c4fbe5fa9980ff38f2a8 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 18 Jul 2025 09:57:30 +0100 Subject: [PATCH 23/27] back to square one --- src/Algebra/Properties/BooleanSemiring.agda | 23 +++------------------ 1 file changed, 3 insertions(+), 20 deletions(-) diff --git a/src/Algebra/Properties/BooleanSemiring.agda b/src/Algebra/Properties/BooleanSemiring.agda index d43c75f13c..959c691c17 100644 --- a/src/Algebra/Properties/BooleanSemiring.agda +++ b/src/Algebra/Properties/BooleanSemiring.agda @@ -268,27 +268,10 @@ absorptive : Absorptive _∨_ _*_ absorptive = ∨-absorbs-* , *-absorbs-∨ ∨-distribʳ-∧ : _∨_ DistributesOverʳ _*_ -∨-distribʳ-∧ = {!!} -{- begin - y * z ∨ x ≡⟨⟩ - y * z + x * (1# + y * z) ≈⟨ {!!} ⟩ - (y + x * (1# + y)) * (z + x * (1# + z)) ≡⟨⟩ - (y ∨ x) * (z ∨ x) ∎ --} -{- comm∧distrˡ⇒distrʳ *-cong ∨-comm (distrib∧absorbs⇒distribˡ {_∙_ = _+_} {!*-cong!} {!!} {!*-comm!} ∨-absorbs-* *-absorbs-∨ {!!}) - where open Consequences --} -{- - y * z + x * (1# + y * z) ≈⟨ +-congˡ (distribˡ x 1# (y * z)) ⟩ - y * z + (x * 1# + x * (y * z)) ≈⟨ +-congˡ (+-congʳ (*-identityʳ x)) ⟩ - y * z + (x + x * (y * z)) ≈⟨ {!!} ⟩ +∨-distribʳ-∧ x y z = begin + y * z ∨ x ≈⟨ {!!} ⟩ {!!} ≈⟨ {!!} ⟩ - {!!} ≈⟨ {!!} ⟩ - {!!} ≈⟨ {!!} ⟩ - {!!} ≈⟨ {!!} ⟩ - y * z + y * (x * ¬ z) + x * ¬ y * z + x * (¬ y * ¬ z) ≈⟨ +-congˡ (∙-distrˡ-∙ x (¬ y) (¬ z)) ⟩ - y * z + y * (x * ¬ z) + x * ¬ y * z + x * ¬ y * (x * ¬ z) ≈⟨ expand y (x * ¬ y) z (x * ¬ z) ⟨ --} + (y ∨ x) * (z ∨ x) ∎ -- Structures From 94d1b1971191a3261d8790dab9686f1087cb7584 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 18 Jul 2025 12:39:56 +0100 Subject: [PATCH 24/27] fix: finally! --- src/Algebra/Properties/BooleanSemiring.agda | 44 ++++++++++++--------- 1 file changed, 26 insertions(+), 18 deletions(-) diff --git a/src/Algebra/Properties/BooleanSemiring.agda b/src/Algebra/Properties/BooleanSemiring.agda index 959c691c17..b36898ccbb 100644 --- a/src/Algebra/Properties/BooleanSemiring.agda +++ b/src/Algebra/Properties/BooleanSemiring.agda @@ -16,9 +16,10 @@ module Algebra.Properties.BooleanSemiring open import Algebra.Core using (Op₁; Op₂) open import Algebra.Lattice.Bundles - using (BooleanAlgebra) + using (DistributiveLattice; BooleanAlgebra) import Algebra.Properties.CommutativeMonoid as CommutativeMonoidProperties import Algebra.Properties.IdempotentCommutativeMonoid as IdempotentCommutativeMonoidProperties +import Algebra.Lattice.Properties.DistributiveLattice as DistributiveLatticeProperties open import Data.Product.Base using (_,_) open import Function.Base using (id; _∘_; _$_) @@ -264,14 +265,14 @@ deMorgan₂ x y = begin x ∎ where open CommutativeMonoidProperties *-commutativeMonoid -absorptive : Absorptive _∨_ _*_ -absorptive = ∨-absorbs-* , *-absorbs-∨ - -∨-distribʳ-∧ : _∨_ DistributesOverʳ _*_ -∨-distribʳ-∧ x y z = begin - y * z ∨ x ≈⟨ {!!} ⟩ - {!!} ≈⟨ {!!} ⟩ - (y ∨ x) * (z ∨ x) ∎ +*-distribʳ-∨ : _*_ DistributesOverʳ _∨_ +*-distribʳ-∨ x y z = begin + (y ∨ z) * x ≈⟨ *-congʳ (∨-def y z) ⟩ + (y + z + y * z) * x ≈⟨ distribʳ x (y + z) (y * z) ⟩ + ((y + z) * x + y * z * x) ≈⟨ +-cong (distribʳ x y z) (∙-distrʳ-∙ x y z) ⟩ + (y * x + z * x) + (y * x) * (z * x) ≈⟨ ∨-def (y * x) (z * x) ⟨ + (y * x) ∨ (z * x) ∎ + where open IdempotentCommutativeMonoidProperties *-idempotentCommutativeMonoid -- Structures @@ -284,19 +285,26 @@ absorptive = ∨-absorbs-* , *-absorbs-∨ ∨-isBand : IsBand _∨_ ∨-isBand = record { isSemigroup = ∨-isSemigroup ; idem = ∨-idem } -isLattice : IsLattice _∨_ _*_ -isLattice = isLattice₂ $ record - { isJoinSemilattice = record { isBand = ∨-isBand ; comm = ∨-comm } - ; isMeetSemilattice = record { isBand = *-isBand ; comm = *-comm } - ; absorptive = absorptive +*-∨-isLattice : IsLattice _*_ _∨_ +*-∨-isLattice = isLattice₂ $ record + { isJoinSemilattice = record { isBand = *-isBand ; comm = *-comm } + ; isMeetSemilattice = record { isBand = ∨-isBand ; comm = ∨-comm } + ; absorptive = *-absorbs-∨ , ∨-absorbs-* } -isDistributiveLattice : IsDistributiveLattice _∨_ _*_ -isDistributiveLattice = isDistributiveLatticeʳʲᵐ $ record - { isLattice = isLattice - ; ∨-distribʳ-∧ = ∨-distribʳ-∧ +*-∨-isDistributiveLattice : IsDistributiveLattice _*_ _∨_ +*-∨-isDistributiveLattice = isDistributiveLatticeʳʲᵐ $ record + { isLattice = *-∨-isLattice + ; ∨-distribʳ-∧ = *-distribʳ-∨ } +*-∨-distributiveLattice : DistributiveLattice _ _ +*-∨-distributiveLattice = record { isDistributiveLattice = *-∨-isDistributiveLattice } + +isDistributiveLattice : IsDistributiveLattice _∨_ _*_ +isDistributiveLattice = + DistributiveLatticeProperties.∧-∨-isDistributiveLattice *-∨-distributiveLattice + isBooleanAlgebra : IsBooleanAlgebra _∨_ _*_ ¬_ 1# 0# isBooleanAlgebra = isBooleanAlgebraʳ $ record { isDistributiveLattice = isDistributiveLattice From a9a28a960e1501905afbf92d70fff81ff79a8787 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 18 Jul 2025 18:04:06 +0100 Subject: [PATCH 25/27] fix: remove shadowing of `isBooleanRing` and `booleanRing` --- src/Algebra/Properties/BooleanRing.agda | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Algebra/Properties/BooleanRing.agda b/src/Algebra/Properties/BooleanRing.agda index 48262f26fc..c0c28b979b 100644 --- a/src/Algebra/Properties/BooleanRing.agda +++ b/src/Algebra/Properties/BooleanRing.agda @@ -51,6 +51,7 @@ open BooleanSemiring booleanSemiring public -- Export properties of Boolean semirings open import Algebra.Properties.BooleanSemiring booleanSemiring public + hiding (isBooleanRing; booleanRing) ------------------------------------------------------------------------ -- Further consequences From 05f07f936084d14fad8d5e7cad85e2c75b08a6f8 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 20 Jul 2025 20:22:34 +0100 Subject: [PATCH 26/27] reset: `CHANGELOG` for v2.4 --- CHANGELOG.md | 556 +-------------------------------------------------- 1 file changed, 11 insertions(+), 545 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a9e75f24b1..f82190da4e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,154 +1,29 @@ -Version 2.3-rc1 +Version 2.4-dev =============== -The library has been tested using Agda 2.7.0 and 2.8.0. +The library has been tested using Agda 2.8.0. + +Highlights +---------- Bug-fixes --------- -* In `Algebra.Apartness.Structures`, renamed `sym` from `IsApartnessRelation` - to `#-sym` in order to avoid overloaded projection. - `irrefl` and `cotrans` are similarly renamed for the sake of consistency. - -* In `Algebra.Definitions.RawMagma` and `Relation.Binary.Construct.Interior.Symmetric`, - the record constructors `_,_` incorrectly had no declared fixity. They have been given - the fixity `infixr 4 _,_`, consistent with that of `Data.Product.Base`. +Non-backwards compatible changes +-------------------------------- -* In `Data.Product.Function.Dependent.Setoid`, `left-inverse` defined a - `RightInverse`. - This has been deprecated in favor or `rightInverse`, and a corrected (and - correctly-named) function `leftInverse` has been added. +Minor improvements +------------------ -* The implementation of `_IsRelatedTo_` in `Relation.Binary.Reasoning.Base.Partial` - has been modified to correctly support equational reasoning at the beginning and the end. - The detail of this issue is described in [#2677](https://github.com/agda/agda-stdlib/pull/2677). Since the names of constructors - of `_IsRelatedTo_` are changed and the reduction behaviour of reasoning steps - are changed, this modification is non-backwards compatible. - -* The implementation of `≤-total` in `Data.Nat.Properties` used to use recursion - making it infeasibly slow for even relatively small natural numbers. It's definition - has been altered to use operations backed by primitives making it - significantly faster. However, its reduction behaviour on open terms may have - changed in some limited circumstances. +Deprecated modules +------------------ Deprecated names ---------------- -* In `Algebra.Definitions.RawMagma`: - ```agda - _∣∣_ ↦ _∥_ - _∤∤_ ↦ _∦_ - ``` - -* In `Algebra.Lattice.Properties.BooleanAlgebra` - ```agda - ⊥≉⊤ ↦ ¬⊥≈⊤ - ⊤≉⊥ ↦ ¬⊤≈⊥ - ``` - -* In `Algebra.Module.Consequences` - ```agda - *ₗ-assoc+comm⇒*ᵣ-assoc ↦ *ₗ-assoc∧comm⇒*ᵣ-assoc - *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc ↦ *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc - *ᵣ-assoc+comm⇒*ₗ-assoc ↦ *ᵣ-assoc∧comm⇒*ₗ-assoc - *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc ↦ *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc - ``` - -* In `Algebra.Modules.Structures.IsLeftModule`: - ```agda - uniqueˡ‿⁻ᴹ ↦ Algebra.Module.Properties.LeftModule.inverseˡ-uniqueᴹ - uniqueʳ‿⁻ᴹ ↦ Algebra.Module.Properties.LeftModule.inverseʳ-uniqueᴹ - ``` - -* In `Algebra.Modules.Structures.IsRightModule`: - ```agda - uniqueˡ‿⁻ᴹ ↦ Algebra.Module.Properties.RightModule.inverseˡ-uniqueᴹ - uniqueʳ‿⁻ᴹ ↦ Algebra.Module.Properties.RightModule.inverseʳ-uniqueᴹ - ``` - -* In `Algebra.Properties.Magma.Divisibility`: - ```agda - ∣∣-sym ↦ ∥-sym - ∣∣-respˡ-≈ ↦ ∥-respˡ-≈ - ∣∣-respʳ-≈ ↦ ∥-respʳ-≈ - ∣∣-resp-≈ ↦ ∥-resp-≈ - ∤∤-sym -≈ ↦ ∦-sym - ∤∤-respˡ-≈ ↦ ∦-respˡ-≈ - ∤∤-respʳ-≈ ↦ ∦-respʳ-≈ - ∤∤-resp-≈ ↦ ∦-resp-≈ - ∣-respʳ-≈ ↦ ∣ʳ-respʳ-≈ - ∣-respˡ-≈ ↦ ∣ʳ-respˡ-≈ - ∣-resp-≈ ↦ ∣ʳ-resp-≈ - x∣yx ↦ x∣ʳyx - xy≈z⇒y∣z ↦ xy≈z⇒y∣ʳz - ``` - -* In `Algebra.Properties.Monoid.Divisibility`: - ```agda - ∣∣-refl ↦ ∥-refl - ∣∣-reflexive ↦ ∥-reflexive - ∣∣-isEquivalence ↦ ∥-isEquivalence - ε∣_ ↦ ε∣ʳ_ - ∣-refl ↦ ∣ʳ-refl - ∣-reflexive ↦ ∣ʳ-reflexive - ∣-isPreorder ↦ ∣ʳ-isPreorder - ∣-preorder ↦ ∣ʳ-preorder - ``` - -* In `Algebra.Properties.Semigroup.Divisibility`: - ```agda - ∣∣-trans ↦ ∥-trans - ∣-trans ↦ ∣ʳ-trans - ``` - -* In `Algebra.Structures.Group`: - ```agda - uniqueˡ-⁻¹ ↦ Algebra.Properties.Group.inverseˡ-unique - uniqueʳ-⁻¹ ↦ Algebra.Properties.Group.inverseʳ-unique - ``` - -* In `Data.List.Base`: - ```agda - and ↦ Data.Bool.ListAction.and - or ↦ Data.Bool.ListAction.or - any ↦ Data.Bool.ListAction.any - all ↦ Data.Bool.ListAction.all - sum ↦ Data.Nat.ListAction.sum - product ↦ Data.Nat.ListAction.product - ``` - -* In `Data.List.Properties`: - ```agda - sum-++ ↦ Data.Nat.ListAction.Properties.sum-++ - ∈⇒∣product ↦ Data.Nat.ListAction.Properties.∈⇒∣product - product≢0 ↦ Data.Nat.ListAction.Properties.product≢0 - ∈⇒≤product ↦ Data.Nat.ListAction.Properties.∈⇒≤product - ∷-ʳ++-eqFree ↦ Data.List.Properties.ʳ++-ʳ++-eqFree - ``` - -* In `Data.List.Relation.Binary.Permutation.Propositional.Properties`: - ```agda - sum-↭ ↦ Data.Nat.ListAction.Properties.sum-↭ - product-↭ ↦ Data.Nat.ListAction.Properties.product-↭ - ``` - -* In `Data.Product.Function.Dependent.Setoid`: - ```agda - left-inverse ↦ rightInverse - ``` - -* In `Data.Product.Nary.NonDependent`: - ```agda - Allₙ ↦ Pointwiseₙ - ``` - New modules ----------- -* `Algebra.Module.Properties.{Bimodule|LeftModule|RightModule}`. - -* `Algebra.Morphism.Construct.DirectProduct`. - * `Algebra.Properties.BooleanRing`. * `Algebra.Properties.BooleanSemiring`. @@ -157,29 +32,6 @@ New modules * `Algebra.Properties.Semiring`. -* `Data.Bool.ListAction` - a new location for the lifted specialised list operations `Data.List.Base.{and|or|any|all}`. - -* `Data.Nat.ListAction(.Properties)` - a new location for the definitions and properties of `Data.List.Base.{sum|product}`. - -* `Data.List.Relation.Binary.Prefix.Propositional.Properties`. - -* `Data.List.Relation.Binary.Suffix.Propositional.Properties`. - -* `Data.List.Sort.InsertionSort(.{Base|Properties})` - defines insertion sort and proves properties of insertion sort. - -* `Data.List.Sort.MergeSort(.{Base|Properties})` - a refactor of the previous `Data.List.Sort.MergeSort`. - -* `Data.Sign.Show` - code for converting a sign to a string. - -* `Relation.Binary.Morphism.Construct.Product` - plumbing in the (categorical) product structure on `RawSetoid`. - -* `Relation.Binary.Properties.PartialSetoid` - systematise properties of the partial equivalence relation bundled with a set. - -* `Relation.Nullary.Recomputable.Core` - -* `Relation.Nullary.Irrelevant` - moved the concept `Irrelevant` of irrelevance (h-proposition) - from `Relation.Nullary` to its own dedicated module . - Additions to existing modules ----------------------------- @@ -189,14 +41,6 @@ Additions to existing modules record BooleanRing _ _ : Set _ ``` -* In `Algebra.Consequences.Base`: - ```agda - module Congruence (_≈_ : Rel A ℓ) (cong : Congruent₂ _≈_ _∙_) (refl : Reflexive _≈_) - where - ∙-congˡ : LeftCongruent _≈_ _∙_ - ∙-congʳ : RightCongruent _≈_ _∙_ - ``` - * In `Algebra.Consequences.Propositional`: ```agda binomial-expansion : Associative _∙_ → _◦_ DistributesOver _∙_ → @@ -205,397 +49,19 @@ Additions to existing modules * In `Algebra.Consequences.Setoid`: ```agda - module Congruence (cong : Congruent₂ _≈_ _∙_) where - ∙-congˡ : LeftCongruent _≈_ _∙_ - ∙-congʳ : RightCongruent _≈_ _∙_ binomial-expansion : Congruent₂ _∙_ → Associative _∙_ → _◦_ DistributesOver _∙_ → ∀ w x y z → ((w ∙ x) ◦ (y ∙ z)) ≈ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z)) ``` -* In `Algebra.Construct.Initial`: - ```agda - assoc : Associative _≈_ _∙_ - idem : Idempotent _≈_ _∙_ - ``` - -* In `Algebra.Construct.Pointwise`: - ```agda - isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0# → - IsNearSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) - isSemiringWithoutOne : IsSemiringWithoutOne _≈_ _+_ _*_ 0# → - IsSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) - isCommutativeSemiringWithoutOne : IsCommutativeSemiringWithoutOne _≈_ _+_ _*_ 0# → - IsCommutativeSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) - isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1# → - IsCommutativeSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#) - isIdempotentSemiring : IsIdempotentSemiring _≈_ _+_ _*_ 0# 1# → - IsIdempotentSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#) - isKleeneAlgebra : IsKleeneAlgebra _≈_ _+_ _*_ _⋆ 0# 1# → - IsKleeneAlgebra (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ _⋆) (lift₀ 0#) (lift₀ 1#) - isQuasiring : IsQuasiring _≈_ _+_ _*_ 0# 1# → - IsQuasiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#) - isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1# → - IsCommutativeRing (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ -_) (lift₀ 0#) (lift₀ 1#) - commutativeMonoid : CommutativeMonoid c ℓ → CommutativeMonoid (a ⊔ c) (a ⊔ ℓ) - nearSemiring : NearSemiring c ℓ → NearSemiring (a ⊔ c) (a ⊔ ℓ) - semiringWithoutOne : SemiringWithoutOne c ℓ → SemiringWithoutOne (a ⊔ c) (a ⊔ ℓ) - commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne c ℓ → CommutativeSemiringWithoutOne (a ⊔ c) (a ⊔ ℓ) - commutativeSemiring : CommutativeSemiring c ℓ → CommutativeSemiring (a ⊔ c) (a ⊔ ℓ) - idempotentSemiring : IdempotentSemiring c ℓ → IdempotentSemiring (a ⊔ c) (a ⊔ ℓ) - kleeneAlgebra : KleeneAlgebra c ℓ → KleeneAlgebra (a ⊔ c) (a ⊔ ℓ) - quasiring : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ) - commutativeRing : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ) - ``` - * In `Algebra.Lattice.Properties.BooleanAlgebra.XorRing`: ```agda ⊕-∧-isBooleanRing : IsBooleanRing _⊕_ _∧_ id ⊥ ⊤ ⊕-∧-booleanRing : BooleanRing _ _ ``` -* In `Algebra.Modules.Properties`: - ```agda - inverseˡ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → x ≈ -ᴹ y - inverseʳ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → y ≈ -ᴹ x - ``` - -* In `Algebra.Properties.Magma.Divisibility`: - ```agda - ∣ˡ-respʳ-≈ : _∣ˡ_ Respectsʳ _≈_ - ∣ˡ-respˡ-≈ : _∣ˡ_ Respectsˡ _≈_ - ∣ˡ-resp-≈ : _∣ˡ_ Respects₂ _≈_ - x∣ˡxy : x ∣ˡ x ∙ y - xy≈z⇒x∣ˡz : x ∙ y ≈ z → x ∣ˡ z - ``` - -* In `Algebra.Properties.Monoid.Divisibility`: - ```agda - ε∣ˡ_ : ε ∣ˡ x - ∣ˡ-refl : Reflexive _∣ˡ_ - ∣ˡ-reflexive : _≈_ ⇒ _∣ˡ_ - ∣ˡ-isPreorder : IsPreorder _≈_ _∣ˡ_ - ∣ˡ-preorder : Preorder a ℓ _ - ``` - -* In `Algebra.Properties.Monoid`: - ```agda - ε-unique : (∀ b → b ∙ a ≈ b) → a ≈ ε - ε-comm : a ∙ ε ≈ ε ∙ a - elimʳ : a ≈ ε → b ∙ a ≈ b - elimˡ : a ≈ ε → a ∙ b ≈ b - introʳ : a ≈ ε → b ≈ b ∙ a - introˡ : a ≈ ε → b ≈ a ∙ b - introᶜ : a ≈ ε → b ∙ c ≈ b ∙ (a ∙ c) - cancelʳ : a ∙ c ≈ ε → (b ∙ a) ∙ c ≈ b - cancelˡ : a ∙ c ≈ ε → a ∙ (c ∙ b) ≈ b - insertˡ : a ∙ c ≈ ε → b ≈ a ∙ (c ∙ b) - insertʳ : a ∙ c ≈ ε → b ≈ (b ∙ a) ∙ c - cancelᶜ : a ∙ c ≈ ε → (b ∙ a) ∙ (c ∙ d) ≈ b ∙ d - insertᶜ : a ∙ c ≈ ε ∙ d ≈ (b ∙ a) ∙ (c ∙ d) - ``` - -* In `Algebra.Properties.Semigroup`: - ```agda - uv≈w⇒xu∙v≈xw : x → (x ∙ u) ∙ v ≈ x ∙ w - uv≈w⇒u∙vx≈wx : u ∙ (v ∙ x) ≈ w ∙ x - uv≈w⇒u[vx∙y]≈w∙xy : u ∙ ((v ∙ x) ∙ y) ≈ w ∙ (x ∙ y) - uv≈w⇒x[uv∙y]≈x∙wy : x ∙ (u ∙ (v ∙ y)) ≈ x ∙ (w ∙ y) - uv≈w⇒[x∙yu]v≈x∙yw : (x ∙ (y ∙ u)) ∙ v ≈ x ∙ (y ∙ w) - uv≈w⇒[xu∙v]y≈x∙wy : ((x ∙ u) ∙ v) ∙ y ≈ x ∙ (w ∙ y) - uv≈w⇒[xy∙u]v≈x∙yw : ((x ∙ y) ∙ u) ∙ v ≈ x ∙ (y ∙ w) - uv≈w⇒xu∙vy≈x∙wy : (x ∙ u) ∙ (v ∙ y) ≈ x ∙ (w ∙ y) - uv≈w⇒xy≈z⇒u[vx∙y]≈wz : x ∙ y ≈ z → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z - uv≈w⇒x∙wy≈x∙[u∙vy] : x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y)) - [uv∙w]x≈u[vw∙x] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ ((v ∙ w) ∙ x) - [uv∙w]x≈u[v∙wx] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ (v ∙ (w ∙ x)) - [u∙vw]x≈uv∙wx : (u ∙ (v ∙ w)) ∙ x ≈ (u ∙ v) ∙ (w ∙ x) - [u∙vw]x≈u[v∙wx] : (u ∙ (v ∙ w)) ∙ x ≈ u ∙ (v ∙ (w ∙ x)) - uv∙wx≈u[vw∙x] : (u ∙ v) ∙ (w ∙ x) ≈ u ∙ ((v ∙ w) ∙ x) - uv≈wx⇒yu∙v≈yw∙x : (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x - uv≈wx⇒u∙vy≈w∙xy : u ∙ (v ∙ y) ≈ w ∙ (x ∙ y) - uv≈wx⇒yu∙vz≈yw∙xz : (y ∙ u) ∙ (v ∙ z) ≈ (y ∙ w) ∙ (x ∙ z) - ``` - - -* In `Algebra.Properties.Semigroup.Divisibility`: - ```agda - ∣ˡ-trans : Transitive _∣ˡ_ - x∣ʳy⇒x∣ʳzy : x ∣ʳ y → x ∣ʳ z ∙ y - x∣ʳy⇒xz∣ʳyz : x ∣ʳ y → x ∙ z ∣ʳ y ∙ z - x∣ˡy⇒zx∣ˡzy : x ∣ˡ y → z ∙ x ∣ˡ z ∙ y - x∣ˡy⇒x∣ˡyz : x ∣ˡ y → x ∣ˡ y ∙ z - ``` - -* In `Algebra.Properties.CommutativeSemigroup.Divisibility`: - ```agda - ∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b - ``` - * In `Algebra.Structures`: ```agda record IsBooleanSemiring + * 0# 1# : Set _ record IsBooleanRing + * - 0# 1# : Set _ ``` NB. the latter is based on `IsCommutativeRing`, with the former on `IsSemiring`. - -* In `Data.Bool.Properties`: - ```agda - if-eta : if b then x else x ≡ x - if-idem-then : (if b then (if b then x else y) else y) ≡ (if b then x else y) - if-idem-else : (if b then x else (if b then x else y)) ≡ (if b then x else y) - if-swap-then : (if b then (if c then x else y) else y) ≡ (if c then (if b then x else y) else y) - if-swap-else : (if b then x else (if c then x else y)) ≡ (if c then x else (if b then x else y)) - if-not : (if not b then x else y) ≡ (if b then y else x) - if-∧ : (if b ∧ c then x else y) ≡ (if b then (if c then x else y) else y) - if-∨ : (if b ∨ c then x else y) ≡ (if b then x else (if c then x else y)) - if-xor : (if b xor c then x else y) ≡ (if b then (if c then y else x) else (if c then x else y)) - if-cong : b ≡ c → (if b then x else y) ≡ (if c then x else y) - if-cong-then : x ≡ z → (if b then x else y) ≡ (if b then z else y) - if-cong-else : y ≡ z → (if b then x else y) ≡ (if b then x else z) - if-cong₂ : x ≡ z → y ≡ w → (if b then x else y) ≡ (if b then z else w) - ``` - -* In `Data.Fin.Base`: - ```agda - _≰_ : Rel (Fin n) 0ℓ - _≮_ : Rel (Fin n) 0ℓ - lower : ∀ (i : Fin m) → .(toℕ i ℕ.< n) → Fin n - ``` - -* In `Data.Fin.Permutation`: - ```agda - cast-id : .(m ≡ n) → Permutation m n - swap : Permutation m n → Permutation (2+ m) (2+ n) - ``` - -* In `Data.Fin.Properties`: - ```agda - cast-involutive : .(eq₁ : m ≡ n) .(eq₂ : n ≡ m) → ∀ k → cast eq₁ (cast eq₂ k) ≡ k - inject!-injective : Injective _≡_ _≡_ inject! - inject!-< : (k : Fin′ i) → inject! k < i - lower-injective : lower i i Date: Sun, 20 Jul 2025 20:25:42 +0100 Subject: [PATCH 27/27] fix: whitespace --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index db1b7fe33e..18bb61e8b2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -65,4 +65,4 @@ Additions to existing modules record IsBooleanRing + * - 0# 1# : Set _ ``` NB. the latter is based on `IsCommutativeRing`, with the former on `IsSemiring`. - \ No newline at end of file +