diff --git a/CHANGELOG.md b/CHANGELOG.md index 3cf9a9ac90..18bb61e8b2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -24,5 +24,45 @@ Deprecated names New modules ----------- +* `Algebra.Properties.BooleanRing`. + +* `Algebra.Properties.BooleanSemiring`. + +* `Algebra.Properties.CommutativeRing`. + +* `Algebra.Properties.Semiring`. + Additions to existing modules ----------------------------- + +* In `Algebra.Bundles`: + ```agda + record BooleanSemiring _ _ : Set _ + record BooleanRing _ _ : Set _ + ``` + +* 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 + binomial-expansion : Congruent₂ _∙_ → Associative _∙_ → _◦_ DistributesOver _∙_ → + ∀ w x y z → ((w ∙ x) ◦ (y ∙ z)) ≈ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z)) + ``` + +* In `Algebra.Lattice.Properties.BooleanAlgebra.XorRing`: + ```agda + ⊕-∧-isBooleanRing : IsBooleanRing _⊕_ _∧_ id ⊥ ⊤ + ⊕-∧-booleanRing : BooleanRing _ _ + ``` + +* 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`. + diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 88b195ec7d..bc66a893f4 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -921,6 +921,41 @@ 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 } + + 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 } + + open IdempotentMonoid *-idempotentMonoid public + using () renaming (band to *-band) + + ------------------------------------------------------------------------ -- Bundles with 2 binary operations, 1 unary operation & 1 element ------------------------------------------------------------------------ @@ -1106,7 +1141,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 = @@ -1124,6 +1162,47 @@ 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 + using (isCommutativeRing; *-idem) + + open IsCommutativeRing isCommutativeRing public + + commutativeRing : CommutativeRing _ _ + commutativeRing = record { isCommutativeRing = isCommutativeRing } + + open CommutativeRing commutativeRing public + using + (_≉_; rawRing + ; +-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 + ) + + ------------------------------------------------------------------------ -- Bundles with 3 binary operations ------------------------------------------------------------------------ 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/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 _⊕_ diff --git a/src/Algebra/Properties/BooleanRing.agda b/src/Algebra/Properties/BooleanRing.agda new file mode 100644 index 0000000000..c0c28b979b --- /dev/null +++ b/src/Algebra/Properties/BooleanRing.agda @@ -0,0 +1,61 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Some basic properties of Boolean Rings +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles + using (CommutativeRing; BooleanSemiring; BooleanRing) + +module Algebra.Properties.BooleanRing + {c ℓ} (booleanRing : BooleanRing c ℓ) where + +open import Function.Base using (_∘_) +open import Data.Product.Base using (_,_) + +open BooleanRing booleanRing +open import Algebra.Structures _≈_ + using (IsBooleanSemiring) +open import Relation.Binary.Reasoning.Setoid setoid + +------------------------------------------------------------------------ +-- Re-export properties of Commutative Rings + +open import Algebra.Properties.CommutativeRing commutativeRing public + +------------------------------------------------------------------------ +-- Structures + +isBooleanSemiring : IsBooleanSemiring _+_ _*_ 0# 1# +isBooleanSemiring = record + { isSemiring = isSemiring + ; +-cancel = +-cancel + ; *-idem = *-idem + } + +open IsBooleanSemiring isBooleanSemiring public + using (*-isIdempotentMonoid) + +------------------------------------------------------------------------ +-- Bundles + +booleanSemiring : BooleanSemiring _ _ +booleanSemiring = record { isBooleanSemiring = isBooleanSemiring } + +open BooleanSemiring booleanSemiring public + using (*-idempotentMonoid) + +------------------------------------------------------------------------ +-- Export properties of Boolean semirings + +open import Algebra.Properties.BooleanSemiring booleanSemiring public + hiding (isBooleanRing; booleanRing) + +------------------------------------------------------------------------ +-- Further consequences + +-x≈x : ∀ x → - x ≈ x +-x≈x = x+y≈0⇒y≈x ∘ -‿inverseʳ + diff --git a/src/Algebra/Properties/BooleanSemiring.agda b/src/Algebra/Properties/BooleanSemiring.agda new file mode 100644 index 0000000000..b36898ccbb --- /dev/null +++ b/src/Algebra/Properties/BooleanSemiring.agda @@ -0,0 +1,319 @@ +------------------------------------------------------------------------ +-- 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 Algebra.Core using (Op₁; Op₂) +open import Algebra.Lattice.Bundles + 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; _∘_; _$_) + +open BooleanSemiring booleanSemiring +import Algebra.Consequences.Setoid setoid as Consequences +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 (IsMagma; IsSemigroup; IsBand + ; IsCommutativeMonoid; IsIdempotentCommutativeMonoid + ; IsGroup; IsAbelianGroup + ; IsRing; IsCommutativeRing; IsBooleanRing + ) +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 ≈⟨ 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 ∎ + +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 } + +open CommutativeRing commutativeRing public + using (ring) + +booleanRing : BooleanRing _ _ +booleanRing = record { isBooleanRing = isBooleanRing } + +------------------------------------------------------------------------ +-- Boolean Semirings yield Boolean Algebras + +-- Definitions + +infix 8 ¬_ +¬_ : Op₁ Carrier +¬ x = 1# + x + +¬-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 ⟩ + x * 1# + x * x ≈⟨ +-cong (*-identityʳ x) (*-idem x) ⟩ + 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) ⟩ + 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′)) + +∨-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 ∎ + +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 ≈⟨ binomial-expansion 1# x 1# y ⟨ + (1# + x) * (1# + y) ≡⟨⟩ + ¬ x * ¬ y ∎ + where open CommutativeMonoidProperties +-commutativeMonoid + +∨-assoc : Associative _∨_ +∨-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 + +∨-absorbs-* : _∨_ Absorbs _*_ +∨-absorbs-* x y = begin + x ∨ x * y ≈⟨ +-congˡ (xy∙z≈xz∙y x y (¬ x)) ⟩ + x + (x * ¬ x) * y ≈⟨ *-lemma x y ⟩ + x ∎ + where open CommutativeMonoidProperties *-commutativeMonoid + +*-absorbs-∨ : _*_ Absorbs _∨_ +*-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 + +*-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 + +∨-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 = record { isBand = *-isBand ; comm = *-comm } + ; isMeetSemilattice = record { isBand = ∨-isBand ; comm = ∨-comm } + ; absorptive = *-absorbs-∨ , ∨-absorbs-* + } + +*-∨-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 + ; ∨-complementʳ = ∨-complementʳ + ; ∧-complementʳ = ∧-complementʳ + ; ¬-cong = ¬-cong + } + +-- Bundle + +booleanAlgebra : BooleanAlgebra _ _ +booleanAlgebra = record { isBooleanAlgebra = isBooleanAlgebra } 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 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/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# 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 + diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 1b465c6d0f..a92d24f8d2 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,6 +984,16 @@ record IsCommutativeRing ; *-isCommutativeMonoid ) + +record IsBooleanRing + (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where + field + isCommutativeRing : IsCommutativeRing + * - 0# 1# + *-idem : Idempotent * + + open IsCommutativeRing isCommutativeRing public + + ------------------------------------------------------------------------ -- Structures with 3 binary operations ------------------------------------------------------------------------