diff --git a/CHANGELOG.md b/CHANGELOG.md index 7b585690f4..560ae43a9b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,7 +7,7 @@ Highlights ---------- * A golden testing library in `Test.Golden`. This allows you to run a set - of tests and make sure their output matches an expected `golden' value. + of tests and make sure their output matches an expected `golden` value. The test runner has many options: filtering tests by name, dumping the list of failures to a file, timing the runs, coloured output, etc. Cf. the comments in `Test.Golden` and the standard library's own tests @@ -31,19 +31,11 @@ Bug-fixes Non-backwards compatible changes -------------------------------- -* In `Algebra.Morphism.Structures`, `IsNearSemiringHomomorphism`, - `IsSemiringHomomorphism`, and `IsRingHomomorphism` have been redeisgned to - build up from `IsMonoidHomomorphism`, `IsNearSemiringHomomorphism`, and - `IsSemiringHomomorphism` respectively, adding a single property at each step. - This means that they no longer need to have two separate proofs of - `IsRelHomomorphism`. Similarly, `IsLatticeHomomorphism` is now built as - `IsRelHomomorphism` along with proofs that `_∧_` and `_∨_` are homorphic. +#### Removed deprecated names - Also, `⁻¹-homo` in `IsRingHomomorphism` has been renamed to `-‿homo`. +* All modules and names that were deprecated prior to v1.0 have been removed. -* move definition of `_>>=_` under `Data.Vec.Base` to its submodule `CartesianBind` - in order to keep another new definition of `_>>=_`, located in `DiagonalBind` - which is also a submodule of `Data.Vec.Base`. +### Improvements to pretty printing and regexes * In `Text.Pretty`, `Doc` is now a record rather than a type alias. This helps Agda reconstruct the `width` parameter when the module is opened @@ -75,9 +67,64 @@ Non-backwards compatible changes So `[a-zA-Z]+.agdai?` run on "the path _build/Main.agdai corresponds to" will return "Main.agdai" when it used to be happy to just return "n.agda". -#### Removed deprecated names -* All modules and names that were deprecated prior to v1.0 have been removed. +### Refactoring of algebraic lattice hierarchy + +* In order to improve modularity and consistency with `Relation.Binary.Lattice`, + the structures & bundles for `Semilattice`, `Lattice`, `DistributiveLattice` + & `BooleanAlgebra` have been moved out of the `Algebra` modules and into their + own hierarchy in `Algebra.Lattice`. + +* All submodules, (e.g. `Algebra.Properties.Semilattice` or `Algebra.Morphism.Lattice`) + have been moved to the corresponding place under `Algebra.Lattice` (e.g. + `Algebra.Lattice.Properties.Semilattice` or `Algebra.Lattice.Morphism.Lattice`). See + the `Deprecated modules` section below for full details. + +* Changed definition of `IsDistributiveLattice` and `IsBooleanAlgebra` so that they are + no longer right-biased which hinders compositionality. More concretely, `IsDistributiveLattice` + now has fields: + ```agda + ∨-distrib-∧ : ∨ DistributesOver ∧ + ∧-distrib-∨ : ∧ DistributesOver ∨ + ``` + instead of + ```agda + ∨-distribʳ-∧ : ∨ DistributesOverʳ ∧ + ``` + and `IsBooleanAlgebra` now has fields: + ``` + ∨-complement : Inverse ⊤ ¬ ∨ + ∧-complement : Inverse ⊥ ¬ ∧ + ``` + instead of: + ```agda + ∨-complementʳ : RightInverse ⊤ ¬ ∨ + ∧-complementʳ : RightInverse ⊥ ¬ ∧ + ``` + +* To allow construction of these structures via their old form, smart constructors + have been added to a new module `Algebra.Lattice.Structures.Biased`, which are by + re-exported automatically by `Algebra.Lattice`. For example, if before you wrote: + ```agda + ∧-∨-isDistributiveLattice = record + { isLattice = ∧-∨-isLattice + ; ∨-distribʳ-∧ = ∨-distribʳ-∧ + } + ``` + you can use the smart constructor `isDistributiveLatticeʳʲᵐ` to write: + ```agda + ∧-∨-isDistributiveLattice = isDistributiveLatticeʳʲᵐ (record + { isLattice = ∧-∨-isLattice + ; ∨-distribʳ-∧ = ∨-distribʳ-∧ + }) + ``` + without having to prove full distributivity. + +* Added new `IsBoundedSemilattice`/`BoundedSemilattice` records. + +* Added new aliases `Is(Meet/Join)(Bounded)Semilattice` for `Is(Bounded)Semilattice` + which can be used to indicate meet/join-ness of the original structures. + #### Proofs of non-zeroness/positivity/negativity as instance arguments @@ -202,9 +249,23 @@ Non-backwards compatible changes domain) so that `_⟶_` can be inferred, which it could not from the previous implementation using the sum type `a ⟶ b ⊎ b ⟶ a`. - ### Creation of `Relation.Binary.Lattice` hierarchy - * In order to improve modularity Relation.Binary.Lattice is split out into Relation.Binary.Lattice.(Definitions/Structures/Bundles). - ### +* In `Algebra.Morphism.Structures`, `IsNearSemiringHomomorphism`, + `IsSemiringHomomorphism`, and `IsRingHomomorphism` have been redeisgned to + build up from `IsMonoidHomomorphism`, `IsNearSemiringHomomorphism`, and + `IsSemiringHomomorphism` respectively, adding a single property at each step. + This means that they no longer need to have two separate proofs of + `IsRelHomomorphism`. Similarly, `IsLatticeHomomorphism` is now built as + `IsRelHomomorphism` along with proofs that `_∧_` and `_∨_` are homorphic. + + Also, `⁻¹-homo` in `IsRingHomomorphism` has been renamed to `-‿homo`. + +* Moved definition of `_>>=_` under `Data.Vec.Base` to its submodule `CartesianBind` + in order to keep another new definition of `_>>=_`, located in `DiagonalBind` + which is also a submodule of `Data.Vec.Base`. + +* The constructors `+0` and `+[1+_]` from `Data.Integer.Base` are no longer + exported by `Data.Rational.Base`. You will have to open `Data.Integer(.Base)` + directly to use them. Deprecated modules ------------------ @@ -227,6 +288,17 @@ Deprecated modules Equivalence-kind ↦ EquivalenceKind ``` +### Moving `Algebra.Lattice` files + +* As discussed above the following files have been moved: + ```agda + Algebra.Properties.Semilattice ↦ Algebra.Lattice.Properties.Semilattice + Algebra.Properties.Lattice ↦ Algebra.Lattice.Properties.Lattice + Algebra.Properties.DistributiveLattice ↦ Algebra.Lattice.Properties.DistributiveLattice + Algebra.Properties.BooleanAlgebra ↦ Algebra.Lattice.Properties.BooleanAlgebra + Algebra.Properties.BooleanAlgebra.Expression ↦ Algebra.Lattice.Properties.BooleanAlgebra.Expression + Algebra.Morphism.LatticeMonomorphism ↦ Algebra.Lattice.Morphism.LatticeMonomorphism + ``` Deprecated names ---------------- @@ -406,6 +478,15 @@ New modules Function.Properties.Surjection ``` +* In order to improve modularity, the contents of `Relation.Binary.Lattice` has been + split out into the standard: + ``` + Relation.Binary.Lattice.Definitions + Relation.Binary.Lattice.Structures + Relation.Binary.Lattice.Bundles + ``` + All contents is re-exported by `Relation.Binary.Lattice` as before. + * Both versions of equality on predications are equivalences ``` Relation.Unary.Relation.Binary.Equality @@ -460,12 +541,15 @@ Other minor changes * Added new proofs to `Algebra.Consequences.Setoid`: ```agda - comm+idˡ⇒id : Commutative _•_ → LeftIdentity e _•_ → Identity e _•_ - comm+idʳ⇒id : Commutative _•_ → RightIdentity e _•_ → Identity e _•_ - comm+zeˡ⇒ze : Commutative _•_ → LeftZero e _•_ → Zero e _•_ - comm+zeʳ⇒ze : Commutative _•_ → RightZero e _•_ → Zero e _•_ - comm+distrˡ⇒distr : Commutative _•_ → _•_ DistributesOverˡ _◦_ → _•_ DistributesOver _◦_ - comm+distrʳ⇒distr : Commutative _•_ → _•_ DistributesOverʳ _◦_ → _•_ DistributesOver _◦_ + comm+idˡ⇒id : Commutative _•_ → LeftIdentity e _•_ → Identity e _•_ + comm+idʳ⇒id : Commutative _•_ → RightIdentity e _•_ → Identity e _•_ + comm+zeˡ⇒ze : Commutative _•_ → LeftZero e _•_ → Zero e _•_ + comm+zeʳ⇒ze : Commutative _•_ → RightZero e _•_ → Zero e _•_ + comm+invˡ⇒inv : Commutative _•_ → LeftInverse e _⁻¹ _•_ → Inverse e _⁻¹ _•_ + comm+invʳ⇒inv : Commutative _•_ → RightInverse e _⁻¹ _•_ → Inverse e _⁻¹ _•_ + comm+distrˡ⇒distr : Commutative _•_ → _•_ DistributesOverˡ _◦_ → _•_ DistributesOver _◦_ + comm+distrʳ⇒distr : Commutative _•_ → _•_ DistributesOverʳ _◦_ → _•_ DistributesOver _◦_ + distrib+absorbs⇒distribˡ : Associative _•_ → Commutative _◦_ → _•_ Absorbs _◦_ → _◦_ Absorbs _•_ → _◦_ DistributesOver _•_ → _•_ DistributesOverˡ _◦_ ``` * Added new functions to `Algebra.Construct.DirectProduct`: diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 1a25c9db9c..6614742f70 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -143,25 +143,6 @@ record CommutativeSemigroup c ℓ : Set (suc (c ⊔ ℓ)) where commutativeMagma : CommutativeMagma c ℓ commutativeMagma = record { isCommutativeMagma = isCommutativeMagma } - -record Semilattice c ℓ : Set (suc (c ⊔ ℓ)) where - infixr 7 _∧_ - infix 4 _≈_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ - _∧_ : Op₂ Carrier - isSemilattice : IsSemilattice _≈_ _∧_ - - open IsSemilattice isSemilattice public - - band : Band c ℓ - band = record { isBand = isBand } - - open Band band public - using (_≉_; rawMagma; magma; semigroup) - - ------------------------------------------------------------------------ -- Bundles with 1 binary operation & 1 element ------------------------------------------------------------------------ @@ -417,81 +398,6 @@ record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where open CommutativeMonoid commutativeMonoid public using (commutativeMagma; commutativeSemigroup) - ------------------------------------------------------------------------- --- Bundles with 2 binary operations ------------------------------------------------------------------------- - -record RawLattice c ℓ : Set (suc (c ⊔ ℓ)) where - infixr 7 _∧_ - infixr 6 _∨_ - infix 4 _≈_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ - _∧_ : Op₂ Carrier - _∨_ : Op₂ Carrier - - ∨-rawMagma : RawMagma c ℓ - ∨-rawMagma = record { _≈_ = _≈_; _∙_ = _∨_ } - - ∧-rawMagma : RawMagma c ℓ - ∧-rawMagma = record { _≈_ = _≈_; _∙_ = _∧_ } - - open RawMagma ∨-rawMagma public - using (_≉_) - - -record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where - infixr 7 _∧_ - infixr 6 _∨_ - infix 4 _≈_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ - _∨_ : Op₂ Carrier - _∧_ : Op₂ Carrier - isLattice : IsLattice _≈_ _∨_ _∧_ - - open IsLattice isLattice public - - rawLattice : RawLattice c ℓ - rawLattice = record - { _≈_ = _≈_ - ; _∧_ = _∧_ - ; _∨_ = _∨_ - } - - open RawLattice rawLattice public - using (∨-rawMagma; ∧-rawMagma) - - setoid : Setoid _ _ - setoid = record { isEquivalence = isEquivalence } - - open Setoid setoid public - using (_≉_) - - -record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where - infixr 7 _∧_ - infixr 6 _∨_ - infix 4 _≈_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ - _∨_ : Op₂ Carrier - _∧_ : Op₂ Carrier - isDistributiveLattice : IsDistributiveLattice _≈_ _∨_ _∧_ - - open IsDistributiveLattice isDistributiveLattice public - - lattice : Lattice _ _ - lattice = record { isLattice = isLattice } - - open Lattice lattice public - using (_≉_; rawLattice; setoid) - - ------------------------------------------------------------------------ -- Bundles with 2 binary operations & 1 element ------------------------------------------------------------------------ @@ -976,31 +882,6 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where ; commutativeSemiringWithoutOne ) - -record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where - infix 8 ¬_ - infixr 7 _∧_ - infixr 6 _∨_ - infix 4 _≈_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ - _∨_ : Op₂ Carrier - _∧_ : Op₂ Carrier - ¬_ : Op₁ Carrier - ⊤ : Carrier - ⊥ : Carrier - isBooleanAlgebra : IsBooleanAlgebra _≈_ _∨_ _∧_ ¬_ ⊤ ⊥ - - open IsBooleanAlgebra isBooleanAlgebra public - - distributiveLattice : DistributiveLattice _ _ - distributiveLattice = record { isDistributiveLattice = isDistributiveLattice } - - open DistributiveLattice distributiveLattice public - using (_≉_; setoid; lattice) - - ------------------------------------------------------------------------ -- DEPRECATED NAMES ------------------------------------------------------------------------ diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda index 450b25f7a3..8e97b77305 100644 --- a/src/Algebra/Consequences/Setoid.agda +++ b/src/Algebra/Consequences/Setoid.agda @@ -117,12 +117,18 @@ module _ {_•_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _•_) whe (x ⁻¹) • x ≈⟨ invˡ x ⟩ e ∎ + comm+invˡ⇒inv : LeftInverse e _⁻¹ _•_ → Inverse e _⁻¹ _•_ + comm+invˡ⇒inv invˡ = invˡ , comm+invˡ⇒invʳ invˡ + comm+invʳ⇒invˡ : RightInverse e _⁻¹ _•_ → LeftInverse e _⁻¹ _•_ comm+invʳ⇒invˡ invʳ x = begin (x ⁻¹) • x ≈⟨ comm (x ⁻¹) x ⟩ x • (x ⁻¹) ≈⟨ invʳ x ⟩ e ∎ + comm+invʳ⇒inv : RightInverse e _⁻¹ _•_ → Inverse e _⁻¹ _•_ + comm+invʳ⇒inv invʳ = comm+invʳ⇒invˡ invʳ , invʳ + module _ {_•_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _•_) where assoc+id+invʳ⇒invˡ-unique : Associative _•_ → @@ -182,6 +188,26 @@ module _ {_•_ _◦_ : Op₂ A} (x ◦ y) • (x ◦ z) ≈⟨ •-comm (x ◦ y) (x ◦ z) ⟩ (x ◦ z) • (x ◦ y) ∎ + +module _ {_•_ _◦_ : Op₂ A} + (•-cong : Congruent₂ _•_) + (•-assoc : Associative _•_) + (◦-comm : Commutative _◦_) + where + + distrib+absorbs⇒distribˡ : _•_ Absorbs _◦_ → + _◦_ Absorbs _•_ → + _◦_ DistributesOver _•_ → + _•_ DistributesOverˡ _◦_ + distrib+absorbs⇒distribˡ •-absorbs-◦ ◦-absorbs-• (◦-distribˡ-• , ◦-distribʳ-•) x y z = begin + x • (y ◦ z) ≈˘⟨ •-cong (•-absorbs-◦ _ _) refl ⟩ + (x • (x ◦ y)) • (y ◦ z) ≈⟨ •-cong (•-cong refl (◦-comm _ _)) refl ⟩ + (x • (y ◦ x)) • (y ◦ z) ≈⟨ •-assoc _ _ _ ⟩ + x • ((y ◦ x) • (y ◦ z)) ≈˘⟨ •-cong refl (◦-distribˡ-• _ _ _) ⟩ + x • (y ◦ (x • z)) ≈˘⟨ •-cong (◦-absorbs-• _ _) refl ⟩ + (x ◦ (x • z)) • (y ◦ (x • z)) ≈˘⟨ ◦-distribʳ-• _ _ _ ⟩ + (x • y) ◦ (x • z) ∎ + ---------------------------------------------------------------------- -- Ring-like structures diff --git a/src/Algebra/Construct/DirectProduct.agda b/src/Algebra/Construct/DirectProduct.agda index a6bdc5d349..145bd066b7 100644 --- a/src/Algebra/Construct/DirectProduct.agda +++ b/src/Algebra/Construct/DirectProduct.agda @@ -111,15 +111,6 @@ commutativeSemigroup G H = record } } where module G = CommutativeSemigroup G; module H = CommutativeSemigroup H -semilattice : Semilattice a ℓ₁ → Semilattice b ℓ₂ → - Semilattice (a ⊔ b) (ℓ₁ ⊔ ℓ₂) -semilattice L M = record - { isSemilattice = record - { isBand = Band.isBand (band L.band M.band) - ; comm = λ x y → (L.comm , M.comm) <*> x <*> y - } - } where module L = Semilattice L; module M = Semilattice M - monoid : Monoid a ℓ₁ → Monoid b ℓ₂ → Monoid (a ⊔ b) (ℓ₁ ⊔ ℓ₂) monoid M N = record { ε = M.ε , N.ε diff --git a/src/Algebra/Construct/LiftedChoice.agda b/src/Algebra/Construct/LiftedChoice.agda index 562e0f01e5..790c5b85af 100644 --- a/src/Algebra/Construct/LiftedChoice.agda +++ b/src/Algebra/Construct/LiftedChoice.agda @@ -16,13 +16,8 @@ open import Relation.Nullary using (¬_; yes; no) open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]) open import Data.Product using (_×_; _,_) open import Level using (Level; _⊔_) -open import Function.Base using (id; _on_) -open import Function.Injection using (Injection) -open import Function.Equality using (Π) -open import Relation.Binary using (Setoid; _Preserves_⟶_) open import Relation.Binary.PropositionalEquality as P using (_≡_) open import Relation.Unary using (Pred) -open import Relation.Nullary.Negation using (contradiction) import Relation.Binary.Reasoning.Setoid as EqReasoning @@ -134,13 +129,13 @@ module _ {_≈_ : Rel B ℓ} {_∙_ : Op₂ B} isMagma : IsMagma _≈′_ _◦_ isMagma = record { isEquivalence = ≈′-isEquivalence - ; ∙-cong = cong (λ {x y} → f-injective {x} {y}) f-cong + ; ∙-cong = cong (λ {x} → f-injective {x}) f-cong } isSemigroup : Associative _≈_ _∙_ → IsSemigroup _≈′_ _◦_ isSemigroup ∙-assoc = record { isMagma = isMagma - ; assoc = assoc (λ {x y} → f-injective {x} {y}) ∙-assoc + ; assoc = assoc (λ {x} → f-injective {x}) ∙-assoc } isBand : Associative _≈_ _∙_ → IsBand _≈′_ _◦_ @@ -149,13 +144,6 @@ module _ {_≈_ : Rel B ℓ} {_∙_ : Op₂ B} ; idem = idem f E.reflexive } - isSemilattice : Associative _≈_ _∙_ → Commutative _≈_ _∙_ → - IsSemilattice _≈′_ _◦_ - isSemilattice ∙-assoc ∙-comm = record - { isBand = isBand ∙-assoc - ; comm = comm (λ {x y} → f-injective {x} {y}) ∙-comm - } - isSelectiveMagma : IsSelectiveMagma _≈′_ _◦_ isSelectiveMagma = record { isMagma = isMagma diff --git a/src/Algebra/Construct/NaturalChoice/Base.agda b/src/Algebra/Construct/NaturalChoice/Base.agda index 2f92eecfb6..9cdb6b1439 100644 --- a/src/Algebra/Construct/NaturalChoice/Base.agda +++ b/src/Algebra/Construct/NaturalChoice/Base.agda @@ -2,7 +2,7 @@ -- The Agda standard library -- -- Basic definition of an operator that computes the min/max value --- with respect to a total ordering. +-- with respect to a total preorder. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} diff --git a/src/Algebra/Construct/NaturalChoice/Max.agda b/src/Algebra/Construct/NaturalChoice/Max.agda index 2400cf76e0..8ecb520b88 100644 --- a/src/Algebra/Construct/NaturalChoice/Max.agda +++ b/src/Algebra/Construct/NaturalChoice/Max.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- The max operator derived from an arbitrary total order +-- The max operator derived from an arbitrary total preorder. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} diff --git a/src/Algebra/Construct/NaturalChoice/MaxOp.agda b/src/Algebra/Construct/NaturalChoice/MaxOp.agda index 69c3084bdb..49fdde41cb 100644 --- a/src/Algebra/Construct/NaturalChoice/MaxOp.agda +++ b/src/Algebra/Construct/NaturalChoice/MaxOp.agda @@ -1,7 +1,8 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Properties of a max operator derived from a spec over a total order. +-- Properties of a max operator derived from a spec over a total +-- preorder. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} @@ -48,7 +49,6 @@ open Min public ; ⊓-isSemigroup to ⊔-isSemigroup ; ⊓-isCommutativeSemigroup to ⊔-isCommutativeSemigroup ; ⊓-isBand to ⊔-isBand - ; ⊓-isSemilattice to ⊔-isSemilattice ; ⊓-isMonoid to ⊔-isMonoid ; ⊓-isSelectiveMagma to ⊔-isSelectiveMagma @@ -56,7 +56,6 @@ open Min public ; ⊓-semigroup to ⊔-semigroup ; ⊓-commutativeSemigroup to ⊔-commutativeSemigroup ; ⊓-band to ⊔-band - ; ⊓-semilattice to ⊔-semilattice ; ⊓-monoid to ⊔-monoid ; ⊓-selectiveMagma to ⊔-selectiveMagma diff --git a/src/Algebra/Construct/NaturalChoice/Min.agda b/src/Algebra/Construct/NaturalChoice/Min.agda index c1752014cb..7014069e4e 100644 --- a/src/Algebra/Construct/NaturalChoice/Min.agda +++ b/src/Algebra/Construct/NaturalChoice/Min.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- The min operator derived from an arbitrary total order +-- The min operator derived from an arbitrary total preorder. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} diff --git a/src/Algebra/Construct/NaturalChoice/MinMaxOp.agda b/src/Algebra/Construct/NaturalChoice/MinMaxOp.agda index 9d94b2cf05..194716ac8a 100644 --- a/src/Algebra/Construct/NaturalChoice/MinMaxOp.agda +++ b/src/Algebra/Construct/NaturalChoice/MinMaxOp.agda @@ -1,7 +1,8 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Properties of min and max operators specified over a total order +-- Properties of min and max operators specified over a total +-- preorder. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} @@ -107,62 +108,6 @@ open import Algebra.Construct.NaturalChoice.MaxOp maxOp public ⊓-⊔-absorptive : Absorptive _⊓_ _⊔_ ⊓-⊔-absorptive = ⊓-absorbs-⊔ , ⊔-absorbs-⊓ -⊔-⊓-isLattice : IsLattice _⊔_ _⊓_ -⊔-⊓-isLattice = record - { isEquivalence = isEquivalence - ; ∨-comm = ⊔-comm - ; ∨-assoc = ⊔-assoc - ; ∨-cong = ⊔-cong - ; ∧-comm = ⊓-comm - ; ∧-assoc = ⊓-assoc - ; ∧-cong = ⊓-cong - ; absorptive = ⊔-⊓-absorptive - } - -⊓-⊔-isLattice : IsLattice _⊓_ _⊔_ -⊓-⊔-isLattice = record - { isEquivalence = isEquivalence - ; ∨-comm = ⊓-comm - ; ∨-assoc = ⊓-assoc - ; ∨-cong = ⊓-cong - ; ∧-comm = ⊔-comm - ; ∧-assoc = ⊔-assoc - ; ∧-cong = ⊔-cong - ; absorptive = ⊓-⊔-absorptive - } - -⊓-⊔-isDistributiveLattice : IsDistributiveLattice _⊓_ _⊔_ -⊓-⊔-isDistributiveLattice = record - { isLattice = ⊓-⊔-isLattice - ; ∨-distribʳ-∧ = ⊓-distribʳ-⊔ - } - -⊔-⊓-isDistributiveLattice : IsDistributiveLattice _⊔_ _⊓_ -⊔-⊓-isDistributiveLattice = record - { isLattice = ⊔-⊓-isLattice - ; ∨-distribʳ-∧ = ⊔-distribʳ-⊓ - } - -⊔-⊓-lattice : Lattice _ _ -⊔-⊓-lattice = record - { isLattice = ⊔-⊓-isLattice - } - -⊓-⊔-lattice : Lattice _ _ -⊓-⊔-lattice = record - { isLattice = ⊓-⊔-isLattice - } - -⊔-⊓-distributiveLattice : DistributiveLattice _ _ -⊔-⊓-distributiveLattice = record - { isDistributiveLattice = ⊔-⊓-isDistributiveLattice - } - -⊓-⊔-distributiveLattice : DistributiveLattice _ _ -⊓-⊔-distributiveLattice = record - { isDistributiveLattice = ⊓-⊔-isDistributiveLattice - } - ------------------------------------------------------------------------ -- Other joint properties diff --git a/src/Algebra/Construct/NaturalChoice/MinOp.agda b/src/Algebra/Construct/NaturalChoice/MinOp.agda index 9db37596d9..b6f0e37a72 100644 --- a/src/Algebra/Construct/NaturalChoice/MinOp.agda +++ b/src/Algebra/Construct/NaturalChoice/MinOp.agda @@ -1,7 +1,8 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Properties of a min operator derived from a spec over a total order. +-- Properties of a min operator derived from a spec over a total +-- preorder. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} @@ -142,12 +143,6 @@ x⊓y≤y x y with total x y ; comm = ⊓-comm } -⊓-isSemilattice : IsSemilattice _⊓_ -⊓-isSemilattice = record - { isBand = ⊓-isBand - ; comm = ⊓-comm - } - ⊓-isSelectiveMagma : IsSelectiveMagma _⊓_ ⊓-isSelectiveMagma = record { isMagma = ⊓-isMagma @@ -161,7 +156,7 @@ x⊓y≤y x y with total x y } ------------------------------------------------------------------------ --- Raw bandles +-- Raw bundles ⊓-rawMagma : RawMagma _ _ ⊓-rawMagma = record { _≈_ = _≈_ ; _∙_ = _⊓_ } @@ -189,11 +184,6 @@ x⊓y≤y x y with total x y { isCommutativeSemigroup = ⊓-isCommutativeSemigroup } -⊓-semilattice : Semilattice _ _ -⊓-semilattice = record - { isSemilattice = ⊓-isSemilattice - } - ⊓-selectiveMagma : SelectiveMagma _ _ ⊓-selectiveMagma = record { isSelectiveMagma = ⊓-isSelectiveMagma diff --git a/src/Algebra/Construct/Subst/Equality.agda b/src/Algebra/Construct/Subst/Equality.agda index b5a0252c9c..a8dda52c87 100644 --- a/src/Algebra/Construct/Subst/Equality.agda +++ b/src/Algebra/Construct/Subst/Equality.agda @@ -83,12 +83,6 @@ isBand {∙} S = record ; idem = idem {∙} S.idem } where module S = IsBand S -isSemilattice : ∀ {∧} → IsSemilattice ≈₁ ∧ → IsSemilattice ≈₂ ∧ -isSemilattice S = record - { isBand = isBand S.isBand - ; comm = comm S.comm - } where module S = IsSemilattice S - isSelectiveMagma : ∀ {∙} → IsSelectiveMagma ≈₁ ∙ → IsSelectiveMagma ≈₂ ∙ isSelectiveMagma S = record { isMagma = isMagma S.isMagma @@ -130,34 +124,6 @@ isAbelianGroup S = record ; comm = comm S.comm } where module S = IsAbelianGroup S -isLattice : ∀ {∨ ∧} → IsLattice ≈₁ ∨ ∧ → IsLattice ≈₂ ∨ ∧ -isLattice {∨} {∧} S = record - { isEquivalence = isEquivalence S.isEquivalence - ; ∨-comm = comm S.∨-comm - ; ∨-assoc = assoc {∨} S.∨-assoc - ; ∨-cong = cong₂ S.∨-cong - ; ∧-comm = comm S.∧-comm - ; ∧-assoc = assoc {∧} S.∧-assoc - ; ∧-cong = cong₂ S.∧-cong - ; absorptive = absorptive {∨} {∧} S.absorptive - } where module S = IsLattice S - -isDistributiveLattice : ∀ {∨ ∧} → - IsDistributiveLattice ≈₁ ∨ ∧ → IsDistributiveLattice ≈₂ ∨ ∧ -isDistributiveLattice S = record - { isLattice = isLattice S.isLattice - ; ∨-distribʳ-∧ = λ x y z → to (S.∨-distribʳ-∧ x y z) - } where module S = IsDistributiveLattice S - -isBooleanAlgebra : ∀ {∨ ∧ ¬ ⊤ ⊥} → - IsBooleanAlgebra ≈₁ ∨ ∧ ¬ ⊤ ⊥ → IsBooleanAlgebra ≈₂ ∨ ∧ ¬ ⊤ ⊥ -isBooleanAlgebra S = record - { isDistributiveLattice = isDistributiveLattice S.isDistributiveLattice - ; ∨-complementʳ = to ∘ S.∨-complementʳ - ; ∧-complementʳ = to ∘ S.∧-complementʳ - ; ¬-cong = cong₁ S.¬-cong - } where module S = IsBooleanAlgebra S - isNearSemiring : ∀ {+ * 0#} → IsNearSemiring ≈₁ + * 0# → IsNearSemiring ≈₂ + * 0# isNearSemiring S = record diff --git a/src/Algebra/Construct/Zero.agda b/src/Algebra/Construct/Zero.agda index ea61540460..12f5c87ffe 100644 --- a/src/Algebra/Construct/Zero.agda +++ b/src/Algebra/Construct/Zero.agda @@ -47,9 +47,6 @@ band = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } commutativeSemigroup : CommutativeSemigroup c ℓ commutativeSemigroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } -semilattice : Semilattice c ℓ -semilattice = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } - monoid : Monoid c ℓ monoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } diff --git a/src/Algebra/Lattice.agda b/src/Algebra/Lattice.agda new file mode 100644 index 0000000000..2ea6eee951 --- /dev/null +++ b/src/Algebra/Lattice.agda @@ -0,0 +1,18 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definitions of algebraic structures like semilattices and lattices +-- (packed in records together with sets, operations, etc.), defined via +-- meet/join operations and their properties +-- +-- For lattices defined via an order relation, see +-- Relation.Binary.Lattice. +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Algebra.Lattice where + +open import Algebra.Lattice.Structures public +open import Algebra.Lattice.Structures.Biased public +open import Algebra.Lattice.Bundles public diff --git a/src/Algebra/Lattice/Bundles.agda b/src/Algebra/Lattice/Bundles.agda new file mode 100644 index 0000000000..51fa917160 --- /dev/null +++ b/src/Algebra/Lattice/Bundles.agda @@ -0,0 +1,237 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definitions of algebraic structures like semilattices and lattices +-- (packed in records together with sets, operations, etc.), defined via +-- meet/join operations and their properties +-- +-- For lattices defined via an order relation, see +-- Relation.Binary.Lattice. +------------------------------------------------------------------------ + +-- The contents of this module should be accessed via `Algebra.Lattice`. + +{-# OPTIONS --without-K --safe #-} + +module Algebra.Lattice.Bundles where + +open import Algebra.Core +open import Algebra.Bundles +open import Algebra.Structures +open import Algebra.Lattice.Structures +open import Level using (suc; _⊔_) +open import Relation.Binary + +record Semilattice c ℓ : Set (suc (c ⊔ ℓ)) where + infixr 7 _∙_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∙_ : Op₂ Carrier + isSemilattice : IsSemilattice _≈_ _∙_ + + open IsSemilattice isSemilattice public + + band : Band c ℓ + band = record { isBand = isBand } + + open Band band public + using (_≉_; rawMagma; magma; isMagma; semigroup; isSemigroup; isBand) + + +record MeetSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where + infixr 7 _∧_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∧_ : Op₂ Carrier + isMeetSemilattice : IsSemilattice _≈_ _∧_ + + open IsMeetSemilattice _≈_ isMeetSemilattice public + + semilattice : Semilattice c ℓ + semilattice = record { isSemilattice = isMeetSemilattice } + + open Semilattice semilattice public + using (rawMagma; magma; semigroup; band) + + +record JoinSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where + infixr 7 _∨_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∨_ : Op₂ Carrier + isJoinSemilattice : IsSemilattice _≈_ _∨_ + + open IsJoinSemilattice _≈_ isJoinSemilattice public + + semilattice : Semilattice c ℓ + semilattice = record { isSemilattice = isJoinSemilattice } + + open Semilattice semilattice public + using (rawMagma; magma; semigroup; band) + + +record BoundedSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where + infixr 7 _∙_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∙_ : Op₂ Carrier + ε : Carrier + isBoundedSemilattice : IsBoundedSemilattice _≈_ _∙_ ε + + open IsBoundedSemilattice _≈_ isBoundedSemilattice public + + semilattice : Semilattice c ℓ + semilattice = record { isSemilattice = isSemilattice } + + open Semilattice semilattice public using (rawMagma; magma; semigroup; band) + + +record BoundedMeetSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where + infixr 7 _∧_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∧_ : Op₂ Carrier + ⊤ : Carrier + isBoundedMeetSemilattice : IsBoundedSemilattice _≈_ _∧_ ⊤ + + open IsBoundedMeetSemilattice _≈_ isBoundedMeetSemilattice public + + boundedSemilattice : BoundedSemilattice c ℓ + boundedSemilattice = record + { isBoundedSemilattice = isBoundedMeetSemilattice } + + open BoundedSemilattice boundedSemilattice public + using (rawMagma; magma; semigroup; band; semilattice) + + +record BoundedJoinSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where + infixr 7 _∨_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∨_ : Op₂ Carrier + ⊥ : Carrier + isBoundedJoinSemilattice : IsBoundedSemilattice _≈_ _∨_ ⊥ + + open IsBoundedJoinSemilattice _≈_ isBoundedJoinSemilattice public + + boundedSemilattice : BoundedSemilattice c ℓ + boundedSemilattice = record + { isBoundedSemilattice = isBoundedJoinSemilattice } + + open BoundedSemilattice boundedSemilattice public + using (rawMagma; magma; semigroup; band; semilattice) + + +record RawLattice c ℓ : Set (suc (c ⊔ ℓ)) where + infixr 7 _∧_ + infixr 6 _∨_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∧_ : Op₂ Carrier + _∨_ : Op₂ Carrier + + ∨-rawMagma : RawMagma c ℓ + ∨-rawMagma = record { _≈_ = _≈_; _∙_ = _∨_ } + + ∧-rawMagma : RawMagma c ℓ + ∧-rawMagma = record { _≈_ = _≈_; _∙_ = _∧_ } + + open RawMagma ∨-rawMagma public + using (_≉_) + + +record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where + infixr 7 _∧_ + infixr 6 _∨_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∨_ : Op₂ Carrier + _∧_ : Op₂ Carrier + isLattice : IsLattice _≈_ _∨_ _∧_ + + open IsLattice isLattice public + + rawLattice : RawLattice c ℓ + rawLattice = record + { _≈_ = _≈_ + ; _∧_ = _∧_ + ; _∨_ = _∨_ + } + + open RawLattice rawLattice public + using (∨-rawMagma; ∧-rawMagma) + + setoid : Setoid c ℓ + setoid = record { isEquivalence = isEquivalence } + + open Setoid setoid public + using (_≉_) + + +record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where + infixr 7 _∧_ + infixr 6 _∨_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∨_ : Op₂ Carrier + _∧_ : Op₂ Carrier + isDistributiveLattice : IsDistributiveLattice _≈_ _∨_ _∧_ + + open IsDistributiveLattice isDistributiveLattice public + + lattice : Lattice _ _ + lattice = record { isLattice = isLattice } + + open Lattice lattice public + using + ( _≉_; setoid; rawLattice + ; ∨-rawMagma; ∧-rawMagma + ) + + +record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where + infix 8 ¬_ + infixr 7 _∧_ + infixr 6 _∨_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∨_ : Op₂ Carrier + _∧_ : Op₂ Carrier + ¬_ : Op₁ Carrier + ⊤ : Carrier + ⊥ : Carrier + isBooleanAlgebra : IsBooleanAlgebra _≈_ _∨_ _∧_ ¬_ ⊤ ⊥ + + open IsBooleanAlgebra isBooleanAlgebra public + + distributiveLattice : DistributiveLattice _ _ + distributiveLattice = record + { isDistributiveLattice = isDistributiveLattice + } + + open DistributiveLattice distributiveLattice public + using + ( _≉_; setoid; rawLattice + ; ∨-rawMagma; ∧-rawMagma + ; lattice + ) diff --git a/src/Algebra/Lattice/Construct/DirectProduct.agda b/src/Algebra/Lattice/Construct/DirectProduct.agda new file mode 100644 index 0000000000..6f896cca2f --- /dev/null +++ b/src/Algebra/Lattice/Construct/DirectProduct.agda @@ -0,0 +1,39 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Instances of algebraic structures made by taking two other instances +-- A and B, and having elements of the new instance be pairs |A| × |B|. +-- In mathematics, this would usually be written A × B or A ⊕ B. +-- +-- From semigroups up, these new instances are products of the relevant +-- category. For structures with commutative addition (commutative +-- monoids, Abelian groups, semirings, rings), the direct product is +-- also the coproduct, making it a biproduct. +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Algebra +open import Algebra.Lattice +import Algebra.Construct.DirectProduct as DirectProduct +open import Data.Product +open import Data.Product.Relation.Binary.Pointwise.NonDependent +open import Level using (Level; _⊔_) + +module Algebra.Lattice.Construct.DirectProduct where + +private + variable + a b ℓ₁ ℓ₂ : Level + +------------------------------------------------------------------------ +-- Bundles + +semilattice : Semilattice a ℓ₁ → Semilattice b ℓ₂ → + Semilattice (a ⊔ b) (ℓ₁ ⊔ ℓ₂) +semilattice L M = record + { isSemilattice = record + { isBand = Band.isBand (DirectProduct.band L.band M.band) + ; comm = λ x y → (L.comm , M.comm) <*> x <*> y + } + } where module L = Semilattice L; module M = Semilattice M diff --git a/src/Algebra/Lattice/Construct/LiftedChoice.agda b/src/Algebra/Lattice/Construct/LiftedChoice.agda new file mode 100644 index 0000000000..0183d009cc --- /dev/null +++ b/src/Algebra/Lattice/Construct/LiftedChoice.agda @@ -0,0 +1,44 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Choosing between elements based on the result of applying a function +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Algebra +open import Algebra.Lattice +open import Algebra.Construct.LiftedChoice +open import Relation.Binary +open import Level using (Level) + +module Algebra.Lattice.Construct.LiftedChoice where + +private + variable + a b p ℓ : Level + A : Set a + B : Set b + +------------------------------------------------------------------------ +-- Structures + +module _ {_≈_ : Rel B ℓ} {_∙_ : Op₂ B} + (∙-isSelectiveMagma : IsSelectiveMagma _≈_ _∙_) + {_≈′_ : Rel A ℓ} {f : A → B} + (f-injective : ∀ {x y} → f x ≈ f y → x ≈′ y) + (f-cong : f Preserves _≈′_ ⟶ _≈_) + (≈′-isEquivalence : IsEquivalence _≈′_) + where + + open IsSelectiveMagma ∙-isSelectiveMagma renaming (sel to ∙-sel) + + private + _◦_ = Lift _≈_ _∙_ ∙-sel f + + isSemilattice : Associative _≈_ _∙_ → Commutative _≈_ _∙_ → + IsSemilattice _≈′_ _◦_ + isSemilattice ∙-assoc ∙-comm = record + { isBand = isBand ∙-isSelectiveMagma f-injective f-cong ≈′-isEquivalence ∙-assoc + ; comm = comm ∙-isSelectiveMagma (λ {x} → f-injective {x}) ∙-comm + } diff --git a/src/Algebra/Lattice/Construct/NaturalChoice/MaxOp.agda b/src/Algebra/Lattice/Construct/NaturalChoice/MaxOp.agda new file mode 100644 index 0000000000..12cc7cf67e --- /dev/null +++ b/src/Algebra/Lattice/Construct/NaturalChoice/MaxOp.agda @@ -0,0 +1,26 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of a max operator derived from a spec over a total +-- preorder. +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Construct.NaturalChoice.Base +import Algebra.Lattice.Construct.NaturalChoice.MinOp as MinOp +open import Relation.Binary + +module Algebra.Lattice.Construct.NaturalChoice.MaxOp + {a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (maxOp : MaxOperator O) + where + +private + module Min = MinOp (MaxOp⇒MinOp maxOp) + +open Min public + using () + renaming + ( ⊓-isSemilattice to ⊔-isSemilattice + ; ⊓-semilattice to ⊔-semilattice + ) diff --git a/src/Algebra/Lattice/Construct/NaturalChoice/MinMaxOp.agda b/src/Algebra/Lattice/Construct/NaturalChoice/MinMaxOp.agda new file mode 100644 index 0000000000..9c1d03a9e8 --- /dev/null +++ b/src/Algebra/Lattice/Construct/NaturalChoice/MinMaxOp.agda @@ -0,0 +1,95 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of min and max operators specified over a total preorder. +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Lattice.Bundles +open import Algebra.Construct.NaturalChoice.Base +open import Relation.Binary + +module Algebra.Lattice.Construct.NaturalChoice.MinMaxOp + {a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} + (minOp : MinOperator O) + (maxOp : MaxOperator O) + where + +open TotalPreorder O +open MinOperator minOp +open MaxOperator maxOp + +open import Algebra.Lattice.Structures _≈_ +open import Algebra.Construct.NaturalChoice.MinMaxOp minOp maxOp +open import Relation.Binary.Reasoning.Preorder preorder + +------------------------------------------------------------------------ +-- Re-export properties of individual operators + +open import Algebra.Lattice.Construct.NaturalChoice.MinOp minOp public +open import Algebra.Lattice.Construct.NaturalChoice.MaxOp maxOp public + +------------------------------------------------------------------------ +-- Structures + +⊔-⊓-isLattice : IsLattice _⊔_ _⊓_ +⊔-⊓-isLattice = record + { isEquivalence = isEquivalence + ; ∨-comm = ⊔-comm + ; ∨-assoc = ⊔-assoc + ; ∨-cong = ⊔-cong + ; ∧-comm = ⊓-comm + ; ∧-assoc = ⊓-assoc + ; ∧-cong = ⊓-cong + ; absorptive = ⊔-⊓-absorptive + } + +⊓-⊔-isLattice : IsLattice _⊓_ _⊔_ +⊓-⊔-isLattice = record + { isEquivalence = isEquivalence + ; ∨-comm = ⊓-comm + ; ∨-assoc = ⊓-assoc + ; ∨-cong = ⊓-cong + ; ∧-comm = ⊔-comm + ; ∧-assoc = ⊔-assoc + ; ∧-cong = ⊔-cong + ; absorptive = ⊓-⊔-absorptive + } + +⊓-⊔-isDistributiveLattice : IsDistributiveLattice _⊓_ _⊔_ +⊓-⊔-isDistributiveLattice = record + { isLattice = ⊓-⊔-isLattice + ; ∨-distrib-∧ = ⊓-distrib-⊔ + ; ∧-distrib-∨ = ⊔-distrib-⊓ + } + +⊔-⊓-isDistributiveLattice : IsDistributiveLattice _⊔_ _⊓_ +⊔-⊓-isDistributiveLattice = record + { isLattice = ⊔-⊓-isLattice + ; ∨-distrib-∧ = ⊔-distrib-⊓ + ; ∧-distrib-∨ = ⊓-distrib-⊔ + } + +------------------------------------------------------------------------ +-- Bundles + +⊔-⊓-lattice : Lattice _ _ +⊔-⊓-lattice = record + { isLattice = ⊔-⊓-isLattice + } + +⊓-⊔-lattice : Lattice _ _ +⊓-⊔-lattice = record + { isLattice = ⊓-⊔-isLattice + } + +⊔-⊓-distributiveLattice : DistributiveLattice _ _ +⊔-⊓-distributiveLattice = record + { isDistributiveLattice = ⊔-⊓-isDistributiveLattice + } + +⊓-⊔-distributiveLattice : DistributiveLattice _ _ +⊓-⊔-distributiveLattice = record + { isDistributiveLattice = ⊓-⊔-isDistributiveLattice + } diff --git a/src/Algebra/Lattice/Construct/NaturalChoice/MinOp.agda b/src/Algebra/Lattice/Construct/NaturalChoice/MinOp.agda new file mode 100644 index 0000000000..c4b9b0a78b --- /dev/null +++ b/src/Algebra/Lattice/Construct/NaturalChoice/MinOp.agda @@ -0,0 +1,39 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of a min operator derived from a spec over a total +-- preorder. +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Bundles +open import Algebra.Lattice.Bundles +open import Algebra.Construct.NaturalChoice.Base +open import Relation.Binary + +module Algebra.Lattice.Construct.NaturalChoice.MinOp + {a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (minOp : MinOperator O) where + +open TotalPreorder O +open MinOperator minOp + +open import Algebra.Lattice.Structures _≈_ +open import Algebra.Construct.NaturalChoice.MinOp minOp + +------------------------------------------------------------------------ +-- Structures + +⊓-isSemilattice : IsSemilattice _⊓_ +⊓-isSemilattice = record + { isBand = ⊓-isBand + ; comm = ⊓-comm + } + +------------------------------------------------------------------------ +-- Bundles + +⊓-semilattice : Semilattice _ _ +⊓-semilattice = record + { isSemilattice = ⊓-isSemilattice + } diff --git a/src/Algebra/Lattice/Construct/Subst/Equality.agda b/src/Algebra/Lattice/Construct/Subst/Equality.agda new file mode 100644 index 0000000000..cef0e2afc3 --- /dev/null +++ b/src/Algebra/Lattice/Construct/Subst/Equality.agda @@ -0,0 +1,69 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Substituting equalities for binary relations +------------------------------------------------------------------------ + +-- For more general transformations between algebraic lattice structures +-- see `Algebra.Lattice.Morphisms`. + +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Core using (Op₂) +open import Algebra.Definitions +open import Algebra.Lattice.Structures +import Data.Sum as Sum +open import Data.Product as Prod +open import Function.Base +open import Relation.Binary.Core + +module Algebra.Lattice.Construct.Subst.Equality + {a ℓ₁ ℓ₂} {A : Set a} {≈₁ : Rel A ℓ₁} {≈₂ : Rel A ℓ₂} + (equiv@(to , from) : ≈₁ ⇔ ≈₂) + where + +open import Algebra.Construct.Subst.Equality equiv +open import Relation.Binary.Construct.Subst.Equality equiv + +private + variable + ∧ ∨ : Op₂ A + +------------------------------------------------------------------------ +-- Structures + +isSemilattice : IsSemilattice ≈₁ ∧ → IsSemilattice ≈₂ ∧ +isSemilattice S = record + { isBand = isBand S.isBand + ; comm = comm S.comm + } where module S = IsSemilattice S + +isLattice : IsLattice ≈₁ ∨ ∧ → IsLattice ≈₂ ∨ ∧ +isLattice {∨} {∧} S = record + { isEquivalence = isEquivalence S.isEquivalence + ; ∨-comm = comm S.∨-comm + ; ∨-assoc = assoc {∨} S.∨-assoc + ; ∨-cong = cong₂ S.∨-cong + ; ∧-comm = comm S.∧-comm + ; ∧-assoc = assoc {∧} S.∧-assoc + ; ∧-cong = cong₂ S.∧-cong + ; absorptive = absorptive {∨} {∧} S.absorptive + } where module S = IsLattice S + +isDistributiveLattice : IsDistributiveLattice ≈₁ ∨ ∧ → + IsDistributiveLattice ≈₂ ∨ ∧ +isDistributiveLattice {∨} {∧} S = record + { isLattice = isLattice S.isLattice + ; ∨-distrib-∧ = distrib {∨} {∧} S.∨-distrib-∧ + ; ∧-distrib-∨ = distrib {∧} {∨} S.∧-distrib-∨ + } where module S = IsDistributiveLattice S + +isBooleanAlgebra : ∀ {¬ ⊤ ⊥} → + IsBooleanAlgebra ≈₁ ∨ ∧ ¬ ⊤ ⊥ → + IsBooleanAlgebra ≈₂ ∨ ∧ ¬ ⊤ ⊥ +isBooleanAlgebra {∨} {∧} S = record + { isDistributiveLattice = isDistributiveLattice S.isDistributiveLattice + ; ∨-complement = inverse {_} {∨} S.∨-complement + ; ∧-complement = inverse {_} {∧} S.∧-complement + ; ¬-cong = cong₁ S.¬-cong + } where module S = IsBooleanAlgebra S diff --git a/src/Algebra/Lattice/Construct/Zero.agda b/src/Algebra/Lattice/Construct/Zero.agda new file mode 100644 index 0000000000..90a20c8875 --- /dev/null +++ b/src/Algebra/Lattice/Construct/Zero.agda @@ -0,0 +1,27 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Instances of algebraic lattice structures where the carrier is ⊤. +-- In mathematics, this is usually called 0. +-- +-- From monoids up, these are are zero-objects – i.e, both the initial +-- and the terminal object in the relevant category. +-- For structures without an identity element, we can't necessarily +-- produce a homomorphism out of 0, because there is an instance of such +-- a structure with an empty Carrier. +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) + +module Algebra.Lattice.Construct.Zero {c ℓ : Level} where + +open import Algebra.Lattice.Bundles +open import Data.Unit.Polymorphic + +------------------------------------------------------------------------ +-- Bundles + +semilattice : Semilattice c ℓ +semilattice = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } diff --git a/src/Algebra/Lattice/Morphism.agda b/src/Algebra/Lattice/Morphism.agda new file mode 100644 index 0000000000..35583a29fe --- /dev/null +++ b/src/Algebra/Lattice/Morphism.agda @@ -0,0 +1,15 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Morphisms between algebraic lattice structures +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Algebra.Lattice.Morphism where + +------------------------------------------------------------------------ +-- Re-export + +open import Algebra.Morphism.Definitions public +open import Algebra.Lattice.Morphism.Structures public diff --git a/src/Algebra/Lattice/Morphism/Construct/Composition.agda b/src/Algebra/Lattice/Morphism/Construct/Composition.agda new file mode 100644 index 0000000000..a594a6380d --- /dev/null +++ b/src/Algebra/Lattice/Morphism/Construct/Composition.agda @@ -0,0 +1,61 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The composition of morphisms between algebraic lattice structures. +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +module Algebra.Lattice.Morphism.Construct.Composition where + +open import Algebra.Lattice.Bundles +open import Algebra.Lattice.Morphism.Structures +open import Function.Base using (_∘_) +import Function.Construct.Composition as Func +open import Level using (Level) +open import Relation.Binary.Morphism.Construct.Composition +open import Relation.Binary.Definitions using (Transitive) + +private + variable + a b c ℓ₁ ℓ₂ ℓ₃ : Level + +------------------------------------------------------------------------ +-- Lattices + +module _ {L₁ : RawLattice a ℓ₁} + {L₂ : RawLattice b ℓ₂} + {L₃ : RawLattice c ℓ₃} + (open RawLattice) + (≈₃-trans : Transitive (_≈_ L₃)) + {f : Carrier L₁ → Carrier L₂} + {g : Carrier L₂ → Carrier L₃} + where + + isLatticeHomomorphism + : IsLatticeHomomorphism L₁ L₂ f + → IsLatticeHomomorphism L₂ L₃ g + → IsLatticeHomomorphism L₁ L₃ (g ∘ f) + isLatticeHomomorphism f-homo g-homo = record + { isRelHomomorphism = isRelHomomorphism F.isRelHomomorphism G.isRelHomomorphism + ; ∧-homo = λ x y → ≈₃-trans (G.⟦⟧-cong (F.∧-homo x y)) (G.∧-homo (f x) (f y)) + ; ∨-homo = λ x y → ≈₃-trans (G.⟦⟧-cong (F.∨-homo x y)) (G.∨-homo (f x) (f y)) + } where module F = IsLatticeHomomorphism f-homo; module G = IsLatticeHomomorphism g-homo + + isLatticeMonomorphism + : IsLatticeMonomorphism L₁ L₂ f + → IsLatticeMonomorphism L₂ L₃ g + → IsLatticeMonomorphism L₁ L₃ (g ∘ f) + isLatticeMonomorphism f-mono g-mono = record + { isLatticeHomomorphism = isLatticeHomomorphism F.isLatticeHomomorphism G.isLatticeHomomorphism + ; injective = F.injective ∘ G.injective + } where module F = IsLatticeMonomorphism f-mono; module G = IsLatticeMonomorphism g-mono + + isLatticeIsomorphism + : IsLatticeIsomorphism L₁ L₂ f + → IsLatticeIsomorphism L₂ L₃ g + → IsLatticeIsomorphism L₁ L₃ (g ∘ f) + isLatticeIsomorphism f-iso g-iso = record + { isLatticeMonomorphism = isLatticeMonomorphism F.isLatticeMonomorphism G.isLatticeMonomorphism + ; surjective = Func.surjective (_≈_ L₁) _ _ ≈₃-trans G.⟦⟧-cong F.surjective G.surjective + } where module F = IsLatticeIsomorphism f-iso; module G = IsLatticeIsomorphism g-iso diff --git a/src/Algebra/Lattice/Morphism/Construct/Identity.agda b/src/Algebra/Lattice/Morphism/Construct/Identity.agda new file mode 100644 index 0000000000..23a8ed0425 --- /dev/null +++ b/src/Algebra/Lattice/Morphism/Construct/Identity.agda @@ -0,0 +1,44 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The identity morphism for algebraic lattice structures +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +module Algebra.Lattice.Morphism.Construct.Identity where + +open import Algebra.Lattice.Bundles +open import Algebra.Lattice.Morphism.Structures + using ( module LatticeMorphisms ) +open import Data.Product using (_,_) +open import Function.Base using (id) +open import Level using (Level) +open import Relation.Binary.Morphism.Construct.Identity using (isRelHomomorphism) +open import Relation.Binary.Definitions using (Reflexive) + +private + variable + c ℓ : Level + +module _ (L : RawLattice c ℓ) (open RawLattice L) (refl : Reflexive _≈_) where + open LatticeMorphisms L L + + isLatticeHomomorphism : IsLatticeHomomorphism id + isLatticeHomomorphism = record + { isRelHomomorphism = isRelHomomorphism _ + ; ∧-homo = λ _ _ → refl + ; ∨-homo = λ _ _ → refl + } + + isLatticeMonomorphism : IsLatticeMonomorphism id + isLatticeMonomorphism = record + { isLatticeHomomorphism = isLatticeHomomorphism + ; injective = id + } + + isLatticeIsomorphism : IsLatticeIsomorphism id + isLatticeIsomorphism = record + { isLatticeMonomorphism = isLatticeMonomorphism + ; surjective = _, refl + } diff --git a/src/Algebra/Morphism/LatticeMonomorphism.agda b/src/Algebra/Lattice/Morphism/LatticeMonomorphism.agda similarity index 87% rename from src/Algebra/Morphism/LatticeMonomorphism.agda rename to src/Algebra/Lattice/Morphism/LatticeMonomorphism.agda index 60db102c7b..53bbe8c55f 100644 --- a/src/Algebra/Morphism/LatticeMonomorphism.agda +++ b/src/Algebra/Lattice/Morphism/LatticeMonomorphism.agda @@ -9,17 +9,18 @@ {-# OPTIONS --without-K --safe #-} -open import Algebra.Structures -open import Algebra.Definitions -open import Algebra.Bundles -open import Algebra.Morphism.Structures -import Relation.Binary.Morphism.RelMonomorphism as RelMonomorphisms +open import Algebra +open import Algebra.Lattice +open import Algebra.Lattice.Morphism.Structures +import Algebra.Consequences.Setoid as Consequences import Algebra.Morphism.MagmaMonomorphism as MagmaMonomorphisms -import Algebra.Properties.Lattice as LatticeProperties -open import Data.Product using (_,_) +import Algebra.Lattice.Properties.Lattice as LatticeProperties +open import Data.Product using (_,_; map) +open import Relation.Binary +import Relation.Binary.Morphism.RelMonomorphism as RelMonomorphisms import Relation.Binary.Reasoning.Setoid as SetoidReasoning -module Algebra.Morphism.LatticeMonomorphism +module Algebra.Lattice.Morphism.LatticeMonomorphism {a b ℓ₁ ℓ₂} {L₁ : RawLattice a ℓ₁} {L₂ : RawLattice b ℓ₂} {⟦_⟧} (isLatticeMonomorphism : IsLatticeMonomorphism L₁ L₂ ⟦_⟧) where @@ -68,7 +69,11 @@ module _ (⊔-⊓-isLattice : IsLattice _≈₂_ _⊔_ _⊓_) where ; ∨-absorbs-∧ to ⊔-absorbs-⊓ ; ∧-absorbs-∨ to ⊓-absorbs-⊔ ) - open SetoidReasoning (record { isEquivalence = isEquivalence }) + + setoid : Setoid b ℓ₂ + setoid = record { isEquivalence = isEquivalence } + + open SetoidReasoning setoid ∨-absorbs-∧ : _Absorbs_ _≈₁_ _∨_ _∧_ ∨-absorbs-∧ x y = injective (begin @@ -112,8 +117,8 @@ isLattice isLattice = record isDistributiveLattice : IsDistributiveLattice _≈₂_ _⊔_ _⊓_ → IsDistributiveLattice _≈₁_ _∨_ _∧_ -isDistributiveLattice isDL = record - { isLattice = isLattice L.isLattice - ; ∨-distribʳ-∧ = distribʳ L.isLattice L.∨-distribʳ-∧ - } where module L = IsDistributiveLattice isDL +isDistributiveLattice isDL = isDistributiveLatticeʳʲᵐ (record + { isLattice = isLattice L.isLattice + ; ∨-distribʳ-∧ = distribʳ L.isLattice L.∨-distribʳ-∧ + }) where module L = IsDistributiveLattice isDL diff --git a/src/Algebra/Lattice/Morphism/Structures.agda b/src/Algebra/Lattice/Morphism/Structures.agda new file mode 100644 index 0000000000..5f45c6dfd6 --- /dev/null +++ b/src/Algebra/Lattice/Morphism/Structures.agda @@ -0,0 +1,119 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Morphisms between algebraic lattice structures +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Core +open import Algebra.Bundles +open import Algebra.Morphism +open import Algebra.Lattice.Bundles +import Algebra.Morphism.Definitions as MorphismDefinitions +open import Level using (Level; _⊔_) +import Function.Definitions as FunctionDefinitions +open import Relation.Binary.Morphism.Structures +open import Relation.Binary.Core + +module Algebra.Lattice.Morphism.Structures where + +private + variable + a b ℓ₁ ℓ₂ : Level + +------------------------------------------------------------------------ +-- Morphisms over lattice-like structures +------------------------------------------------------------------------ + +module LatticeMorphisms (L₁ : RawLattice a ℓ₁) (L₂ : RawLattice b ℓ₂) where + + open RawLattice L₁ renaming + ( Carrier to A; _≈_ to _≈₁_ + ; _∧_ to _∧₁_; _∨_ to _∨₁_ + ; ∧-rawMagma to ∧-rawMagma₁ + ; ∨-rawMagma to ∨-rawMagma₁) + + open RawLattice L₂ renaming + ( Carrier to B; _≈_ to _≈₂_ + ; _∧_ to _∧₂_; _∨_ to _∨₂_ + ; ∧-rawMagma to ∧-rawMagma₂ + ; ∨-rawMagma to ∨-rawMagma₂) + + module ∨ = MagmaMorphisms ∨-rawMagma₁ ∨-rawMagma₂ + module ∧ = MagmaMorphisms ∧-rawMagma₁ ∧-rawMagma₂ + + open MorphismDefinitions A B _≈₂_ + open FunctionDefinitions _≈₁_ _≈₂_ + + + record IsLatticeHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + field + isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧ + ∧-homo : Homomorphic₂ ⟦_⟧ _∧₁_ _∧₂_ + ∨-homo : Homomorphic₂ ⟦_⟧ _∨₁_ _∨₂_ + + open IsRelHomomorphism isRelHomomorphism public + renaming (cong to ⟦⟧-cong) + + ∧-isMagmaHomomorphism : ∧.IsMagmaHomomorphism ⟦_⟧ + ∧-isMagmaHomomorphism = record + { isRelHomomorphism = isRelHomomorphism + ; homo = ∧-homo + } + + ∨-isMagmaHomomorphism : ∨.IsMagmaHomomorphism ⟦_⟧ + ∨-isMagmaHomomorphism = record + { isRelHomomorphism = isRelHomomorphism + ; homo = ∨-homo + } + + record IsLatticeMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + field + isLatticeHomomorphism : IsLatticeHomomorphism ⟦_⟧ + injective : Injective ⟦_⟧ + + open IsLatticeHomomorphism isLatticeHomomorphism public + + ∨-isMagmaMonomorphism : ∨.IsMagmaMonomorphism ⟦_⟧ + ∨-isMagmaMonomorphism = record + { isMagmaHomomorphism = ∨-isMagmaHomomorphism + ; injective = injective + } + + ∧-isMagmaMonomorphism : ∧.IsMagmaMonomorphism ⟦_⟧ + ∧-isMagmaMonomorphism = record + { isMagmaHomomorphism = ∧-isMagmaHomomorphism + ; injective = injective + } + + open ∧.IsMagmaMonomorphism ∧-isMagmaMonomorphism public + using (isRelMonomorphism) + + + record IsLatticeIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where + field + isLatticeMonomorphism : IsLatticeMonomorphism ⟦_⟧ + surjective : Surjective ⟦_⟧ + + open IsLatticeMonomorphism isLatticeMonomorphism public + + ∨-isMagmaIsomorphism : ∨.IsMagmaIsomorphism ⟦_⟧ + ∨-isMagmaIsomorphism = record + { isMagmaMonomorphism = ∨-isMagmaMonomorphism + ; surjective = surjective + } + + ∧-isMagmaIsomorphism : ∧.IsMagmaIsomorphism ⟦_⟧ + ∧-isMagmaIsomorphism = record + { isMagmaMonomorphism = ∧-isMagmaMonomorphism + ; surjective = surjective + } + + open ∧.IsMagmaIsomorphism ∧-isMagmaIsomorphism public + using (isRelIsomorphism) + +------------------------------------------------------------------------ +-- Re-export contents of modules publicly + +open LatticeMorphisms public diff --git a/src/Algebra/Lattice/Properties/BooleanAlgebra.agda b/src/Algebra/Lattice/Properties/BooleanAlgebra.agda new file mode 100644 index 0000000000..3c8717a217 --- /dev/null +++ b/src/Algebra/Lattice/Properties/BooleanAlgebra.agda @@ -0,0 +1,560 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Some derivable properties of Boolean algebras +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +-- Disabled to prevent warnings from deprecated names +{-# OPTIONS --warn=noUserWarning #-} + +open import Algebra.Lattice.Bundles + +module Algebra.Lattice.Properties.BooleanAlgebra + {b₁ b₂} (B : BooleanAlgebra b₁ b₂) + where + +open BooleanAlgebra B + +import Algebra.Properties.DistributiveLattice as DistribLatticeProperties +open import Algebra.Core +open import Algebra.Structures _≈_ +open import Algebra.Definitions _≈_ +open import Algebra.Consequences.Setoid setoid +open import Algebra.Bundles +open import Algebra.Lattice.Structures _≈_ +open import Relation.Binary.Reasoning.Setoid setoid +open import Relation.Binary +open import Function.Base +open import Function.Equality using (_⟨$⟩_) +open import Function.Equivalence using (_⇔_; module Equivalence) +open import Data.Product using (_,_) + +------------------------------------------------------------------------ +-- Export properties from distributive lattices + +open DistribLatticeProperties distributiveLattice public + hiding (replace-equality) + +------------------------------------------------------------------------ +-- The dual construction is also a boolean algebra + +∧-∨-isBooleanAlgebra : IsBooleanAlgebra _∧_ _∨_ ¬_ ⊥ ⊤ +∧-∨-isBooleanAlgebra = record + { isDistributiveLattice = ∧-∨-isDistributiveLattice + ; ∨-complement = ∧-complement + ; ∧-complement = ∨-complement + ; ¬-cong = ¬-cong + } + +∧-∨-booleanAlgebra : BooleanAlgebra _ _ +∧-∨-booleanAlgebra = record + { isBooleanAlgebra = ∧-∨-isBooleanAlgebra + } + +------------------------------------------------------------------------ +-- (∨, ∧, ⊥, ⊤) and (∧, ∨, ⊤, ⊥) are commutative semirings + +∧-identityʳ : RightIdentity ⊤ _∧_ +∧-identityʳ x = begin + x ∧ ⊤ ≈⟨ ∧-congˡ (sym (∨-complementʳ _)) ⟩ + x ∧ (x ∨ ¬ x) ≈⟨ ∧-absorbs-∨ _ _ ⟩ + x ∎ + +∧-identityˡ : LeftIdentity ⊤ _∧_ +∧-identityˡ = comm+idʳ⇒idˡ ∧-comm ∧-identityʳ + +∧-identity : Identity ⊤ _∧_ +∧-identity = ∧-identityˡ , ∧-identityʳ + +∨-identityʳ : RightIdentity ⊥ _∨_ +∨-identityʳ x = begin + x ∨ ⊥ ≈⟨ ∨-congˡ $ sym (∧-complementʳ _) ⟩ + x ∨ x ∧ ¬ x ≈⟨ ∨-absorbs-∧ _ _ ⟩ + x ∎ + +∨-identityˡ : LeftIdentity ⊥ _∨_ +∨-identityˡ = comm+idʳ⇒idˡ ∨-comm ∨-identityʳ + +∨-identity : Identity ⊥ _∨_ +∨-identity = ∨-identityˡ , ∨-identityʳ + +∧-zeroʳ : RightZero ⊥ _∧_ +∧-zeroʳ x = begin + x ∧ ⊥ ≈˘⟨ ∧-congˡ (∧-complementʳ x) ⟩ + x ∧ x ∧ ¬ x ≈˘⟨ ∧-assoc x x (¬ x) ⟩ + (x ∧ x) ∧ ¬ x ≈⟨ ∧-congʳ (∧-idem x) ⟩ + x ∧ ¬ x ≈⟨ ∧-complementʳ x ⟩ + ⊥ ∎ + +∧-zeroˡ : LeftZero ⊥ _∧_ +∧-zeroˡ = comm+zeʳ⇒zeˡ ∧-comm ∧-zeroʳ + +∧-zero : Zero ⊥ _∧_ +∧-zero = ∧-zeroˡ , ∧-zeroʳ + +∨-zeroʳ : ∀ x → x ∨ ⊤ ≈ ⊤ +∨-zeroʳ x = begin + x ∨ ⊤ ≈˘⟨ ∨-congˡ (∨-complementʳ x) ⟩ + x ∨ x ∨ ¬ x ≈˘⟨ ∨-assoc x x (¬ x) ⟩ + (x ∨ x) ∨ ¬ x ≈⟨ ∨-congʳ (∨-idem x) ⟩ + x ∨ ¬ x ≈⟨ ∨-complementʳ x ⟩ + ⊤ ∎ + +∨-zeroˡ : LeftZero ⊤ _∨_ +∨-zeroˡ = comm+zeʳ⇒zeˡ ∨-comm ∨-zeroʳ + +∨-zero : Zero ⊤ _∨_ +∨-zero = ∨-zeroˡ , ∨-zeroʳ + +∨-⊥-isMonoid : IsMonoid _∨_ ⊥ +∨-⊥-isMonoid = record + { isSemigroup = ∨-isSemigroup + ; identity = ∨-identity + } + +∧-⊤-isMonoid : IsMonoid _∧_ ⊤ +∧-⊤-isMonoid = record + { isSemigroup = ∧-isSemigroup + ; identity = ∧-identity + } + +∨-⊥-isCommutativeMonoid : IsCommutativeMonoid _∨_ ⊥ +∨-⊥-isCommutativeMonoid = record + { isMonoid = ∨-⊥-isMonoid + ; comm = ∨-comm + } + +∧-⊤-isCommutativeMonoid : IsCommutativeMonoid _∧_ ⊤ +∧-⊤-isCommutativeMonoid = record + { isMonoid = ∧-⊤-isMonoid + ; comm = ∧-comm + } + +∨-∧-isSemiring : IsSemiring _∨_ _∧_ ⊥ ⊤ +∨-∧-isSemiring = record + { isSemiringWithoutAnnihilatingZero = record + { +-isCommutativeMonoid = ∨-⊥-isCommutativeMonoid + ; *-isMonoid = ∧-⊤-isMonoid + ; distrib = ∧-∨-distrib + } + ; zero = ∧-zero + } + +∧-∨-isSemiring : IsSemiring _∧_ _∨_ ⊤ ⊥ +∧-∨-isSemiring = record + { isSemiringWithoutAnnihilatingZero = record + { +-isCommutativeMonoid = ∧-⊤-isCommutativeMonoid + ; *-isMonoid = ∨-⊥-isMonoid + ; distrib = ∨-∧-distrib + } + ; zero = ∨-zero + } + +∨-∧-isCommutativeSemiring : IsCommutativeSemiring _∨_ _∧_ ⊥ ⊤ +∨-∧-isCommutativeSemiring = record + { isSemiring = ∨-∧-isSemiring + ; *-comm = ∧-comm + } + +∧-∨-isCommutativeSemiring : IsCommutativeSemiring _∧_ _∨_ ⊤ ⊥ +∧-∨-isCommutativeSemiring = record + { isSemiring = ∧-∨-isSemiring + ; *-comm = ∨-comm + } + +∨-∧-commutativeSemiring : CommutativeSemiring _ _ +∨-∧-commutativeSemiring = record + { isCommutativeSemiring = ∨-∧-isCommutativeSemiring + } + +∧-∨-commutativeSemiring : CommutativeSemiring _ _ +∧-∨-commutativeSemiring = record + { isCommutativeSemiring = ∧-∨-isCommutativeSemiring + } + +------------------------------------------------------------------------ +-- Some other properties + +-- I took the statement of this lemma (called Uniqueness of +-- Complements) from some course notes, "Boolean Algebra", written +-- by Gert Smolka. + +private + lemma : ∀ x y → x ∧ y ≈ ⊥ → x ∨ y ≈ ⊤ → ¬ x ≈ y + lemma x y x∧y=⊥ x∨y=⊤ = begin + ¬ x ≈˘⟨ ∧-identityʳ _ ⟩ + ¬ x ∧ ⊤ ≈˘⟨ ∧-congˡ x∨y=⊤ ⟩ + ¬ x ∧ (x ∨ y) ≈⟨ ∧-∨-distribˡ _ _ _ ⟩ + ¬ x ∧ x ∨ ¬ x ∧ y ≈⟨ ∨-congʳ $ ∧-complementˡ _ ⟩ + ⊥ ∨ ¬ x ∧ y ≈˘⟨ ∨-congʳ x∧y=⊥ ⟩ + x ∧ y ∨ ¬ x ∧ y ≈˘⟨ ∧-∨-distribʳ _ _ _ ⟩ + (x ∨ ¬ x) ∧ y ≈⟨ ∧-congʳ $ ∨-complementʳ _ ⟩ + ⊤ ∧ y ≈⟨ ∧-identityˡ _ ⟩ + y ∎ + +⊥≉⊤ : ¬ ⊥ ≈ ⊤ +⊥≉⊤ = lemma ⊥ ⊤ (∧-identityʳ _) (∨-zeroʳ _) + +⊤≉⊥ : ¬ ⊤ ≈ ⊥ +⊤≉⊥ = lemma ⊤ ⊥ (∧-zeroʳ _) (∨-identityʳ _) + +¬-involutive : Involutive ¬_ +¬-involutive x = lemma (¬ x) x (∧-complementˡ _) (∨-complementˡ _) + +deMorgan₁ : ∀ x y → ¬ (x ∧ y) ≈ ¬ x ∨ ¬ y +deMorgan₁ x y = lemma (x ∧ y) (¬ x ∨ ¬ y) lem₁ lem₂ + where + lem₁ = begin + (x ∧ y) ∧ (¬ x ∨ ¬ y) ≈⟨ ∧-∨-distribˡ _ _ _ ⟩ + (x ∧ y) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y ≈⟨ ∨-congʳ $ ∧-congʳ $ ∧-comm _ _ ⟩ + (y ∧ x) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y ≈⟨ ∧-assoc _ _ _ ⟨ ∨-cong ⟩ ∧-assoc _ _ _ ⟩ + y ∧ (x ∧ ¬ x) ∨ x ∧ (y ∧ ¬ y) ≈⟨ (∧-congˡ $ ∧-complementʳ _) ⟨ ∨-cong ⟩ + (∧-congˡ $ ∧-complementʳ _) ⟩ + (y ∧ ⊥) ∨ (x ∧ ⊥) ≈⟨ ∧-zeroʳ _ ⟨ ∨-cong ⟩ ∧-zeroʳ _ ⟩ + ⊥ ∨ ⊥ ≈⟨ ∨-identityʳ _ ⟩ + ⊥ ∎ + + lem₃ = begin + (x ∧ y) ∨ ¬ x ≈⟨ ∨-distribʳ-∧ _ _ _ ⟩ + (x ∨ ¬ x) ∧ (y ∨ ¬ x) ≈⟨ ∧-congʳ $ ∨-complementʳ _ ⟩ + ⊤ ∧ (y ∨ ¬ x) ≈⟨ ∧-identityˡ _ ⟩ + y ∨ ¬ x ≈⟨ ∨-comm _ _ ⟩ + ¬ x ∨ y ∎ + + lem₂ = begin + (x ∧ y) ∨ (¬ x ∨ ¬ y) ≈˘⟨ ∨-assoc _ _ _ ⟩ + ((x ∧ y) ∨ ¬ x) ∨ ¬ y ≈⟨ ∨-congʳ lem₃ ⟩ + (¬ x ∨ y) ∨ ¬ y ≈⟨ ∨-assoc _ _ _ ⟩ + ¬ x ∨ (y ∨ ¬ y) ≈⟨ ∨-congˡ $ ∨-complementʳ _ ⟩ + ¬ x ∨ ⊤ ≈⟨ ∨-zeroʳ _ ⟩ + ⊤ ∎ + +deMorgan₂ : ∀ x y → ¬ (x ∨ y) ≈ ¬ x ∧ ¬ y +deMorgan₂ x y = begin + ¬ (x ∨ y) ≈˘⟨ ¬-cong $ ((¬-involutive _) ⟨ ∨-cong ⟩ (¬-involutive _)) ⟩ + ¬ (¬ ¬ x ∨ ¬ ¬ y) ≈˘⟨ ¬-cong $ deMorgan₁ _ _ ⟩ + ¬ ¬ (¬ x ∧ ¬ y) ≈⟨ ¬-involutive _ ⟩ + ¬ x ∧ ¬ y ∎ + +------------------------------------------------------------------------ +-- (⊕, ∧, id, ⊥, ⊤) is a commutative ring + +-- This construction is parameterised over the definition of xor. + +module XorRing + (xor : Op₂ Carrier) + (⊕-def : ∀ x y → xor x y ≈ (x ∨ y) ∧ ¬ (x ∧ y)) + where + + private + infixl 6 _⊕_ + + _⊕_ : Op₂ Carrier + _⊕_ = xor + + helper : ∀ {x y u v} → x ≈ y → u ≈ v → x ∧ ¬ u ≈ y ∧ ¬ v + helper x≈y u≈v = x≈y ⟨ ∧-cong ⟩ ¬-cong u≈v + + ⊕-cong : Congruent₂ _⊕_ + ⊕-cong {x} {y} {u} {v} x≈y u≈v = begin + x ⊕ u ≈⟨ ⊕-def _ _ ⟩ + (x ∨ u) ∧ ¬ (x ∧ u) ≈⟨ helper (x≈y ⟨ ∨-cong ⟩ u≈v) + (x≈y ⟨ ∧-cong ⟩ u≈v) ⟩ + (y ∨ v) ∧ ¬ (y ∧ v) ≈˘⟨ ⊕-def _ _ ⟩ + y ⊕ v ∎ + + ⊕-comm : Commutative _⊕_ + ⊕-comm x y = begin + x ⊕ y ≈⟨ ⊕-def _ _ ⟩ + (x ∨ y) ∧ ¬ (x ∧ y) ≈⟨ helper (∨-comm _ _) (∧-comm _ _) ⟩ + (y ∨ x) ∧ ¬ (y ∧ x) ≈˘⟨ ⊕-def _ _ ⟩ + y ⊕ x ∎ + + ¬-distribˡ-⊕ : ∀ x y → ¬ (x ⊕ y) ≈ ¬ x ⊕ y + ¬-distribˡ-⊕ x y = begin + ¬ (x ⊕ y) ≈⟨ ¬-cong $ ⊕-def _ _ ⟩ + ¬ ((x ∨ y) ∧ (¬ (x ∧ y))) ≈⟨ ¬-cong (∧-∨-distribʳ _ _ _) ⟩ + ¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (x ∧ y))) ≈⟨ ¬-cong $ ∨-congˡ $ ∧-congˡ $ ¬-cong (∧-comm _ _) ⟩ + ¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (y ∧ x))) ≈⟨ ¬-cong $ lem _ _ ⟨ ∨-cong ⟩ lem _ _ ⟩ + ¬ ((x ∧ ¬ y) ∨ (y ∧ ¬ x)) ≈⟨ deMorgan₂ _ _ ⟩ + ¬ (x ∧ ¬ y) ∧ ¬ (y ∧ ¬ x) ≈⟨ ∧-congʳ $ deMorgan₁ _ _ ⟩ + (¬ x ∨ (¬ ¬ y)) ∧ ¬ (y ∧ ¬ x) ≈⟨ helper (∨-congˡ $ ¬-involutive _) (∧-comm _ _) ⟩ + (¬ x ∨ y) ∧ ¬ (¬ x ∧ y) ≈˘⟨ ⊕-def _ _ ⟩ + ¬ x ⊕ y ∎ + where + lem : ∀ x y → x ∧ ¬ (x ∧ y) ≈ x ∧ ¬ y + lem x y = begin + x ∧ ¬ (x ∧ y) ≈⟨ ∧-congˡ $ deMorgan₁ _ _ ⟩ + x ∧ (¬ x ∨ ¬ y) ≈⟨ ∧-∨-distribˡ _ _ _ ⟩ + (x ∧ ¬ x) ∨ (x ∧ ¬ y) ≈⟨ ∨-congʳ $ ∧-complementʳ _ ⟩ + ⊥ ∨ (x ∧ ¬ y) ≈⟨ ∨-identityˡ _ ⟩ + x ∧ ¬ y ∎ + + ¬-distribʳ-⊕ : ∀ x y → ¬ (x ⊕ y) ≈ x ⊕ ¬ y + ¬-distribʳ-⊕ x y = begin + ¬ (x ⊕ y) ≈⟨ ¬-cong $ ⊕-comm _ _ ⟩ + ¬ (y ⊕ x) ≈⟨ ¬-distribˡ-⊕ _ _ ⟩ + ¬ y ⊕ x ≈⟨ ⊕-comm _ _ ⟩ + x ⊕ ¬ y ∎ + + ⊕-annihilates-¬ : ∀ x y → x ⊕ y ≈ ¬ x ⊕ ¬ y + ⊕-annihilates-¬ x y = begin + x ⊕ y ≈˘⟨ ¬-involutive _ ⟩ + ¬ ¬ (x ⊕ y) ≈⟨ ¬-cong $ ¬-distribˡ-⊕ _ _ ⟩ + ¬ (¬ x ⊕ y) ≈⟨ ¬-distribʳ-⊕ _ _ ⟩ + ¬ x ⊕ ¬ y ∎ + + ⊕-identityˡ : LeftIdentity ⊥ _⊕_ + ⊕-identityˡ x = begin + ⊥ ⊕ x ≈⟨ ⊕-def _ _ ⟩ + (⊥ ∨ x) ∧ ¬ (⊥ ∧ x) ≈⟨ helper (∨-identityˡ _) (∧-zeroˡ _) ⟩ + x ∧ ¬ ⊥ ≈⟨ ∧-congˡ ⊥≉⊤ ⟩ + x ∧ ⊤ ≈⟨ ∧-identityʳ _ ⟩ + x ∎ + + ⊕-identityʳ : RightIdentity ⊥ _⊕_ + ⊕-identityʳ _ = ⊕-comm _ _ ⟨ trans ⟩ ⊕-identityˡ _ + + ⊕-identity : Identity ⊥ _⊕_ + ⊕-identity = ⊕-identityˡ , ⊕-identityʳ + + ⊕-inverseˡ : LeftInverse ⊥ id _⊕_ + ⊕-inverseˡ x = begin + x ⊕ x ≈⟨ ⊕-def _ _ ⟩ + (x ∨ x) ∧ ¬ (x ∧ x) ≈⟨ helper (∨-idem _) (∧-idem _) ⟩ + x ∧ ¬ x ≈⟨ ∧-complementʳ _ ⟩ + ⊥ ∎ + + ⊕-inverseʳ : RightInverse ⊥ id _⊕_ + ⊕-inverseʳ _ = ⊕-comm _ _ ⟨ trans ⟩ ⊕-inverseˡ _ + + ⊕-inverse : Inverse ⊥ id _⊕_ + ⊕-inverse = ⊕-inverseˡ , ⊕-inverseʳ + + ∧-distribˡ-⊕ : _∧_ DistributesOverˡ _⊕_ + ∧-distribˡ-⊕ x y z = begin + x ∧ (y ⊕ z) ≈⟨ ∧-congˡ $ ⊕-def _ _ ⟩ + x ∧ ((y ∨ z) ∧ ¬ (y ∧ z)) ≈˘⟨ ∧-assoc _ _ _ ⟩ + (x ∧ (y ∨ z)) ∧ ¬ (y ∧ z) ≈⟨ ∧-congˡ $ deMorgan₁ _ _ ⟩ + (x ∧ (y ∨ z)) ∧ + (¬ y ∨ ¬ z) ≈˘⟨ ∨-identityˡ _ ⟩ + ⊥ ∨ + ((x ∧ (y ∨ z)) ∧ + (¬ y ∨ ¬ z)) ≈⟨ ∨-congʳ lem₃ ⟩ + ((x ∧ (y ∨ z)) ∧ ¬ x) ∨ + ((x ∧ (y ∨ z)) ∧ + (¬ y ∨ ¬ z)) ≈˘⟨ ∧-∨-distribˡ _ _ _ ⟩ + (x ∧ (y ∨ z)) ∧ + (¬ x ∨ (¬ y ∨ ¬ z)) ≈˘⟨ ∧-congˡ $ ∨-congˡ (deMorgan₁ _ _) ⟩ + (x ∧ (y ∨ z)) ∧ + (¬ x ∨ ¬ (y ∧ z)) ≈˘⟨ ∧-congˡ (deMorgan₁ _ _) ⟩ + (x ∧ (y ∨ z)) ∧ + ¬ (x ∧ (y ∧ z)) ≈⟨ helper refl lem₁ ⟩ + (x ∧ (y ∨ z)) ∧ + ¬ ((x ∧ y) ∧ (x ∧ z)) ≈⟨ ∧-congʳ $ ∧-∨-distribˡ _ _ _ ⟩ + ((x ∧ y) ∨ (x ∧ z)) ∧ + ¬ ((x ∧ y) ∧ (x ∧ z)) ≈˘⟨ ⊕-def _ _ ⟩ + (x ∧ y) ⊕ (x ∧ z) ∎ + where + lem₂ = begin + x ∧ (y ∧ z) ≈˘⟨ ∧-assoc _ _ _ ⟩ + (x ∧ y) ∧ z ≈⟨ ∧-congʳ $ ∧-comm _ _ ⟩ + (y ∧ x) ∧ z ≈⟨ ∧-assoc _ _ _ ⟩ + y ∧ (x ∧ z) ∎ + + lem₁ = begin + x ∧ (y ∧ z) ≈˘⟨ ∧-congʳ (∧-idem _) ⟩ + (x ∧ x) ∧ (y ∧ z) ≈⟨ ∧-assoc _ _ _ ⟩ + x ∧ (x ∧ (y ∧ z)) ≈⟨ ∧-congˡ lem₂ ⟩ + x ∧ (y ∧ (x ∧ z)) ≈˘⟨ ∧-assoc _ _ _ ⟩ + (x ∧ y) ∧ (x ∧ z) ∎ + + lem₃ = begin + ⊥ ≈˘⟨ ∧-zeroʳ _ ⟩ + (y ∨ z) ∧ ⊥ ≈˘⟨ ∧-congˡ (∧-complementʳ _) ⟩ + (y ∨ z) ∧ (x ∧ ¬ x) ≈˘⟨ ∧-assoc _ _ _ ⟩ + ((y ∨ z) ∧ x) ∧ ¬ x ≈⟨ ∧-comm _ _ ⟨ ∧-cong ⟩ refl ⟩ + (x ∧ (y ∨ z)) ∧ ¬ x ∎ + + ∧-distribʳ-⊕ : _∧_ DistributesOverʳ _⊕_ + ∧-distribʳ-⊕ = comm+distrˡ⇒distrʳ ⊕-cong ∧-comm ∧-distribˡ-⊕ + + ∧-distrib-⊕ : _∧_ DistributesOver _⊕_ + ∧-distrib-⊕ = ∧-distribˡ-⊕ , ∧-distribʳ-⊕ + + private + + lemma₂ : ∀ x y u v → + (x ∧ y) ∨ (u ∧ v) ≈ + ((x ∨ u) ∧ (y ∨ u)) ∧ + ((x ∨ v) ∧ (y ∨ v)) + lemma₂ x y u v = begin + (x ∧ y) ∨ (u ∧ v) ≈⟨ ∨-distribˡ-∧ _ _ _ ⟩ + ((x ∧ y) ∨ u) ∧ ((x ∧ y) ∨ v) ≈⟨ ∨-distribʳ-∧ _ _ _ + ⟨ ∧-cong ⟩ + ∨-distribʳ-∧ _ _ _ ⟩ + ((x ∨ u) ∧ (y ∨ u)) ∧ + ((x ∨ v) ∧ (y ∨ v)) ∎ + + ⊕-assoc : Associative _⊕_ + ⊕-assoc x y z = sym $ begin + x ⊕ (y ⊕ z) ≈⟨ refl ⟨ ⊕-cong ⟩ ⊕-def _ _ ⟩ + x ⊕ ((y ∨ z) ∧ ¬ (y ∧ z)) ≈⟨ ⊕-def _ _ ⟩ + (x ∨ ((y ∨ z) ∧ ¬ (y ∧ z))) ∧ + ¬ (x ∧ ((y ∨ z) ∧ ¬ (y ∧ z))) ≈⟨ lem₃ ⟨ ∧-cong ⟩ lem₄ ⟩ + (((x ∨ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)) ∧ + (((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z)) ≈⟨ ∧-assoc _ _ _ ⟩ + ((x ∨ y) ∨ z) ∧ + (((x ∨ ¬ y) ∨ ¬ z) ∧ + (((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z))) ≈⟨ ∧-congˡ lem₅ ⟩ + ((x ∨ y) ∨ z) ∧ + (((¬ x ∨ ¬ y) ∨ z) ∧ + (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z))) ≈˘⟨ ∧-assoc _ _ _ ⟩ + (((x ∨ y) ∨ z) ∧ ((¬ x ∨ ¬ y) ∨ z)) ∧ + (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z)) ≈⟨ lem₁ ⟨ ∧-cong ⟩ lem₂ ⟩ + (((x ∨ y) ∧ ¬ (x ∧ y)) ∨ z) ∧ + ¬ (((x ∨ y) ∧ ¬ (x ∧ y)) ∧ z) ≈˘⟨ ⊕-def _ _ ⟩ + ((x ∨ y) ∧ ¬ (x ∧ y)) ⊕ z ≈˘⟨ ⊕-def _ _ ⟨ ⊕-cong ⟩ refl ⟩ + (x ⊕ y) ⊕ z ∎ + where + lem₁ = begin + ((x ∨ y) ∨ z) ∧ ((¬ x ∨ ¬ y) ∨ z) ≈˘⟨ ∨-distribʳ-∧ _ _ _ ⟩ + ((x ∨ y) ∧ (¬ x ∨ ¬ y)) ∨ z ≈˘⟨ ∨-congʳ $ ∧-congˡ (deMorgan₁ _ _) ⟩ + ((x ∨ y) ∧ ¬ (x ∧ y)) ∨ z ∎ + + lem₂′ = begin + (x ∨ ¬ y) ∧ (¬ x ∨ y) ≈˘⟨ ∧-identityˡ _ ⟨ ∧-cong ⟩ ∧-identityʳ _ ⟩ + (⊤ ∧ (x ∨ ¬ y)) ∧ ((¬ x ∨ y) ∧ ⊤) ≈˘⟨ (∨-complementˡ _ ⟨ ∧-cong ⟩ ∨-comm _ _) + ⟨ ∧-cong ⟩ + (∧-congˡ $ ∨-complementˡ _) ⟩ + ((¬ x ∨ x) ∧ (¬ y ∨ x)) ∧ + ((¬ x ∨ y) ∧ (¬ y ∨ y)) ≈˘⟨ lemma₂ _ _ _ _ ⟩ + (¬ x ∧ ¬ y) ∨ (x ∧ y) ≈˘⟨ deMorgan₂ _ _ ⟨ ∨-cong ⟩ ¬-involutive _ ⟩ + ¬ (x ∨ y) ∨ ¬ ¬ (x ∧ y) ≈˘⟨ deMorgan₁ _ _ ⟩ + ¬ ((x ∨ y) ∧ ¬ (x ∧ y)) ∎ + + lem₂ = begin + ((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z) ≈˘⟨ ∨-distribʳ-∧ _ _ _ ⟩ + ((x ∨ ¬ y) ∧ (¬ x ∨ y)) ∨ ¬ z ≈⟨ ∨-congʳ lem₂′ ⟩ + ¬ ((x ∨ y) ∧ ¬ (x ∧ y)) ∨ ¬ z ≈˘⟨ deMorgan₁ _ _ ⟩ + ¬ (((x ∨ y) ∧ ¬ (x ∧ y)) ∧ z) ∎ + + lem₃ = begin + x ∨ ((y ∨ z) ∧ ¬ (y ∧ z)) ≈⟨ ∨-congˡ $ ∧-congˡ $ deMorgan₁ _ _ ⟩ + x ∨ ((y ∨ z) ∧ (¬ y ∨ ¬ z)) ≈⟨ ∨-∧-distribˡ _ _ _ ⟩ + (x ∨ (y ∨ z)) ∧ (x ∨ (¬ y ∨ ¬ z)) ≈˘⟨ ∨-assoc _ _ _ ⟨ ∧-cong ⟩ ∨-assoc _ _ _ ⟩ + ((x ∨ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z) ∎ + + lem₄′ = begin + ¬ ((y ∨ z) ∧ ¬ (y ∧ z)) ≈⟨ deMorgan₁ _ _ ⟩ + ¬ (y ∨ z) ∨ ¬ ¬ (y ∧ z) ≈⟨ deMorgan₂ _ _ ⟨ ∨-cong ⟩ ¬-involutive _ ⟩ + (¬ y ∧ ¬ z) ∨ (y ∧ z) ≈⟨ lemma₂ _ _ _ _ ⟩ + ((¬ y ∨ y) ∧ (¬ z ∨ y)) ∧ + ((¬ y ∨ z) ∧ (¬ z ∨ z)) ≈⟨ (∨-complementˡ _ ⟨ ∧-cong ⟩ ∨-comm _ _) + ⟨ ∧-cong ⟩ + (∧-congˡ $ ∨-complementˡ _) ⟩ + (⊤ ∧ (y ∨ ¬ z)) ∧ + ((¬ y ∨ z) ∧ ⊤) ≈⟨ ∧-identityˡ _ ⟨ ∧-cong ⟩ ∧-identityʳ _ ⟩ + (y ∨ ¬ z) ∧ (¬ y ∨ z) ∎ + + lem₄ = begin + ¬ (x ∧ ((y ∨ z) ∧ ¬ (y ∧ z))) ≈⟨ deMorgan₁ _ _ ⟩ + ¬ x ∨ ¬ ((y ∨ z) ∧ ¬ (y ∧ z)) ≈⟨ ∨-congˡ lem₄′ ⟩ + ¬ x ∨ ((y ∨ ¬ z) ∧ (¬ y ∨ z)) ≈⟨ ∨-∧-distribˡ _ _ _ ⟩ + (¬ x ∨ (y ∨ ¬ z)) ∧ + (¬ x ∨ (¬ y ∨ z)) ≈˘⟨ ∨-assoc _ _ _ ⟨ ∧-cong ⟩ ∨-assoc _ _ _ ⟩ + ((¬ x ∨ y) ∨ ¬ z) ∧ + ((¬ x ∨ ¬ y) ∨ z) ≈⟨ ∧-comm _ _ ⟩ + ((¬ x ∨ ¬ y) ∨ z) ∧ + ((¬ x ∨ y) ∨ ¬ z) ∎ + + lem₅ = begin + ((x ∨ ¬ y) ∨ ¬ z) ∧ + (((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z)) ≈˘⟨ ∧-assoc _ _ _ ⟩ + (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ ¬ y) ∨ z)) ∧ + ((¬ x ∨ y) ∨ ¬ z) ≈⟨ ∧-congʳ $ ∧-comm _ _ ⟩ + (((¬ x ∨ ¬ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)) ∧ + ((¬ x ∨ y) ∨ ¬ z) ≈⟨ ∧-assoc _ _ _ ⟩ + ((¬ x ∨ ¬ y) ∨ z) ∧ + (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z)) ∎ + + ⊕-isMagma : IsMagma _⊕_ + ⊕-isMagma = record + { isEquivalence = isEquivalence + ; ∙-cong = ⊕-cong + } + + ⊕-isSemigroup : IsSemigroup _⊕_ + ⊕-isSemigroup = record + { isMagma = ⊕-isMagma + ; assoc = ⊕-assoc + } + + ⊕-⊥-isMonoid : IsMonoid _⊕_ ⊥ + ⊕-⊥-isMonoid = record + { isSemigroup = ⊕-isSemigroup + ; identity = ⊕-identity + } + + ⊕-⊥-isGroup : IsGroup _⊕_ ⊥ id + ⊕-⊥-isGroup = record + { isMonoid = ⊕-⊥-isMonoid + ; inverse = ⊕-inverse + ; ⁻¹-cong = id + } + + ⊕-⊥-isAbelianGroup : IsAbelianGroup _⊕_ ⊥ id + ⊕-⊥-isAbelianGroup = record + { isGroup = ⊕-⊥-isGroup + ; comm = ⊕-comm + } + + ⊕-∧-isRing : IsRing _⊕_ _∧_ id ⊥ ⊤ + ⊕-∧-isRing = record + { +-isAbelianGroup = ⊕-⊥-isAbelianGroup + ; *-isMonoid = ∧-⊤-isMonoid + ; distrib = ∧-distrib-⊕ + ; zero = ∧-zero + } + + ⊕-∧-isCommutativeRing : IsCommutativeRing _⊕_ _∧_ id ⊥ ⊤ + ⊕-∧-isCommutativeRing = record + { isRing = ⊕-∧-isRing + ; *-comm = ∧-comm + } + + ⊕-∧-commutativeRing : CommutativeRing _ _ + ⊕-∧-commutativeRing = record + { isCommutativeRing = ⊕-∧-isCommutativeRing + } + + ⊕-¬-distribˡ = ¬-distribˡ-⊕ + {-# WARNING_ON_USAGE ⊕-¬-distribˡ + "Warning: ⊕-¬-distribˡ was deprecated in v1.1. + Please use ¬-distribˡ-⊕ instead." + #-} + ⊕-¬-distribʳ = ¬-distribʳ-⊕ + {-# WARNING_ON_USAGE ⊕-¬-distribʳ + "Warning: ⊕-¬-distribʳ was deprecated in v1.1. + Please use ¬-distribʳ-⊕ instead." + #-} + isCommutativeRing = ⊕-∧-isCommutativeRing + {-# WARNING_ON_USAGE isCommutativeRing + "Warning: isCommutativeRing was deprecated in v1.1. + Please use ⊕-∧-isCommutativeRing instead." + #-} + commutativeRing = ⊕-∧-commutativeRing + {-# WARNING_ON_USAGE commutativeRing + "Warning: commutativeRing was deprecated in v1.1. + Please use ⊕-∧-commutativeRing instead." + #-} + + +infixl 6 _⊕_ + +_⊕_ : Op₂ Carrier +x ⊕ y = (x ∨ y) ∧ ¬ (x ∧ y) + +module DefaultXorRing = XorRing _⊕_ (λ _ _ → refl) diff --git a/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda b/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda new file mode 100644 index 0000000000..faa2b05983 --- /dev/null +++ b/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda @@ -0,0 +1,185 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Boolean algebra expressions +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Lattice + +module Algebra.Lattice.Properties.BooleanAlgebra.Expression + {b} (B : BooleanAlgebra b b) + where + +open BooleanAlgebra B + +open import Category.Applicative +import Category.Applicative.Indexed as Applicative +open import Category.Monad +open import Data.Fin.Base using (Fin) +open import Data.Nat.Base +open import Data.Product using (_,_; proj₁; proj₂) +open import Data.Vec.Base as Vec using (Vec) +import Data.Vec.Categorical as VecCat +import Function.Identity.Categorical as IdCat +open import Data.Vec.Properties using (lookup-map) +open import Data.Vec.Relation.Binary.Pointwise.Extensional as PW + using (Pointwise; ext) +open import Function +open import Relation.Binary.PropositionalEquality as P using (_≗_) +import Relation.Binary.Reflection as Reflection + +-- Expressions made up of variables and the operations of a boolean +-- algebra. + +infixr 7 _and_ +infixr 6 _or_ + +data Expr n : Set b where + var : (x : Fin n) → Expr n + _or_ _and_ : (e₁ e₂ : Expr n) → Expr n + not : (e : Expr n) → Expr n + top bot : Expr n + +-- The semantics of an expression, parametrised by an applicative +-- functor. + +module Semantics + {F : Set b → Set b} + (A : RawApplicative F) + where + + open RawApplicative A + + ⟦_⟧ : ∀ {n} → Expr n → Vec (F Carrier) n → F Carrier + ⟦ var x ⟧ ρ = Vec.lookup ρ x + ⟦ e₁ or e₂ ⟧ ρ = pure _∨_ ⊛ ⟦ e₁ ⟧ ρ ⊛ ⟦ e₂ ⟧ ρ + ⟦ e₁ and e₂ ⟧ ρ = pure _∧_ ⊛ ⟦ e₁ ⟧ ρ ⊛ ⟦ e₂ ⟧ ρ + ⟦ not e ⟧ ρ = pure ¬_ ⊛ ⟦ e ⟧ ρ + ⟦ top ⟧ ρ = pure ⊤ + ⟦ bot ⟧ ρ = pure ⊥ + +-- flip Semantics.⟦_⟧ e is natural. + +module Naturality + {F₁ F₂ : Set b → Set b} + {A₁ : RawApplicative F₁} + {A₂ : RawApplicative F₂} + (f : Applicative.Morphism A₁ A₂) + where + + open P.≡-Reasoning + open Applicative.Morphism f + open Semantics A₁ renaming (⟦_⟧ to ⟦_⟧₁) + open Semantics A₂ renaming (⟦_⟧ to ⟦_⟧₂) + open RawApplicative A₁ renaming (pure to pure₁; _⊛_ to _⊛₁_) + open RawApplicative A₂ renaming (pure to pure₂; _⊛_ to _⊛₂_) + + natural : ∀ {n} (e : Expr n) → op ∘ ⟦ e ⟧₁ ≗ ⟦ e ⟧₂ ∘ Vec.map op + natural (var x) ρ = begin + op (Vec.lookup ρ x) ≡⟨ P.sym $ lookup-map x op ρ ⟩ + Vec.lookup (Vec.map op ρ) x ∎ + natural (e₁ or e₂) ρ = begin + op (pure₁ _∨_ ⊛₁ ⟦ e₁ ⟧₁ ρ ⊛₁ ⟦ e₂ ⟧₁ ρ) ≡⟨ op-⊛ _ _ ⟩ + op (pure₁ _∨_ ⊛₁ ⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (op-⊛ _ _) P.refl ⟩ + op (pure₁ _∨_) ⊛₂ op (⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (P.cong₂ _⊛₂_ (op-pure _) (natural e₁ ρ)) + (natural e₂ ρ) ⟩ + pure₂ _∨_ ⊛₂ ⟦ e₁ ⟧₂ (Vec.map op ρ) ⊛₂ ⟦ e₂ ⟧₂ (Vec.map op ρ) ∎ + natural (e₁ and e₂) ρ = begin + op (pure₁ _∧_ ⊛₁ ⟦ e₁ ⟧₁ ρ ⊛₁ ⟦ e₂ ⟧₁ ρ) ≡⟨ op-⊛ _ _ ⟩ + op (pure₁ _∧_ ⊛₁ ⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (op-⊛ _ _) P.refl ⟩ + op (pure₁ _∧_) ⊛₂ op (⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (P.cong₂ _⊛₂_ (op-pure _) (natural e₁ ρ)) + (natural e₂ ρ) ⟩ + pure₂ _∧_ ⊛₂ ⟦ e₁ ⟧₂ (Vec.map op ρ) ⊛₂ ⟦ e₂ ⟧₂ (Vec.map op ρ) ∎ + natural (not e) ρ = begin + op (pure₁ ¬_ ⊛₁ ⟦ e ⟧₁ ρ) ≡⟨ op-⊛ _ _ ⟩ + op (pure₁ ¬_) ⊛₂ op (⟦ e ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (op-pure _) (natural e ρ) ⟩ + pure₂ ¬_ ⊛₂ ⟦ e ⟧₂ (Vec.map op ρ) ∎ + natural top ρ = begin + op (pure₁ ⊤) ≡⟨ op-pure _ ⟩ + pure₂ ⊤ ∎ + natural bot ρ = begin + op (pure₁ ⊥) ≡⟨ op-pure _ ⟩ + pure₂ ⊥ ∎ + +-- An example of how naturality can be used: Any boolean algebra can +-- be lifted, in a pointwise manner, to vectors of carrier elements. + +lift : ℕ → BooleanAlgebra b b +lift n = record + { Carrier = Vec Carrier n + ; _≈_ = Pointwise _≈_ + ; _∨_ = zipWith _∨_ + ; _∧_ = zipWith _∧_ + ; ¬_ = map ¬_ + ; ⊤ = pure ⊤ + ; ⊥ = pure ⊥ + ; isBooleanAlgebra = isBooleanAlgebraʳ $ record + { isDistributiveLattice = isDistributiveLatticeʳʲᵐ $ record + { isLattice = record + { isEquivalence = PW.isEquivalence isEquivalence + ; ∨-comm = λ _ _ → ext λ i → + solve i 2 (λ x y → x or y , y or x) + (∨-comm _ _) _ _ + ; ∨-assoc = λ _ _ _ → ext λ i → + solve i 3 + (λ x y z → (x or y) or z , x or (y or z)) + (∨-assoc _ _ _) _ _ _ + ; ∨-cong = λ xs≈us ys≈vs → ext λ i → + solve₁ i 4 (λ x y u v → x or y , u or v) + _ _ _ _ + (∨-cong (Pointwise.app xs≈us i) + (Pointwise.app ys≈vs i)) + ; ∧-comm = λ _ _ → ext λ i → + solve i 2 (λ x y → x and y , y and x) + (∧-comm _ _) _ _ + ; ∧-assoc = λ _ _ _ → ext λ i → + solve i 3 + (λ x y z → (x and y) and z , + x and (y and z)) + (∧-assoc _ _ _) _ _ _ + ; ∧-cong = λ xs≈ys us≈vs → ext λ i → + solve₁ i 4 (λ x y u v → x and y , u and v) + _ _ _ _ + (∧-cong (Pointwise.app xs≈ys i) + (Pointwise.app us≈vs i)) + ; absorptive = + (λ _ _ → ext λ i → + solve i 2 (λ x y → x or (x and y) , x) (∨-absorbs-∧ _ _) _ _) , + (λ _ _ → ext λ i → + solve i 2 (λ x y → x and (x or y) , x) (∧-absorbs-∨ _ _) _ _) + } + ; ∨-distribʳ-∧ = λ _ _ _ → ext λ i → + solve i 3 + (λ x y z → (y and z) or x , + (y or x) and (z or x)) + (∨-distribʳ-∧ _ _ _) _ _ _ + } + ; ∨-complementʳ = λ _ → ext λ i → + solve i 1 (λ x → x or (not x) , top) + (∨-complementʳ _) _ + ; ∧-complementʳ = λ _ → ext λ i → + solve i 1 (λ x → x and (not x) , bot) + (∧-complementʳ _) _ + ; ¬-cong = λ xs≈ys → ext λ i → + solve₁ i 2 (λ x y → not x , not y) _ _ + (¬-cong (Pointwise.app xs≈ys i)) + } + } + where + open RawApplicative VecCat.applicative + using (pure; zipWith) renaming (_<$>_ to map) + + ⟦_⟧Id : ∀ {n} → Expr n → Vec Carrier n → Carrier + ⟦_⟧Id = Semantics.⟦_⟧ IdCat.applicative + + ⟦_⟧Vec : ∀ {m n} → Expr n → Vec (Vec Carrier m) n → Vec Carrier m + ⟦_⟧Vec = Semantics.⟦_⟧ VecCat.applicative + + open module R {n} (i : Fin n) = + Reflection setoid var + (λ e ρ → Vec.lookup (⟦ e ⟧Vec ρ) i) + (λ e ρ → ⟦ e ⟧Id (Vec.map (flip Vec.lookup i) ρ)) + (λ e ρ → sym $ reflexive $ + Naturality.natural (VecCat.lookup-morphism i) e ρ) diff --git a/src/Algebra/Lattice/Properties/DistributiveLattice.agda b/src/Algebra/Lattice/Properties/DistributiveLattice.agda new file mode 100644 index 0000000000..ea37c9c132 --- /dev/null +++ b/src/Algebra/Lattice/Properties/DistributiveLattice.agda @@ -0,0 +1,39 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Some derivable properties +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Lattice.Bundles +import Algebra.Lattice.Properties.Lattice as LatticeProperties + +module Algebra.Lattice.Properties.DistributiveLattice + {dl₁ dl₂} (DL : DistributiveLattice dl₁ dl₂) + where + +open DistributiveLattice DL +open import Algebra.Definitions _≈_ +open import Algebra.Lattice.Structures _≈_ +open import Relation.Binary.Reasoning.Setoid setoid + +------------------------------------------------------------------------ +-- Export properties of lattices + +open LatticeProperties lattice public + +------------------------------------------------------------------------ +-- The dual construction is also a distributive lattice. + +∧-∨-isDistributiveLattice : IsDistributiveLattice _∧_ _∨_ +∧-∨-isDistributiveLattice = record + { isLattice = ∧-∨-isLattice + ; ∨-distrib-∧ = ∧-distrib-∨ + ; ∧-distrib-∨ = ∨-distrib-∧ + } + +∧-∨-distributiveLattice : DistributiveLattice _ _ +∧-∨-distributiveLattice = record + { isDistributiveLattice = ∧-∨-isDistributiveLattice + } diff --git a/src/Algebra/Lattice/Properties/Lattice.agda b/src/Algebra/Lattice/Properties/Lattice.agda new file mode 100644 index 0000000000..ae8875182c --- /dev/null +++ b/src/Algebra/Lattice/Properties/Lattice.agda @@ -0,0 +1,180 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Some derivable properties of lattices +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Lattice.Bundles +import Algebra.Lattice.Properties.Semilattice as SemilatticeProperties +open import Relation.Binary +import Relation.Binary.Lattice as R +open import Function.Base +open import Data.Product using (_,_; swap) + +module Algebra.Lattice.Properties.Lattice + {l₁ l₂} (L : Lattice l₁ l₂) where + +open Lattice L +open import Algebra.Definitions _≈_ +open import Algebra.Structures _≈_ +open import Algebra.Lattice.Structures _≈_ +open import Relation.Binary.Reasoning.Setoid setoid + +------------------------------------------------------------------------ +-- _∧_ is a semilattice + +∧-idem : Idempotent _∧_ +∧-idem x = begin + x ∧ x ≈˘⟨ ∧-congˡ (∨-absorbs-∧ _ _) ⟩ + x ∧ (x ∨ x ∧ x) ≈⟨ ∧-absorbs-∨ _ _ ⟩ + x ∎ + +∧-isMagma : IsMagma _∧_ +∧-isMagma = record + { isEquivalence = isEquivalence + ; ∙-cong = ∧-cong + } + +∧-isSemigroup : IsSemigroup _∧_ +∧-isSemigroup = record + { isMagma = ∧-isMagma + ; assoc = ∧-assoc + } + +∧-isBand : IsBand _∧_ +∧-isBand = record + { isSemigroup = ∧-isSemigroup + ; idem = ∧-idem + } + +∧-isSemilattice : IsSemilattice _∧_ +∧-isSemilattice = record + { isBand = ∧-isBand + ; comm = ∧-comm + } + +∧-semilattice : Semilattice l₁ l₂ +∧-semilattice = record + { isSemilattice = ∧-isSemilattice + } + +open SemilatticeProperties ∧-semilattice public + using + ( ∧-isOrderTheoreticMeetSemilattice + ; ∧-isOrderTheoreticJoinSemilattice + ; ∧-orderTheoreticMeetSemilattice + ; ∧-orderTheoreticJoinSemilattice + ) + +------------------------------------------------------------------------ +-- _∨_ is a semilattice + +∨-idem : Idempotent _∨_ +∨-idem x = begin + x ∨ x ≈˘⟨ ∨-congˡ (∧-idem _) ⟩ + x ∨ x ∧ x ≈⟨ ∨-absorbs-∧ _ _ ⟩ + x ∎ + +∨-isMagma : IsMagma _∨_ +∨-isMagma = record + { isEquivalence = isEquivalence + ; ∙-cong = ∨-cong + } + +∨-isSemigroup : IsSemigroup _∨_ +∨-isSemigroup = record + { isMagma = ∨-isMagma + ; assoc = ∨-assoc + } + +∨-isBand : IsBand _∨_ +∨-isBand = record + { isSemigroup = ∨-isSemigroup + ; idem = ∨-idem + } + +∨-isSemilattice : IsSemilattice _∨_ +∨-isSemilattice = record + { isBand = ∨-isBand + ; comm = ∨-comm + } + +∨-semilattice : Semilattice l₁ l₂ +∨-semilattice = record + { isSemilattice = ∨-isSemilattice + } + +open SemilatticeProperties ∨-semilattice public + using () + renaming + ( ∧-isOrderTheoreticMeetSemilattice to ∨-isOrderTheoreticMeetSemilattice + ; ∧-isOrderTheoreticJoinSemilattice to ∨-isOrderTheoreticJoinSemilattice + ; ∧-orderTheoreticMeetSemilattice to ∨-orderTheoreticMeetSemilattice + ; ∧-orderTheoreticJoinSemilattice to ∨-orderTheoreticJoinSemilattice + ) + +------------------------------------------------------------------------ +-- The dual construction is also a lattice. + +∧-∨-isLattice : IsLattice _∧_ _∨_ +∧-∨-isLattice = record + { isEquivalence = isEquivalence + ; ∨-comm = ∧-comm + ; ∨-assoc = ∧-assoc + ; ∨-cong = ∧-cong + ; ∧-comm = ∨-comm + ; ∧-assoc = ∨-assoc + ; ∧-cong = ∨-cong + ; absorptive = swap absorptive + } + +∧-∨-lattice : Lattice _ _ +∧-∨-lattice = record + { isLattice = ∧-∨-isLattice + } + +------------------------------------------------------------------------ +-- Every algebraic lattice can be turned into an order-theoretic one. + +open SemilatticeProperties ∧-semilattice public using (poset) +open Poset poset using (_≤_; isPartialOrder) + +∨-∧-isOrderTheoreticLattice : R.IsLattice _≈_ _≤_ _∨_ _∧_ +∨-∧-isOrderTheoreticLattice = record + { isPartialOrder = isPartialOrder + ; supremum = supremum + ; infimum = infimum + } + where + open R.MeetSemilattice ∧-orderTheoreticMeetSemilattice using (infimum) + open R.JoinSemilattice ∨-orderTheoreticJoinSemilattice using (x≤x∨y; y≤x∨y; ∨-least) + renaming (_≤_ to _≤′_) + + -- An alternative but equivalent interpretation of the order _≤_. + + sound : ∀ {x y} → x ≤′ y → x ≤ y + sound {x} {y} y≈y∨x = sym $ begin + x ∧ y ≈⟨ ∧-congˡ y≈y∨x ⟩ + x ∧ (y ∨ x) ≈⟨ ∧-congˡ (∨-comm y x) ⟩ + x ∧ (x ∨ y) ≈⟨ ∧-absorbs-∨ x y ⟩ + x ∎ + + complete : ∀ {x y} → x ≤ y → x ≤′ y + complete {x} {y} x≈x∧y = sym $ begin + y ∨ x ≈⟨ ∨-congˡ x≈x∧y ⟩ + y ∨ (x ∧ y) ≈⟨ ∨-congˡ (∧-comm x y) ⟩ + y ∨ (y ∧ x) ≈⟨ ∨-absorbs-∧ y x ⟩ + y ∎ + + supremum : R.Supremum _≤_ _∨_ + supremum x y = + sound (x≤x∨y x y) , + sound (y≤x∨y x y) , + λ z x≤z y≤z → sound (∨-least (complete x≤z) (complete y≤z)) + +∨-∧-orderTheoreticLattice : R.Lattice _ _ _ +∨-∧-orderTheoreticLattice = record + { isLattice = ∨-∧-isOrderTheoreticLattice + } diff --git a/src/Algebra/Lattice/Properties/Semilattice.agda b/src/Algebra/Lattice/Properties/Semilattice.agda new file mode 100644 index 0000000000..03bab8cf7c --- /dev/null +++ b/src/Algebra/Lattice/Properties/Semilattice.agda @@ -0,0 +1,60 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Some derivable properties of semilattices +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Lattice +open import Algebra.Structures +open import Function +open import Data.Product +open import Relation.Binary +import Relation.Binary.Lattice as B +import Relation.Binary.Properties.Poset as PosetProperties + +module Algebra.Lattice.Properties.Semilattice + {c ℓ} (L : Semilattice c ℓ) where + +open Semilattice L renaming (_∙_ to _∧_) + +open import Relation.Binary.Reasoning.Setoid setoid +import Relation.Binary.Construct.NaturalOrder.Left _≈_ _∧_ + as LeftNaturalOrder + +------------------------------------------------------------------------ +-- Every semilattice can be turned into a poset via the left natural +-- order. + +poset : Poset c ℓ ℓ +poset = LeftNaturalOrder.poset isSemilattice + +open Poset poset using (_≤_; isPartialOrder) +open PosetProperties poset using (_≥_; ≥-isPartialOrder) + +------------------------------------------------------------------------ +-- Every algebraic semilattice can be turned into an order-theoretic one. + +∧-isOrderTheoreticMeetSemilattice : B.IsMeetSemilattice _≈_ _≤_ _∧_ +∧-isOrderTheoreticMeetSemilattice = record + { isPartialOrder = isPartialOrder + ; infimum = LeftNaturalOrder.infimum isSemilattice + } + +∧-isOrderTheoreticJoinSemilattice : B.IsJoinSemilattice _≈_ _≥_ _∧_ +∧-isOrderTheoreticJoinSemilattice = record + { isPartialOrder = ≥-isPartialOrder + ; supremum = B.IsMeetSemilattice.infimum + ∧-isOrderTheoreticMeetSemilattice + } + +∧-orderTheoreticMeetSemilattice : B.MeetSemilattice c ℓ ℓ +∧-orderTheoreticMeetSemilattice = record + { isMeetSemilattice = ∧-isOrderTheoreticMeetSemilattice + } + +∧-orderTheoreticJoinSemilattice : B.JoinSemilattice c ℓ ℓ +∧-orderTheoreticJoinSemilattice = record + { isJoinSemilattice = ∧-isOrderTheoreticJoinSemilattice + } diff --git a/src/Algebra/Lattice/Structures.agda b/src/Algebra/Lattice/Structures.agda new file mode 100644 index 0000000000..19e36460cb --- /dev/null +++ b/src/Algebra/Lattice/Structures.agda @@ -0,0 +1,201 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Some lattice-like structures defined by properties of _∧_ and _∨_ +-- (not packed up with sets, operations, etc.) +-- +-- For lattices defined via an order relation, see +-- Relation.Binary.Lattice. +------------------------------------------------------------------------ + +-- The contents of this module should be accessed via `Algebra.Lattice`, +-- unless you want to parameterise it via the equality relation. + +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Core +open import Data.Product using (proj₁; proj₂) +open import Level using (_⊔_) +open import Relation.Binary using (Rel; Setoid; IsEquivalence) + +module Algebra.Lattice.Structures + {a ℓ} {A : Set a} -- The underlying set + (_≈_ : Rel A ℓ) -- The underlying equality relation + where + +open import Algebra.Definitions _≈_ +open import Algebra.Structures _≈_ + +------------------------------------------------------------------------ +-- Structures with 1 binary operation + +record IsSemilattice (∙ : Op₂ A) : Set (a ⊔ ℓ) where + field + isBand : IsBand ∙ + comm : Commutative ∙ + + open IsBand isBand public + renaming + ( ∙-cong to ∧-cong + ; ∙-congˡ to ∧-congˡ + ; ∙-congʳ to ∧-congʳ + ) + +-- Used to bring names appropriate for a meet semilattice into scope. +IsMeetSemilattice = IsSemilattice +module IsMeetSemilattice {∧} (L : IsMeetSemilattice ∧) where + open IsSemilattice L public + renaming + ( ∧-cong to ∧-cong + ; ∧-congˡ to ∧-congˡ + ; ∧-congʳ to ∧-congʳ + ) + +-- Used to bring names appropriate for a join semilattice into scope. +IsJoinSemilattice = IsSemilattice +module IsJoinSemilattice {∨} (L : IsJoinSemilattice ∨) where + open IsSemilattice L public + renaming + ( ∧-cong to ∨-cong + ; ∧-congˡ to ∨-congˡ + ; ∧-congʳ to ∨-congʳ + ) + +------------------------------------------------------------------------ +-- Structures with 1 binary operation & 1 element + +-- A bounded semi-lattice is the same thing as an idempotent commutative +-- monoid. +IsBoundedSemilattice = IsIdempotentCommutativeMonoid +module IsBoundedSemilattice {∙ ε} (L : IsBoundedSemilattice ∙ ε) where + + open IsIdempotentCommutativeMonoid L public + + isSemilattice : IsSemilattice ∙ + isSemilattice = record + { isBand = isBand + ; comm = comm + } + + +-- Used to bring names appropriate for a bounded meet semilattice +-- into scope. +IsBoundedMeetSemilattice = IsBoundedSemilattice +module IsBoundedMeetSemilattice {∧ ⊤} (L : IsBoundedMeetSemilattice ∧ ⊤) + where + + open IsBoundedSemilattice L public + using (identity; identityˡ; identityʳ) + renaming (isSemilattice to isMeetSemilattice) + + open IsMeetSemilattice isMeetSemilattice public + + +-- Used to bring names appropriate for a bounded join semilattice +-- into scope. +IsBoundedJoinSemilattice = IsBoundedSemilattice +module IsBoundedJoinSemilattice {∨ ⊥} (L : IsBoundedJoinSemilattice ∨ ⊥) + where + + open IsBoundedSemilattice L public + using (identity; identityˡ; identityʳ) + renaming (isSemilattice to isJoinSemilattice) + + open IsJoinSemilattice isJoinSemilattice public + +------------------------------------------------------------------------ +-- Structures with 2 binary operations + +-- Note that `IsLattice` is not defined in terms of `IsMeetSemilattice` +-- and `IsJoinSemilattice` for two reasons: +-- 1) it would result in a structure with two *different* proofs that +-- the equality relation `≈` is an equivalence relation. +-- 2) the idempotence laws of ∨ and ∧ can be derived from the +-- absorption laws, which makes the corresponding "idem" fields +-- redundant. +-- +-- It is possible to construct the `IsLattice` record from +-- `IsMeetSemilattice` and `IsJoinSemilattice` via the `IsLattice₂` +-- record found in `Algebra.Lattice.Structures.Biased`. +-- +-- The derived idempotence laws are stated and proved in +-- `Algebra.Lattice.Properties.Lattice` along with the fact that every +-- lattice consists of two semilattices. + +record IsLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where + field + isEquivalence : IsEquivalence _≈_ + ∨-comm : Commutative ∨ + ∨-assoc : Associative ∨ + ∨-cong : Congruent₂ ∨ + ∧-comm : Commutative ∧ + ∧-assoc : Associative ∧ + ∧-cong : Congruent₂ ∧ + absorptive : Absorptive ∨ ∧ + + open IsEquivalence isEquivalence public + + ∨-absorbs-∧ : ∨ Absorbs ∧ + ∨-absorbs-∧ = proj₁ absorptive + + ∧-absorbs-∨ : ∧ Absorbs ∨ + ∧-absorbs-∨ = proj₂ absorptive + + ∧-congˡ : LeftCongruent ∧ + ∧-congˡ y≈z = ∧-cong refl y≈z + + ∧-congʳ : RightCongruent ∧ + ∧-congʳ y≈z = ∧-cong y≈z refl + + ∨-congˡ : LeftCongruent ∨ + ∨-congˡ y≈z = ∨-cong refl y≈z + + ∨-congʳ : RightCongruent ∨ + ∨-congʳ y≈z = ∨-cong y≈z refl + + +record IsDistributiveLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where + field + isLattice : IsLattice ∨ ∧ + ∨-distrib-∧ : ∨ DistributesOver ∧ + ∧-distrib-∨ : ∧ DistributesOver ∨ + + open IsLattice isLattice public + + ∨-distribˡ-∧ : ∨ DistributesOverˡ ∧ + ∨-distribˡ-∧ = proj₁ ∨-distrib-∧ + + ∨-distribʳ-∧ : ∨ DistributesOverʳ ∧ + ∨-distribʳ-∧ = proj₂ ∨-distrib-∧ + + ∧-distribˡ-∨ : ∧ DistributesOverˡ ∨ + ∧-distribˡ-∨ = proj₁ ∧-distrib-∨ + + ∧-distribʳ-∨ : ∧ DistributesOverʳ ∨ + ∧-distribʳ-∨ = proj₂ ∧-distrib-∨ + +------------------------------------------------------------------------ +-- Structures with 2 binary ops, 1 unary op and 2 elements. + +record IsBooleanAlgebra (∨ ∧ : Op₂ A) (¬ : Op₁ A) (⊤ ⊥ : A) : Set (a ⊔ ℓ) + where + + field + isDistributiveLattice : IsDistributiveLattice ∨ ∧ + ∨-complement : Inverse ⊤ ¬ ∨ + ∧-complement : Inverse ⊥ ¬ ∧ + ¬-cong : Congruent₁ ¬ + + open IsDistributiveLattice isDistributiveLattice public + + ∨-complementˡ : LeftInverse ⊤ ¬ ∨ + ∨-complementˡ = proj₁ ∨-complement + + ∨-complementʳ : RightInverse ⊤ ¬ ∨ + ∨-complementʳ = proj₂ ∨-complement + + ∧-complementˡ : LeftInverse ⊥ ¬ ∧ + ∧-complementˡ = proj₁ ∧-complement + + ∧-complementʳ : RightInverse ⊥ ¬ ∧ + ∧-complementʳ = proj₂ ∧-complement diff --git a/src/Algebra/Lattice/Structures/Biased.agda b/src/Algebra/Lattice/Structures/Biased.agda new file mode 100644 index 0000000000..b3b7455290 --- /dev/null +++ b/src/Algebra/Lattice/Structures/Biased.agda @@ -0,0 +1,121 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Some biased records for lattice-like structures. Such records are +-- often easier to construct, but are suboptimal to use more widely and +-- should be converted to the standard record definitions immediately +-- using the provided conversion functions. +------------------------------------------------------------------------ + +-- The contents of this module should be accessed via `Algebra.Lattice`, +-- unless you want to parameterise it via the equality relation. + +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Core +open import Algebra.Consequences.Setoid +open import Data.Product using (proj₁; proj₂) +open import Level using (_⊔_) +open import Relation.Binary using (Rel; Setoid; IsEquivalence) + +module Algebra.Lattice.Structures.Biased + {a ℓ} {A : Set a} -- The underlying set + (_≈_ : Rel A ℓ) -- The underlying equality relation + where + +open import Algebra.Definitions _≈_ +open import Algebra.Lattice.Structures _≈_ + +private + variable + ∧ ∨ : Op₂ A + ¬ : Op₁ A + ⊤ ⊥ : A + +------------------------------------------------------------------------ +-- Lattice + +-- An alternative form of `IsLattice` defined in terms of +-- `IsJoinSemilattice` and `IsMeetLattice`. This form may be desirable +-- to use when constructing a lattice object as it requires fewer +-- arguments, but is often a mistake to use as an argument as it +-- contains two, *potentially different*, proofs that the equality +-- relation _≈_ is an equivalence. + +record IsLattice₂ (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where + field + isJoinSemilattice : IsJoinSemilattice ∨ + isMeetSemilattice : IsMeetSemilattice ∧ + absorptive : Absorptive ∨ ∧ + + module ML = IsMeetSemilattice isMeetSemilattice + module JL = IsJoinSemilattice isJoinSemilattice + + isLattice₂ : IsLattice ∨ ∧ + isLattice₂ = record + { isEquivalence = ML.isEquivalence + ; ∨-comm = JL.comm + ; ∨-assoc = JL.assoc + ; ∨-cong = JL.∨-cong + ; ∧-comm = ML.comm + ; ∧-assoc = ML.assoc + ; ∧-cong = ML.∧-cong + ; absorptive = absorptive + } + +open IsLattice₂ public using (isLattice₂) + +------------------------------------------------------------------------ +-- DistributiveLattice + +-- A version of distributive lattice that is biased towards the (r)ight +-- distributivity law for (j)oin and (m)eet. +record IsDistributiveLatticeʳʲᵐ (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where + field + isLattice : IsLattice ∨ ∧ + ∨-distribʳ-∧ : ∨ DistributesOverʳ ∧ + + open IsLattice isLattice public + + setoid : Setoid a ℓ + setoid = record { isEquivalence = isEquivalence } + + ∨-distrib-∧ = comm+distrʳ⇒distr setoid ∧-cong ∨-comm ∨-distribʳ-∧ + ∧-distribˡ-∨ = distrib+absorbs⇒distribˡ setoid ∧-cong ∧-assoc ∨-comm ∧-absorbs-∨ ∨-absorbs-∧ ∨-distrib-∧ + ∧-distrib-∨ = comm+distrˡ⇒distr setoid ∨-cong ∧-comm ∧-distribˡ-∨ + + isDistributiveLatticeʳʲᵐ : IsDistributiveLattice ∨ ∧ + isDistributiveLatticeʳʲᵐ = record + { isLattice = isLattice + ; ∨-distrib-∧ = ∨-distrib-∧ + ; ∧-distrib-∨ = ∧-distrib-∨ + } + +open IsDistributiveLatticeʳʲᵐ public using (isDistributiveLatticeʳʲᵐ) + +------------------------------------------------------------------------ +-- BooleanAlgebra + +-- A (r)ight biased version of a boolean algebra. +record IsBooleanAlgebraʳ + (∨ ∧ : Op₂ A) (¬ : Op₁ A) (⊤ ⊥ : A) : Set (a ⊔ ℓ) where + field + isDistributiveLattice : IsDistributiveLattice ∨ ∧ + ∨-complementʳ : RightInverse ⊤ ¬ ∨ + ∧-complementʳ : RightInverse ⊥ ¬ ∧ + ¬-cong : Congruent₁ ¬ + + open IsDistributiveLattice isDistributiveLattice public + + setoid : Setoid a ℓ + setoid = record { isEquivalence = isEquivalence } + + isBooleanAlgebraʳ : IsBooleanAlgebra ∨ ∧ ¬ ⊤ ⊥ + isBooleanAlgebraʳ = record + { isDistributiveLattice = isDistributiveLattice + ; ∨-complement = comm+invʳ⇒inv setoid ∨-comm ∨-complementʳ + ; ∧-complement = comm+invʳ⇒inv setoid ∧-comm ∧-complementʳ + ; ¬-cong = ¬-cong + } + +open IsBooleanAlgebraʳ public using (isBooleanAlgebraʳ) diff --git a/src/Algebra/Morphism/Construct/Composition.agda b/src/Algebra/Morphism/Construct/Composition.agda index 8da6be7a0c..41dfa43a13 100644 --- a/src/Algebra/Morphism/Construct/Composition.agda +++ b/src/Algebra/Morphism/Construct/Composition.agda @@ -263,44 +263,3 @@ module _ {R₁ : RawRing a ℓ₁} { isRingMonomorphism = isRingMonomorphism F.isRingMonomorphism G.isRingMonomorphism ; surjective = Func.surjective (_≈_ R₁) _ _ ≈₃-trans G.⟦⟧-cong F.surjective G.surjective } where module F = IsRingIsomorphism f-iso; module G = IsRingIsomorphism g-iso - - ------------------------------------------------------------------------- --- Lattices - -module _ {L₁ : RawLattice a ℓ₁} - {L₂ : RawLattice b ℓ₂} - {L₃ : RawLattice c ℓ₃} - (open RawLattice) - (≈₃-trans : Transitive (_≈_ L₃)) - {f : Carrier L₁ → Carrier L₂} - {g : Carrier L₂ → Carrier L₃} - where - - isLatticeHomomorphism - : IsLatticeHomomorphism L₁ L₂ f - → IsLatticeHomomorphism L₂ L₃ g - → IsLatticeHomomorphism L₁ L₃ (g ∘ f) - isLatticeHomomorphism f-homo g-homo = record - { isRelHomomorphism = isRelHomomorphism F.isRelHomomorphism G.isRelHomomorphism - ; ∧-homo = λ x y → ≈₃-trans (G.⟦⟧-cong (F.∧-homo x y)) (G.∧-homo (f x) (f y)) - ; ∨-homo = λ x y → ≈₃-trans (G.⟦⟧-cong (F.∨-homo x y)) (G.∨-homo (f x) (f y)) - } where module F = IsLatticeHomomorphism f-homo; module G = IsLatticeHomomorphism g-homo - - isLatticeMonomorphism - : IsLatticeMonomorphism L₁ L₂ f - → IsLatticeMonomorphism L₂ L₃ g - → IsLatticeMonomorphism L₁ L₃ (g ∘ f) - isLatticeMonomorphism f-mono g-mono = record - { isLatticeHomomorphism = isLatticeHomomorphism F.isLatticeHomomorphism G.isLatticeHomomorphism - ; injective = F.injective ∘ G.injective - } where module F = IsLatticeMonomorphism f-mono; module G = IsLatticeMonomorphism g-mono - - isLatticeIsomorphism - : IsLatticeIsomorphism L₁ L₂ f - → IsLatticeIsomorphism L₂ L₃ g - → IsLatticeIsomorphism L₁ L₃ (g ∘ f) - isLatticeIsomorphism f-iso g-iso = record - { isLatticeMonomorphism = isLatticeMonomorphism F.isLatticeMonomorphism G.isLatticeMonomorphism - ; surjective = Func.surjective (_≈_ L₁) _ _ ≈₃-trans G.⟦⟧-cong F.surjective G.surjective - } where module F = IsLatticeIsomorphism f-iso; module G = IsLatticeIsomorphism g-iso diff --git a/src/Algebra/Morphism/Construct/Identity.agda b/src/Algebra/Morphism/Construct/Identity.agda index add9b499ee..8555c69a5f 100644 --- a/src/Algebra/Morphism/Construct/Identity.agda +++ b/src/Algebra/Morphism/Construct/Identity.agda @@ -16,7 +16,6 @@ open import Algebra.Morphism.Structures ; module NearSemiringMorphisms ; module SemiringMorphisms ; module RingMorphisms - ; module LatticeMorphisms ) open import Data.Product using (_,_) open import Function.Base using (id) @@ -153,25 +152,3 @@ module _ (R : RawRing c ℓ) (open RawRing R) (refl : Reflexive _≈_) where { isRingMonomorphism = isRingMonomorphism ; surjective = _, refl } - -module _ (L : RawLattice c ℓ) (open RawLattice L) (refl : Reflexive _≈_) where - open LatticeMorphisms L L - - isLatticeHomomorphism : IsLatticeHomomorphism id - isLatticeHomomorphism = record - { isRelHomomorphism = isRelHomomorphism _ - ; ∧-homo = λ _ _ → refl - ; ∨-homo = λ _ _ → refl - } - - isLatticeMonomorphism : IsLatticeMonomorphism id - isLatticeMonomorphism = record - { isLatticeHomomorphism = isLatticeHomomorphism - ; injective = id - } - - isLatticeIsomorphism : IsLatticeIsomorphism id - isLatticeIsomorphism = record - { isLatticeMonomorphism = isLatticeMonomorphism - ; surjective = _, refl - } diff --git a/src/Algebra/Morphism/MagmaMonomorphism.agda b/src/Algebra/Morphism/MagmaMonomorphism.agda index e085efd6a1..2cad60e77e 100644 --- a/src/Algebra/Morphism/MagmaMonomorphism.agda +++ b/src/Algebra/Morphism/MagmaMonomorphism.agda @@ -116,12 +116,6 @@ isBand isBand = record ; idem = idem B.isMagma B.idem } where module B = IsBand isBand -isSemilattice : IsSemilattice _≈₂_ _◦_ → IsSemilattice _≈₁_ _∙_ -isSemilattice isSemilattice = record - { isBand = isBand S.isBand - ; comm = comm S.isMagma S.comm - } where module S = IsSemilattice isSemilattice - isSelectiveMagma : IsSelectiveMagma _≈₂_ _◦_ → IsSelectiveMagma _≈₁_ _∙_ isSelectiveMagma isSelMagma = record { isMagma = isMagma S.isMagma diff --git a/src/Algebra/Morphism/RingMonomorphism.agda b/src/Algebra/Morphism/RingMonomorphism.agda index 431a0a5af2..8cb93067c0 100644 --- a/src/Algebra/Morphism/RingMonomorphism.agda +++ b/src/Algebra/Morphism/RingMonomorphism.agda @@ -11,6 +11,8 @@ open import Algebra.Bundles open import Algebra.Morphism.Structures +import Algebra.Morphism.GroupMonomorphism as GroupMonomorphism +import Algebra.Morphism.MonoidMonomorphism as MonoidMonomorphism open import Relation.Binary.Core module Algebra.Morphism.RingMonomorphism @@ -32,44 +34,46 @@ import Relation.Binary.Reasoning.Setoid as SetoidReasoning ------------------------------------------------------------------------ -- Re-export all properties of group and monoid monomorphisms -open import Algebra.Morphism.GroupMonomorphism - +-isGroupMonomorphism renaming - ( assoc to +-assoc - ; comm to +-comm - ; cong to +-cong - ; idem to +-idem +open GroupMonomorphism +-isGroupMonomorphism public + renaming + ( assoc to +-assoc + ; comm to +-comm + ; cong to +-cong + ; idem to +-idem + ; sel to +-sel ; ⁻¹-cong to neg-cong + ; identity to +-identity; identityˡ to +-identityˡ; identityʳ to +-identityʳ - ; cancel to +-cancel; cancelˡ to +-cancelˡ; cancelʳ to +-cancelʳ - ; zero to +-zero; zeroˡ to +-zeroˡ; zeroʳ to +-zeroʳ - ; isMagma to +-isMagma - ; isSemigroup to +-isSemigroup - ; isMonoid to +-isMonoid - ; isSelectiveMagma to +-isSelectiveMagma - ; isSemilattice to +-isSemilattice - ; sel to +-sel - ; isBand to +-isBand + ; cancel to +-cancel; cancelˡ to +-cancelˡ; cancelʳ to +-cancelʳ + ; zero to +-zero; zeroˡ to +-zeroˡ; zeroʳ to +-zeroʳ + + ; isMagma to +-isMagma + ; isSemigroup to +-isSemigroup + ; isMonoid to +-isMonoid + ; isSelectiveMagma to +-isSelectiveMagma + ; isBand to +-isBand ; isCommutativeMonoid to +-isCommutativeMonoid - ) public + ) -open import Algebra.Morphism.MonoidMonomorphism - *-isMonoidMonomorphism renaming +open MonoidMonomorphism *-isMonoidMonomorphism public + renaming ( assoc to *-assoc - ; comm to *-comm - ; cong to *-cong - ; idem to *-idem + ; comm to *-comm + ; cong to *-cong + ; idem to *-idem + ; sel to *-sel + ; identity to *-identity; identityˡ to *-identityˡ; identityʳ to *-identityʳ - ; cancel to *-cancel; cancelˡ to *-cancelˡ; cancelʳ to *-cancelʳ - ; zero to *-zero; zeroˡ to *-zeroˡ; zeroʳ to *-zeroʳ - ; isMagma to *-isMagma - ; isSemigroup to *-isSemigroup - ; isMonoid to *-isMonoid - ; isSelectiveMagma to *-isSelectiveMagma - ; isSemilattice to *-isSemilattice - ; sel to *-sel - ; isBand to *-isBand + ; cancel to *-cancel; cancelˡ to *-cancelˡ; cancelʳ to *-cancelʳ + ; zero to *-zero; zeroˡ to *-zeroˡ; zeroʳ to *-zeroʳ + + ; isMagma to *-isMagma + ; isSemigroup to *-isSemigroup + ; isMonoid to *-isMonoid + ; isSelectiveMagma to *-isSelectiveMagma + ; isBand to *-isBand ; isCommutativeMonoid to *-isCommutativeMonoid - ) public + ) ------------------------------------------------------------------------ -- Properties diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda index 1de98c8700..395e2eeb89 100644 --- a/src/Algebra/Morphism/Structures.agda +++ b/src/Algebra/Morphism/Structures.agda @@ -464,97 +464,6 @@ module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where using () renaming (isMagmaIsomorphism to *-isMagmaIsomorphisn) ------------------------------------------------------------------------- --- Morphisms over lattice-like structures ------------------------------------------------------------------------- - -module LatticeMorphisms (L₁ : RawLattice a ℓ₁) (L₂ : RawLattice b ℓ₂) where - - open RawLattice L₁ renaming - ( Carrier to A; _≈_ to _≈₁_ - ; _∧_ to _∧₁_; _∨_ to _∨₁_ - ; ∧-rawMagma to ∧-rawMagma₁ - ; ∨-rawMagma to ∨-rawMagma₁) - - open RawLattice L₂ renaming - ( Carrier to B; _≈_ to _≈₂_ - ; _∧_ to _∧₂_; _∨_ to _∨₂_ - ; ∧-rawMagma to ∧-rawMagma₂ - ; ∨-rawMagma to ∨-rawMagma₂) - - module ∨ = MagmaMorphisms ∨-rawMagma₁ ∨-rawMagma₂ - module ∧ = MagmaMorphisms ∧-rawMagma₁ ∧-rawMagma₂ - - open MorphismDefinitions A B _≈₂_ - open FunctionDefinitions _≈₁_ _≈₂_ - - - record IsLatticeHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where - field - isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧ - ∧-homo : Homomorphic₂ ⟦_⟧ _∧₁_ _∧₂_ - ∨-homo : Homomorphic₂ ⟦_⟧ _∨₁_ _∨₂_ - - open IsRelHomomorphism isRelHomomorphism public - renaming (cong to ⟦⟧-cong) - - ∧-isMagmaHomomorphism : ∧.IsMagmaHomomorphism ⟦_⟧ - ∧-isMagmaHomomorphism = record - { isRelHomomorphism = isRelHomomorphism - ; homo = ∧-homo - } - - ∨-isMagmaHomomorphism : ∨.IsMagmaHomomorphism ⟦_⟧ - ∨-isMagmaHomomorphism = record - { isRelHomomorphism = isRelHomomorphism - ; homo = ∨-homo - } - - record IsLatticeMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where - field - isLatticeHomomorphism : IsLatticeHomomorphism ⟦_⟧ - injective : Injective ⟦_⟧ - - open IsLatticeHomomorphism isLatticeHomomorphism public - - ∨-isMagmaMonomorphism : ∨.IsMagmaMonomorphism ⟦_⟧ - ∨-isMagmaMonomorphism = record - { isMagmaHomomorphism = ∨-isMagmaHomomorphism - ; injective = injective - } - - ∧-isMagmaMonomorphism : ∧.IsMagmaMonomorphism ⟦_⟧ - ∧-isMagmaMonomorphism = record - { isMagmaHomomorphism = ∧-isMagmaHomomorphism - ; injective = injective - } - - open ∧.IsMagmaMonomorphism ∧-isMagmaMonomorphism public - using (isRelMonomorphism) - - - record IsLatticeIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where - field - isLatticeMonomorphism : IsLatticeMonomorphism ⟦_⟧ - surjective : Surjective ⟦_⟧ - - open IsLatticeMonomorphism isLatticeMonomorphism public - - ∨-isMagmaIsomorphism : ∨.IsMagmaIsomorphism ⟦_⟧ - ∨-isMagmaIsomorphism = record - { isMagmaMonomorphism = ∨-isMagmaMonomorphism - ; surjective = surjective - } - - ∧-isMagmaIsomorphism : ∧.IsMagmaIsomorphism ⟦_⟧ - ∧-isMagmaIsomorphism = record - { isMagmaMonomorphism = ∧-isMagmaMonomorphism - ; surjective = surjective - } - - open ∧.IsMagmaIsomorphism ∧-isMagmaIsomorphism public - using (isRelIsomorphism) - ------------------------------------------------------------------------ -- Re-export contents of modules publicly @@ -564,4 +473,3 @@ open GroupMorphisms public open NearSemiringMorphisms public open SemiringMorphisms public open RingMorphisms public -open LatticeMorphisms public diff --git a/src/Algebra/Properties/BooleanAlgebra.agda b/src/Algebra/Properties/BooleanAlgebra.agda index 73ae60d538..3cd21f3f33 100644 --- a/src/Algebra/Properties/BooleanAlgebra.agda +++ b/src/Algebra/Properties/BooleanAlgebra.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Some derivable properties +-- This module is DEPRECATED. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} @@ -9,570 +9,29 @@ -- Disabled to prevent warnings from deprecated names {-# OPTIONS --warn=noUserWarning #-} -open import Algebra.Bundles +open import Algebra.Lattice.Bundles module Algebra.Properties.BooleanAlgebra {b₁ b₂} (B : BooleanAlgebra b₁ b₂) where +{-# WARNING_ON_IMPORT +"Algebra.Properties.BooleanAlgebra was deprecated in v2.0. +Use Algebra.Lattice.Properties.BooleanAlgebra instead." +#-} + +open import Algebra.Lattice.Properties.BooleanAlgebra B public + open BooleanAlgebra B import Algebra.Properties.DistributiveLattice as DistribLatticeProperties -open import Algebra.Core + open import Algebra.Structures _≈_ -open import Algebra.Definitions _≈_ -open import Algebra.Consequences.Setoid setoid -open import Relation.Binary.Reasoning.Setoid setoid open import Relation.Binary -open import Function.Base open import Function.Equality using (_⟨$⟩_) open import Function.Equivalence using (_⇔_; module Equivalence) open import Data.Product using (_,_) ------------------------------------------------------------------------- --- Export properties from distributive lattices - -open DistribLatticeProperties distributiveLattice public - hiding (replace-equality) - ------------------------------------------------------------------------- --- Some simple consequences - -∨-complementˡ : LeftInverse ⊤ ¬_ _∨_ -∨-complementˡ = comm+invʳ⇒invˡ ∨-comm ∨-complementʳ - -∨-complement : Inverse ⊤ ¬_ _∨_ -∨-complement = ∨-complementˡ , ∨-complementʳ - -∧-complementˡ : LeftInverse ⊥ ¬_ _∧_ -∧-complementˡ = comm+invʳ⇒invˡ ∧-comm ∧-complementʳ - -∧-complement : Inverse ⊥ ¬_ _∧_ -∧-complement = ∧-complementˡ , ∧-complementʳ - ------------------------------------------------------------------------- --- The dual construction is also a boolean algebra - -∧-∨-isBooleanAlgebra : IsBooleanAlgebra _∧_ _∨_ ¬_ ⊥ ⊤ -∧-∨-isBooleanAlgebra = record - { isDistributiveLattice = ∧-∨-isDistributiveLattice - ; ∨-complementʳ = ∧-complementʳ - ; ∧-complementʳ = ∨-complementʳ - ; ¬-cong = ¬-cong - } - -∧-∨-booleanAlgebra : BooleanAlgebra _ _ -∧-∨-booleanAlgebra = record - { isBooleanAlgebra = ∧-∨-isBooleanAlgebra - } - ------------------------------------------------------------------------- --- (∨, ∧, ⊥, ⊤) and (∧, ∨, ⊤, ⊥) are commutative semirings - -∧-identityʳ : RightIdentity ⊤ _∧_ -∧-identityʳ x = begin - x ∧ ⊤ ≈⟨ ∧-congˡ (sym (∨-complementʳ _)) ⟩ - x ∧ (x ∨ ¬ x) ≈⟨ ∧-absorbs-∨ _ _ ⟩ - x ∎ - -∧-identityˡ : LeftIdentity ⊤ _∧_ -∧-identityˡ = comm+idʳ⇒idˡ ∧-comm ∧-identityʳ - -∧-identity : Identity ⊤ _∧_ -∧-identity = ∧-identityˡ , ∧-identityʳ - -∨-identityʳ : RightIdentity ⊥ _∨_ -∨-identityʳ x = begin - x ∨ ⊥ ≈⟨ ∨-congˡ $ sym (∧-complementʳ _) ⟩ - x ∨ x ∧ ¬ x ≈⟨ ∨-absorbs-∧ _ _ ⟩ - x ∎ - -∨-identityˡ : LeftIdentity ⊥ _∨_ -∨-identityˡ = comm+idʳ⇒idˡ ∨-comm ∨-identityʳ - -∨-identity : Identity ⊥ _∨_ -∨-identity = ∨-identityˡ , ∨-identityʳ - -∧-zeroʳ : RightZero ⊥ _∧_ -∧-zeroʳ x = begin - x ∧ ⊥ ≈˘⟨ ∧-congˡ (∧-complementʳ x) ⟩ - x ∧ x ∧ ¬ x ≈˘⟨ ∧-assoc x x (¬ x) ⟩ - (x ∧ x) ∧ ¬ x ≈⟨ ∧-congʳ (∧-idempotent x) ⟩ - x ∧ ¬ x ≈⟨ ∧-complementʳ x ⟩ - ⊥ ∎ - -∧-zeroˡ : LeftZero ⊥ _∧_ -∧-zeroˡ = comm+zeʳ⇒zeˡ ∧-comm ∧-zeroʳ - -∧-zero : Zero ⊥ _∧_ -∧-zero = ∧-zeroˡ , ∧-zeroʳ - -∨-zeroʳ : ∀ x → x ∨ ⊤ ≈ ⊤ -∨-zeroʳ x = begin - x ∨ ⊤ ≈˘⟨ ∨-congˡ (∨-complementʳ x) ⟩ - x ∨ x ∨ ¬ x ≈˘⟨ ∨-assoc x x (¬ x) ⟩ - (x ∨ x) ∨ ¬ x ≈⟨ ∨-congʳ (∨-idempotent x) ⟩ - x ∨ ¬ x ≈⟨ ∨-complementʳ x ⟩ - ⊤ ∎ - -∨-zeroˡ : LeftZero ⊤ _∨_ -∨-zeroˡ = comm+zeʳ⇒zeˡ ∨-comm ∨-zeroʳ - -∨-zero : Zero ⊤ _∨_ -∨-zero = ∨-zeroˡ , ∨-zeroʳ - -∨-⊥-isMonoid : IsMonoid _∨_ ⊥ -∨-⊥-isMonoid = record - { isSemigroup = ∨-isSemigroup - ; identity = ∨-identity - } - -∧-⊤-isMonoid : IsMonoid _∧_ ⊤ -∧-⊤-isMonoid = record - { isSemigroup = ∧-isSemigroup - ; identity = ∧-identity - } - -∨-⊥-isCommutativeMonoid : IsCommutativeMonoid _∨_ ⊥ -∨-⊥-isCommutativeMonoid = record - { isMonoid = ∨-⊥-isMonoid - ; comm = ∨-comm - } - -∧-⊤-isCommutativeMonoid : IsCommutativeMonoid _∧_ ⊤ -∧-⊤-isCommutativeMonoid = record - { isMonoid = ∧-⊤-isMonoid - ; comm = ∧-comm - } - -∨-∧-isSemiring : IsSemiring _∨_ _∧_ ⊥ ⊤ -∨-∧-isSemiring = record - { isSemiringWithoutAnnihilatingZero = record - { +-isCommutativeMonoid = ∨-⊥-isCommutativeMonoid - ; *-isMonoid = ∧-⊤-isMonoid - ; distrib = ∧-∨-distrib - } - ; zero = ∧-zero - } - -∧-∨-isSemiring : IsSemiring _∧_ _∨_ ⊤ ⊥ -∧-∨-isSemiring = record - { isSemiringWithoutAnnihilatingZero = record - { +-isCommutativeMonoid = ∧-⊤-isCommutativeMonoid - ; *-isMonoid = ∨-⊥-isMonoid - ; distrib = ∨-∧-distrib - } - ; zero = ∨-zero - } - -∨-∧-isCommutativeSemiring : IsCommutativeSemiring _∨_ _∧_ ⊥ ⊤ -∨-∧-isCommutativeSemiring = record - { isSemiring = ∨-∧-isSemiring - ; *-comm = ∧-comm - } - -∧-∨-isCommutativeSemiring : IsCommutativeSemiring _∧_ _∨_ ⊤ ⊥ -∧-∨-isCommutativeSemiring = record - { isSemiring = ∧-∨-isSemiring - ; *-comm = ∨-comm - } - -∨-∧-commutativeSemiring : CommutativeSemiring _ _ -∨-∧-commutativeSemiring = record - { isCommutativeSemiring = ∨-∧-isCommutativeSemiring - } - -∧-∨-commutativeSemiring : CommutativeSemiring _ _ -∧-∨-commutativeSemiring = record - { isCommutativeSemiring = ∧-∨-isCommutativeSemiring - } - ------------------------------------------------------------------------- --- Some other properties - --- I took the statement of this lemma (called Uniqueness of --- Complements) from some course notes, "Boolean Algebra", written --- by Gert Smolka. - -private - lemma : ∀ x y → x ∧ y ≈ ⊥ → x ∨ y ≈ ⊤ → ¬ x ≈ y - lemma x y x∧y=⊥ x∨y=⊤ = begin - ¬ x ≈˘⟨ ∧-identityʳ _ ⟩ - ¬ x ∧ ⊤ ≈˘⟨ ∧-congˡ x∨y=⊤ ⟩ - ¬ x ∧ (x ∨ y) ≈⟨ ∧-∨-distribˡ _ _ _ ⟩ - ¬ x ∧ x ∨ ¬ x ∧ y ≈⟨ ∨-congʳ $ ∧-complementˡ _ ⟩ - ⊥ ∨ ¬ x ∧ y ≈˘⟨ ∨-congʳ x∧y=⊥ ⟩ - x ∧ y ∨ ¬ x ∧ y ≈˘⟨ ∧-∨-distribʳ _ _ _ ⟩ - (x ∨ ¬ x) ∧ y ≈⟨ ∧-congʳ $ ∨-complementʳ _ ⟩ - ⊤ ∧ y ≈⟨ ∧-identityˡ _ ⟩ - y ∎ - -⊥≉⊤ : ¬ ⊥ ≈ ⊤ -⊥≉⊤ = lemma ⊥ ⊤ (∧-identityʳ _) (∨-zeroʳ _) - -⊤≉⊥ : ¬ ⊤ ≈ ⊥ -⊤≉⊥ = lemma ⊤ ⊥ (∧-zeroʳ _) (∨-identityʳ _) - -¬-involutive : Involutive ¬_ -¬-involutive x = lemma (¬ x) x (∧-complementˡ _) (∨-complementˡ _) - -deMorgan₁ : ∀ x y → ¬ (x ∧ y) ≈ ¬ x ∨ ¬ y -deMorgan₁ x y = lemma (x ∧ y) (¬ x ∨ ¬ y) lem₁ lem₂ - where - lem₁ = begin - (x ∧ y) ∧ (¬ x ∨ ¬ y) ≈⟨ ∧-∨-distribˡ _ _ _ ⟩ - (x ∧ y) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y ≈⟨ ∨-congʳ $ ∧-congʳ $ ∧-comm _ _ ⟩ - (y ∧ x) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y ≈⟨ ∧-assoc _ _ _ ⟨ ∨-cong ⟩ ∧-assoc _ _ _ ⟩ - y ∧ (x ∧ ¬ x) ∨ x ∧ (y ∧ ¬ y) ≈⟨ (∧-congˡ $ ∧-complementʳ _) ⟨ ∨-cong ⟩ - (∧-congˡ $ ∧-complementʳ _) ⟩ - (y ∧ ⊥) ∨ (x ∧ ⊥) ≈⟨ ∧-zeroʳ _ ⟨ ∨-cong ⟩ ∧-zeroʳ _ ⟩ - ⊥ ∨ ⊥ ≈⟨ ∨-identityʳ _ ⟩ - ⊥ ∎ - - lem₃ = begin - (x ∧ y) ∨ ¬ x ≈⟨ ∨-∧-distribʳ _ _ _ ⟩ - (x ∨ ¬ x) ∧ (y ∨ ¬ x) ≈⟨ ∧-congʳ $ ∨-complementʳ _ ⟩ - ⊤ ∧ (y ∨ ¬ x) ≈⟨ ∧-identityˡ _ ⟩ - y ∨ ¬ x ≈⟨ ∨-comm _ _ ⟩ - ¬ x ∨ y ∎ - - lem₂ = begin - (x ∧ y) ∨ (¬ x ∨ ¬ y) ≈˘⟨ ∨-assoc _ _ _ ⟩ - ((x ∧ y) ∨ ¬ x) ∨ ¬ y ≈⟨ ∨-congʳ lem₃ ⟩ - (¬ x ∨ y) ∨ ¬ y ≈⟨ ∨-assoc _ _ _ ⟩ - ¬ x ∨ (y ∨ ¬ y) ≈⟨ ∨-congˡ $ ∨-complementʳ _ ⟩ - ¬ x ∨ ⊤ ≈⟨ ∨-zeroʳ _ ⟩ - ⊤ ∎ - -deMorgan₂ : ∀ x y → ¬ (x ∨ y) ≈ ¬ x ∧ ¬ y -deMorgan₂ x y = begin - ¬ (x ∨ y) ≈˘⟨ ¬-cong $ ((¬-involutive _) ⟨ ∨-cong ⟩ (¬-involutive _)) ⟩ - ¬ (¬ ¬ x ∨ ¬ ¬ y) ≈˘⟨ ¬-cong $ deMorgan₁ _ _ ⟩ - ¬ ¬ (¬ x ∧ ¬ y) ≈⟨ ¬-involutive _ ⟩ - ¬ x ∧ ¬ y ∎ - ------------------------------------------------------------------------- --- (⊕, ∧, id, ⊥, ⊤) is a commutative ring - --- This construction is parameterised over the definition of xor. - -module XorRing - (xor : Op₂ Carrier) - (⊕-def : ∀ x y → xor x y ≈ (x ∨ y) ∧ ¬ (x ∧ y)) - where - - private - infixl 6 _⊕_ - - _⊕_ : Op₂ Carrier - _⊕_ = xor - - helper : ∀ {x y u v} → x ≈ y → u ≈ v → x ∧ ¬ u ≈ y ∧ ¬ v - helper x≈y u≈v = x≈y ⟨ ∧-cong ⟩ ¬-cong u≈v - - ⊕-cong : Congruent₂ _⊕_ - ⊕-cong {x} {y} {u} {v} x≈y u≈v = begin - x ⊕ u ≈⟨ ⊕-def _ _ ⟩ - (x ∨ u) ∧ ¬ (x ∧ u) ≈⟨ helper (x≈y ⟨ ∨-cong ⟩ u≈v) - (x≈y ⟨ ∧-cong ⟩ u≈v) ⟩ - (y ∨ v) ∧ ¬ (y ∧ v) ≈˘⟨ ⊕-def _ _ ⟩ - y ⊕ v ∎ - - ⊕-comm : Commutative _⊕_ - ⊕-comm x y = begin - x ⊕ y ≈⟨ ⊕-def _ _ ⟩ - (x ∨ y) ∧ ¬ (x ∧ y) ≈⟨ helper (∨-comm _ _) (∧-comm _ _) ⟩ - (y ∨ x) ∧ ¬ (y ∧ x) ≈˘⟨ ⊕-def _ _ ⟩ - y ⊕ x ∎ - - ¬-distribˡ-⊕ : ∀ x y → ¬ (x ⊕ y) ≈ ¬ x ⊕ y - ¬-distribˡ-⊕ x y = begin - ¬ (x ⊕ y) ≈⟨ ¬-cong $ ⊕-def _ _ ⟩ - ¬ ((x ∨ y) ∧ (¬ (x ∧ y))) ≈⟨ ¬-cong (∧-∨-distribʳ _ _ _) ⟩ - ¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (x ∧ y))) ≈⟨ ¬-cong $ ∨-congˡ $ ∧-congˡ $ ¬-cong (∧-comm _ _) ⟩ - ¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (y ∧ x))) ≈⟨ ¬-cong $ lem _ _ ⟨ ∨-cong ⟩ lem _ _ ⟩ - ¬ ((x ∧ ¬ y) ∨ (y ∧ ¬ x)) ≈⟨ deMorgan₂ _ _ ⟩ - ¬ (x ∧ ¬ y) ∧ ¬ (y ∧ ¬ x) ≈⟨ ∧-congʳ $ deMorgan₁ _ _ ⟩ - (¬ x ∨ (¬ ¬ y)) ∧ ¬ (y ∧ ¬ x) ≈⟨ helper (∨-congˡ $ ¬-involutive _) (∧-comm _ _) ⟩ - (¬ x ∨ y) ∧ ¬ (¬ x ∧ y) ≈˘⟨ ⊕-def _ _ ⟩ - ¬ x ⊕ y ∎ - where - lem : ∀ x y → x ∧ ¬ (x ∧ y) ≈ x ∧ ¬ y - lem x y = begin - x ∧ ¬ (x ∧ y) ≈⟨ ∧-congˡ $ deMorgan₁ _ _ ⟩ - x ∧ (¬ x ∨ ¬ y) ≈⟨ ∧-∨-distribˡ _ _ _ ⟩ - (x ∧ ¬ x) ∨ (x ∧ ¬ y) ≈⟨ ∨-congʳ $ ∧-complementʳ _ ⟩ - ⊥ ∨ (x ∧ ¬ y) ≈⟨ ∨-identityˡ _ ⟩ - x ∧ ¬ y ∎ - - ¬-distribʳ-⊕ : ∀ x y → ¬ (x ⊕ y) ≈ x ⊕ ¬ y - ¬-distribʳ-⊕ x y = begin - ¬ (x ⊕ y) ≈⟨ ¬-cong $ ⊕-comm _ _ ⟩ - ¬ (y ⊕ x) ≈⟨ ¬-distribˡ-⊕ _ _ ⟩ - ¬ y ⊕ x ≈⟨ ⊕-comm _ _ ⟩ - x ⊕ ¬ y ∎ - - ⊕-annihilates-¬ : ∀ x y → x ⊕ y ≈ ¬ x ⊕ ¬ y - ⊕-annihilates-¬ x y = begin - x ⊕ y ≈˘⟨ ¬-involutive _ ⟩ - ¬ ¬ (x ⊕ y) ≈⟨ ¬-cong $ ¬-distribˡ-⊕ _ _ ⟩ - ¬ (¬ x ⊕ y) ≈⟨ ¬-distribʳ-⊕ _ _ ⟩ - ¬ x ⊕ ¬ y ∎ - - ⊕-identityˡ : LeftIdentity ⊥ _⊕_ - ⊕-identityˡ x = begin - ⊥ ⊕ x ≈⟨ ⊕-def _ _ ⟩ - (⊥ ∨ x) ∧ ¬ (⊥ ∧ x) ≈⟨ helper (∨-identityˡ _) (∧-zeroˡ _) ⟩ - x ∧ ¬ ⊥ ≈⟨ ∧-congˡ ⊥≉⊤ ⟩ - x ∧ ⊤ ≈⟨ ∧-identityʳ _ ⟩ - x ∎ - - ⊕-identityʳ : RightIdentity ⊥ _⊕_ - ⊕-identityʳ _ = ⊕-comm _ _ ⟨ trans ⟩ ⊕-identityˡ _ - - ⊕-identity : Identity ⊥ _⊕_ - ⊕-identity = ⊕-identityˡ , ⊕-identityʳ - - ⊕-inverseˡ : LeftInverse ⊥ id _⊕_ - ⊕-inverseˡ x = begin - x ⊕ x ≈⟨ ⊕-def _ _ ⟩ - (x ∨ x) ∧ ¬ (x ∧ x) ≈⟨ helper (∨-idempotent _) (∧-idempotent _) ⟩ - x ∧ ¬ x ≈⟨ ∧-complementʳ _ ⟩ - ⊥ ∎ - - ⊕-inverseʳ : RightInverse ⊥ id _⊕_ - ⊕-inverseʳ _ = ⊕-comm _ _ ⟨ trans ⟩ ⊕-inverseˡ _ - - ⊕-inverse : Inverse ⊥ id _⊕_ - ⊕-inverse = ⊕-inverseˡ , ⊕-inverseʳ - - ∧-distribˡ-⊕ : _∧_ DistributesOverˡ _⊕_ - ∧-distribˡ-⊕ x y z = begin - x ∧ (y ⊕ z) ≈⟨ ∧-congˡ $ ⊕-def _ _ ⟩ - x ∧ ((y ∨ z) ∧ ¬ (y ∧ z)) ≈˘⟨ ∧-assoc _ _ _ ⟩ - (x ∧ (y ∨ z)) ∧ ¬ (y ∧ z) ≈⟨ ∧-congˡ $ deMorgan₁ _ _ ⟩ - (x ∧ (y ∨ z)) ∧ - (¬ y ∨ ¬ z) ≈˘⟨ ∨-identityˡ _ ⟩ - ⊥ ∨ - ((x ∧ (y ∨ z)) ∧ - (¬ y ∨ ¬ z)) ≈⟨ ∨-congʳ lem₃ ⟩ - ((x ∧ (y ∨ z)) ∧ ¬ x) ∨ - ((x ∧ (y ∨ z)) ∧ - (¬ y ∨ ¬ z)) ≈˘⟨ ∧-∨-distribˡ _ _ _ ⟩ - (x ∧ (y ∨ z)) ∧ - (¬ x ∨ (¬ y ∨ ¬ z)) ≈˘⟨ ∧-congˡ $ ∨-congˡ (deMorgan₁ _ _) ⟩ - (x ∧ (y ∨ z)) ∧ - (¬ x ∨ ¬ (y ∧ z)) ≈˘⟨ ∧-congˡ (deMorgan₁ _ _) ⟩ - (x ∧ (y ∨ z)) ∧ - ¬ (x ∧ (y ∧ z)) ≈⟨ helper refl lem₁ ⟩ - (x ∧ (y ∨ z)) ∧ - ¬ ((x ∧ y) ∧ (x ∧ z)) ≈⟨ ∧-congʳ $ ∧-∨-distribˡ _ _ _ ⟩ - ((x ∧ y) ∨ (x ∧ z)) ∧ - ¬ ((x ∧ y) ∧ (x ∧ z)) ≈˘⟨ ⊕-def _ _ ⟩ - (x ∧ y) ⊕ (x ∧ z) ∎ - where - lem₂ = begin - x ∧ (y ∧ z) ≈˘⟨ ∧-assoc _ _ _ ⟩ - (x ∧ y) ∧ z ≈⟨ ∧-congʳ $ ∧-comm _ _ ⟩ - (y ∧ x) ∧ z ≈⟨ ∧-assoc _ _ _ ⟩ - y ∧ (x ∧ z) ∎ - - lem₁ = begin - x ∧ (y ∧ z) ≈˘⟨ ∧-congʳ (∧-idempotent _) ⟩ - (x ∧ x) ∧ (y ∧ z) ≈⟨ ∧-assoc _ _ _ ⟩ - x ∧ (x ∧ (y ∧ z)) ≈⟨ ∧-congˡ lem₂ ⟩ - x ∧ (y ∧ (x ∧ z)) ≈˘⟨ ∧-assoc _ _ _ ⟩ - (x ∧ y) ∧ (x ∧ z) ∎ - - lem₃ = begin - ⊥ ≈˘⟨ ∧-zeroʳ _ ⟩ - (y ∨ z) ∧ ⊥ ≈˘⟨ ∧-congˡ (∧-complementʳ _) ⟩ - (y ∨ z) ∧ (x ∧ ¬ x) ≈˘⟨ ∧-assoc _ _ _ ⟩ - ((y ∨ z) ∧ x) ∧ ¬ x ≈⟨ ∧-comm _ _ ⟨ ∧-cong ⟩ refl ⟩ - (x ∧ (y ∨ z)) ∧ ¬ x ∎ - - ∧-distribʳ-⊕ : _∧_ DistributesOverʳ _⊕_ - ∧-distribʳ-⊕ = comm+distrˡ⇒distrʳ ⊕-cong ∧-comm ∧-distribˡ-⊕ - - ∧-distrib-⊕ : _∧_ DistributesOver _⊕_ - ∧-distrib-⊕ = ∧-distribˡ-⊕ , ∧-distribʳ-⊕ - - private - - lemma₂ : ∀ x y u v → - (x ∧ y) ∨ (u ∧ v) ≈ - ((x ∨ u) ∧ (y ∨ u)) ∧ - ((x ∨ v) ∧ (y ∨ v)) - lemma₂ x y u v = begin - (x ∧ y) ∨ (u ∧ v) ≈⟨ ∨-∧-distribˡ _ _ _ ⟩ - ((x ∧ y) ∨ u) ∧ ((x ∧ y) ∨ v) ≈⟨ ∨-∧-distribʳ _ _ _ - ⟨ ∧-cong ⟩ - ∨-∧-distribʳ _ _ _ ⟩ - ((x ∨ u) ∧ (y ∨ u)) ∧ - ((x ∨ v) ∧ (y ∨ v)) ∎ - - ⊕-assoc : Associative _⊕_ - ⊕-assoc x y z = sym $ begin - x ⊕ (y ⊕ z) ≈⟨ refl ⟨ ⊕-cong ⟩ ⊕-def _ _ ⟩ - x ⊕ ((y ∨ z) ∧ ¬ (y ∧ z)) ≈⟨ ⊕-def _ _ ⟩ - (x ∨ ((y ∨ z) ∧ ¬ (y ∧ z))) ∧ - ¬ (x ∧ ((y ∨ z) ∧ ¬ (y ∧ z))) ≈⟨ lem₃ ⟨ ∧-cong ⟩ lem₄ ⟩ - (((x ∨ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)) ∧ - (((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z)) ≈⟨ ∧-assoc _ _ _ ⟩ - ((x ∨ y) ∨ z) ∧ - (((x ∨ ¬ y) ∨ ¬ z) ∧ - (((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z))) ≈⟨ ∧-congˡ lem₅ ⟩ - ((x ∨ y) ∨ z) ∧ - (((¬ x ∨ ¬ y) ∨ z) ∧ - (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z))) ≈˘⟨ ∧-assoc _ _ _ ⟩ - (((x ∨ y) ∨ z) ∧ ((¬ x ∨ ¬ y) ∨ z)) ∧ - (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z)) ≈⟨ lem₁ ⟨ ∧-cong ⟩ lem₂ ⟩ - (((x ∨ y) ∧ ¬ (x ∧ y)) ∨ z) ∧ - ¬ (((x ∨ y) ∧ ¬ (x ∧ y)) ∧ z) ≈˘⟨ ⊕-def _ _ ⟩ - ((x ∨ y) ∧ ¬ (x ∧ y)) ⊕ z ≈˘⟨ ⊕-def _ _ ⟨ ⊕-cong ⟩ refl ⟩ - (x ⊕ y) ⊕ z ∎ - where - lem₁ = begin - ((x ∨ y) ∨ z) ∧ ((¬ x ∨ ¬ y) ∨ z) ≈˘⟨ ∨-∧-distribʳ _ _ _ ⟩ - ((x ∨ y) ∧ (¬ x ∨ ¬ y)) ∨ z ≈˘⟨ ∨-congʳ $ ∧-congˡ (deMorgan₁ _ _) ⟩ - ((x ∨ y) ∧ ¬ (x ∧ y)) ∨ z ∎ - - lem₂′ = begin - (x ∨ ¬ y) ∧ (¬ x ∨ y) ≈˘⟨ ∧-identityˡ _ ⟨ ∧-cong ⟩ ∧-identityʳ _ ⟩ - (⊤ ∧ (x ∨ ¬ y)) ∧ ((¬ x ∨ y) ∧ ⊤) ≈˘⟨ (∨-complementˡ _ ⟨ ∧-cong ⟩ ∨-comm _ _) - ⟨ ∧-cong ⟩ - (∧-congˡ $ ∨-complementˡ _) ⟩ - ((¬ x ∨ x) ∧ (¬ y ∨ x)) ∧ - ((¬ x ∨ y) ∧ (¬ y ∨ y)) ≈˘⟨ lemma₂ _ _ _ _ ⟩ - (¬ x ∧ ¬ y) ∨ (x ∧ y) ≈˘⟨ deMorgan₂ _ _ ⟨ ∨-cong ⟩ ¬-involutive _ ⟩ - ¬ (x ∨ y) ∨ ¬ ¬ (x ∧ y) ≈˘⟨ deMorgan₁ _ _ ⟩ - ¬ ((x ∨ y) ∧ ¬ (x ∧ y)) ∎ - - lem₂ = begin - ((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z) ≈˘⟨ ∨-∧-distribʳ _ _ _ ⟩ - ((x ∨ ¬ y) ∧ (¬ x ∨ y)) ∨ ¬ z ≈⟨ ∨-congʳ lem₂′ ⟩ - ¬ ((x ∨ y) ∧ ¬ (x ∧ y)) ∨ ¬ z ≈˘⟨ deMorgan₁ _ _ ⟩ - ¬ (((x ∨ y) ∧ ¬ (x ∧ y)) ∧ z) ∎ - - lem₃ = begin - x ∨ ((y ∨ z) ∧ ¬ (y ∧ z)) ≈⟨ ∨-congˡ $ ∧-congˡ $ deMorgan₁ _ _ ⟩ - x ∨ ((y ∨ z) ∧ (¬ y ∨ ¬ z)) ≈⟨ ∨-∧-distribˡ _ _ _ ⟩ - (x ∨ (y ∨ z)) ∧ (x ∨ (¬ y ∨ ¬ z)) ≈˘⟨ ∨-assoc _ _ _ ⟨ ∧-cong ⟩ ∨-assoc _ _ _ ⟩ - ((x ∨ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z) ∎ - - lem₄′ = begin - ¬ ((y ∨ z) ∧ ¬ (y ∧ z)) ≈⟨ deMorgan₁ _ _ ⟩ - ¬ (y ∨ z) ∨ ¬ ¬ (y ∧ z) ≈⟨ deMorgan₂ _ _ ⟨ ∨-cong ⟩ ¬-involutive _ ⟩ - (¬ y ∧ ¬ z) ∨ (y ∧ z) ≈⟨ lemma₂ _ _ _ _ ⟩ - ((¬ y ∨ y) ∧ (¬ z ∨ y)) ∧ - ((¬ y ∨ z) ∧ (¬ z ∨ z)) ≈⟨ (∨-complementˡ _ ⟨ ∧-cong ⟩ ∨-comm _ _) - ⟨ ∧-cong ⟩ - (∧-congˡ $ ∨-complementˡ _) ⟩ - (⊤ ∧ (y ∨ ¬ z)) ∧ - ((¬ y ∨ z) ∧ ⊤) ≈⟨ ∧-identityˡ _ ⟨ ∧-cong ⟩ ∧-identityʳ _ ⟩ - (y ∨ ¬ z) ∧ (¬ y ∨ z) ∎ - - lem₄ = begin - ¬ (x ∧ ((y ∨ z) ∧ ¬ (y ∧ z))) ≈⟨ deMorgan₁ _ _ ⟩ - ¬ x ∨ ¬ ((y ∨ z) ∧ ¬ (y ∧ z)) ≈⟨ ∨-congˡ lem₄′ ⟩ - ¬ x ∨ ((y ∨ ¬ z) ∧ (¬ y ∨ z)) ≈⟨ ∨-∧-distribˡ _ _ _ ⟩ - (¬ x ∨ (y ∨ ¬ z)) ∧ - (¬ x ∨ (¬ y ∨ z)) ≈˘⟨ ∨-assoc _ _ _ ⟨ ∧-cong ⟩ ∨-assoc _ _ _ ⟩ - ((¬ x ∨ y) ∨ ¬ z) ∧ - ((¬ x ∨ ¬ y) ∨ z) ≈⟨ ∧-comm _ _ ⟩ - ((¬ x ∨ ¬ y) ∨ z) ∧ - ((¬ x ∨ y) ∨ ¬ z) ∎ - - lem₅ = begin - ((x ∨ ¬ y) ∨ ¬ z) ∧ - (((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z)) ≈˘⟨ ∧-assoc _ _ _ ⟩ - (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ ¬ y) ∨ z)) ∧ - ((¬ x ∨ y) ∨ ¬ z) ≈⟨ ∧-congʳ $ ∧-comm _ _ ⟩ - (((¬ x ∨ ¬ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)) ∧ - ((¬ x ∨ y) ∨ ¬ z) ≈⟨ ∧-assoc _ _ _ ⟩ - ((¬ x ∨ ¬ y) ∨ z) ∧ - (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z)) ∎ - - ⊕-isMagma : IsMagma _⊕_ - ⊕-isMagma = record - { isEquivalence = isEquivalence - ; ∙-cong = ⊕-cong - } - - ⊕-isSemigroup : IsSemigroup _⊕_ - ⊕-isSemigroup = record - { isMagma = ⊕-isMagma - ; assoc = ⊕-assoc - } - - ⊕-⊥-isMonoid : IsMonoid _⊕_ ⊥ - ⊕-⊥-isMonoid = record - { isSemigroup = ⊕-isSemigroup - ; identity = ⊕-identity - } - - ⊕-⊥-isGroup : IsGroup _⊕_ ⊥ id - ⊕-⊥-isGroup = record - { isMonoid = ⊕-⊥-isMonoid - ; inverse = ⊕-inverse - ; ⁻¹-cong = id - } - - ⊕-⊥-isAbelianGroup : IsAbelianGroup _⊕_ ⊥ id - ⊕-⊥-isAbelianGroup = record - { isGroup = ⊕-⊥-isGroup - ; comm = ⊕-comm - } - - ⊕-∧-isRing : IsRing _⊕_ _∧_ id ⊥ ⊤ - ⊕-∧-isRing = record - { +-isAbelianGroup = ⊕-⊥-isAbelianGroup - ; *-isMonoid = ∧-⊤-isMonoid - ; distrib = ∧-distrib-⊕ - ; zero = ∧-zero - } - - ⊕-∧-isCommutativeRing : IsCommutativeRing _⊕_ _∧_ id ⊥ ⊤ - ⊕-∧-isCommutativeRing = record - { isRing = ⊕-∧-isRing - ; *-comm = ∧-comm - } - - ⊕-∧-commutativeRing : CommutativeRing _ _ - ⊕-∧-commutativeRing = record - { isCommutativeRing = ⊕-∧-isCommutativeRing - } - - ⊕-¬-distribˡ = ¬-distribˡ-⊕ - {-# WARNING_ON_USAGE ⊕-¬-distribˡ - "Warning: ⊕-¬-distribˡ was deprecated in v1.1. - Please use ¬-distribˡ-⊕ instead." - #-} - ⊕-¬-distribʳ = ¬-distribʳ-⊕ - {-# WARNING_ON_USAGE ⊕-¬-distribʳ - "Warning: ⊕-¬-distribʳ was deprecated in v1.1. - Please use ¬-distribʳ-⊕ instead." - #-} - isCommutativeRing = ⊕-∧-isCommutativeRing - {-# WARNING_ON_USAGE isCommutativeRing - "Warning: isCommutativeRing was deprecated in v1.1. - Please use ⊕-∧-isCommutativeRing instead." - #-} - commutativeRing = ⊕-∧-commutativeRing - {-# WARNING_ON_USAGE commutativeRing - "Warning: commutativeRing was deprecated in v1.1. - Please use ⊕-∧-commutativeRing instead." - #-} - - -infixl 6 _⊕_ - -_⊕_ : Op₂ Carrier -x ⊕ y = (x ∨ y) ∧ ¬ (x ∧ y) - -module DefaultXorRing = XorRing _⊕_ (λ _ _ → refl) - - ------------------------------------------------------------------------ -- DEPRECATED NAMES ------------------------------------------------------------------------ @@ -598,11 +57,11 @@ replace-equality : {_≈′_ : Rel Carrier b₂} → (∀ {x y} → x ≈ y ⇔ (x ≈′ y)) → BooleanAlgebra _ _ replace-equality {_≈′_} ≈⇔≈′ = record - { isBooleanAlgebra = record + { isBooleanAlgebra = record { isDistributiveLattice = DistributiveLattice.isDistributiveLattice (DistribLatticeProperties.replace-equality distributiveLattice ≈⇔≈′) - ; ∨-complementʳ = λ x → to ⟨$⟩ ∨-complementʳ x - ; ∧-complementʳ = λ x → to ⟨$⟩ ∧-complementʳ x + ; ∨-complement = ((λ x → to ⟨$⟩ ∨-complementˡ x) , λ x → to ⟨$⟩ ∨-complementʳ x) + ; ∧-complement = ((λ x → to ⟨$⟩ ∧-complementˡ x) , λ x → to ⟨$⟩ ∧-complementʳ x) ; ¬-cong = λ i≈j → to ⟨$⟩ ¬-cong (from ⟨$⟩ i≈j) } } where open module E {x y} = Equivalence (≈⇔≈′ {x} {y}) diff --git a/src/Algebra/Properties/BooleanAlgebra/Expression.agda b/src/Algebra/Properties/BooleanAlgebra/Expression.agda index 6297e65220..2394765c8b 100644 --- a/src/Algebra/Properties/BooleanAlgebra/Expression.agda +++ b/src/Algebra/Properties/BooleanAlgebra/Expression.agda @@ -1,185 +1,20 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Boolean algebra expressions +-- This module is DEPRECATED. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} -open import Algebra +open import Algebra.Lattice module Algebra.Properties.BooleanAlgebra.Expression {b} (B : BooleanAlgebra b b) where -open BooleanAlgebra B +{-# WARNING_ON_IMPORT +"Algebra.Properties.BooleanAlgebra.Expression was deprecated in v2.0. +Use Algebra.Lattice.Properties.BooleanAlgebra.Expression instead." +#-} -open import Category.Applicative -import Category.Applicative.Indexed as Applicative -open import Category.Monad -open import Data.Fin.Base using (Fin) -open import Data.Nat.Base -open import Data.Product using (_,_; proj₁; proj₂) -open import Data.Vec.Base as Vec using (Vec) -import Data.Vec.Categorical as VecCat -import Function.Identity.Categorical as IdCat -open import Data.Vec.Properties using (lookup-map) -open import Data.Vec.Relation.Binary.Pointwise.Extensional as PW - using (Pointwise; ext) -open import Function -open import Relation.Binary.PropositionalEquality as P using (_≗_) -import Relation.Binary.Reflection as Reflection - --- Expressions made up of variables and the operations of a boolean --- algebra. - -infixr 7 _and_ -infixr 6 _or_ - -data Expr n : Set b where - var : (x : Fin n) → Expr n - _or_ _and_ : (e₁ e₂ : Expr n) → Expr n - not : (e : Expr n) → Expr n - top bot : Expr n - --- The semantics of an expression, parametrised by an applicative --- functor. - -module Semantics - {F : Set b → Set b} - (A : RawApplicative F) - where - - open RawApplicative A - - ⟦_⟧ : ∀ {n} → Expr n → Vec (F Carrier) n → F Carrier - ⟦ var x ⟧ ρ = Vec.lookup ρ x - ⟦ e₁ or e₂ ⟧ ρ = pure _∨_ ⊛ ⟦ e₁ ⟧ ρ ⊛ ⟦ e₂ ⟧ ρ - ⟦ e₁ and e₂ ⟧ ρ = pure _∧_ ⊛ ⟦ e₁ ⟧ ρ ⊛ ⟦ e₂ ⟧ ρ - ⟦ not e ⟧ ρ = pure ¬_ ⊛ ⟦ e ⟧ ρ - ⟦ top ⟧ ρ = pure ⊤ - ⟦ bot ⟧ ρ = pure ⊥ - --- flip Semantics.⟦_⟧ e is natural. - -module Naturality - {F₁ F₂ : Set b → Set b} - {A₁ : RawApplicative F₁} - {A₂ : RawApplicative F₂} - (f : Applicative.Morphism A₁ A₂) - where - - open P.≡-Reasoning - open Applicative.Morphism f - open Semantics A₁ renaming (⟦_⟧ to ⟦_⟧₁) - open Semantics A₂ renaming (⟦_⟧ to ⟦_⟧₂) - open RawApplicative A₁ renaming (pure to pure₁; _⊛_ to _⊛₁_) - open RawApplicative A₂ renaming (pure to pure₂; _⊛_ to _⊛₂_) - - natural : ∀ {n} (e : Expr n) → op ∘ ⟦ e ⟧₁ ≗ ⟦ e ⟧₂ ∘ Vec.map op - natural (var x) ρ = begin - op (Vec.lookup ρ x) ≡⟨ P.sym $ lookup-map x op ρ ⟩ - Vec.lookup (Vec.map op ρ) x ∎ - natural (e₁ or e₂) ρ = begin - op (pure₁ _∨_ ⊛₁ ⟦ e₁ ⟧₁ ρ ⊛₁ ⟦ e₂ ⟧₁ ρ) ≡⟨ op-⊛ _ _ ⟩ - op (pure₁ _∨_ ⊛₁ ⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (op-⊛ _ _) P.refl ⟩ - op (pure₁ _∨_) ⊛₂ op (⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (P.cong₂ _⊛₂_ (op-pure _) (natural e₁ ρ)) - (natural e₂ ρ) ⟩ - pure₂ _∨_ ⊛₂ ⟦ e₁ ⟧₂ (Vec.map op ρ) ⊛₂ ⟦ e₂ ⟧₂ (Vec.map op ρ) ∎ - natural (e₁ and e₂) ρ = begin - op (pure₁ _∧_ ⊛₁ ⟦ e₁ ⟧₁ ρ ⊛₁ ⟦ e₂ ⟧₁ ρ) ≡⟨ op-⊛ _ _ ⟩ - op (pure₁ _∧_ ⊛₁ ⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (op-⊛ _ _) P.refl ⟩ - op (pure₁ _∧_) ⊛₂ op (⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (P.cong₂ _⊛₂_ (op-pure _) (natural e₁ ρ)) - (natural e₂ ρ) ⟩ - pure₂ _∧_ ⊛₂ ⟦ e₁ ⟧₂ (Vec.map op ρ) ⊛₂ ⟦ e₂ ⟧₂ (Vec.map op ρ) ∎ - natural (not e) ρ = begin - op (pure₁ ¬_ ⊛₁ ⟦ e ⟧₁ ρ) ≡⟨ op-⊛ _ _ ⟩ - op (pure₁ ¬_) ⊛₂ op (⟦ e ⟧₁ ρ) ≡⟨ P.cong₂ _⊛₂_ (op-pure _) (natural e ρ) ⟩ - pure₂ ¬_ ⊛₂ ⟦ e ⟧₂ (Vec.map op ρ) ∎ - natural top ρ = begin - op (pure₁ ⊤) ≡⟨ op-pure _ ⟩ - pure₂ ⊤ ∎ - natural bot ρ = begin - op (pure₁ ⊥) ≡⟨ op-pure _ ⟩ - pure₂ ⊥ ∎ - --- An example of how naturality can be used: Any boolean algebra can --- be lifted, in a pointwise manner, to vectors of carrier elements. - -lift : ℕ → BooleanAlgebra b b -lift n = record - { Carrier = Vec Carrier n - ; _≈_ = Pointwise _≈_ - ; _∨_ = zipWith _∨_ - ; _∧_ = zipWith _∧_ - ; ¬_ = map ¬_ - ; ⊤ = pure ⊤ - ; ⊥ = pure ⊥ - ; isBooleanAlgebra = record - { isDistributiveLattice = record - { isLattice = record - { isEquivalence = PW.isEquivalence isEquivalence - ; ∨-comm = λ _ _ → ext λ i → - solve i 2 (λ x y → x or y , y or x) - (∨-comm _ _) _ _ - ; ∨-assoc = λ _ _ _ → ext λ i → - solve i 3 - (λ x y z → (x or y) or z , x or (y or z)) - (∨-assoc _ _ _) _ _ _ - ; ∨-cong = λ xs≈us ys≈vs → ext λ i → - solve₁ i 4 (λ x y u v → x or y , u or v) - _ _ _ _ - (∨-cong (Pointwise.app xs≈us i) - (Pointwise.app ys≈vs i)) - ; ∧-comm = λ _ _ → ext λ i → - solve i 2 (λ x y → x and y , y and x) - (∧-comm _ _) _ _ - ; ∧-assoc = λ _ _ _ → ext λ i → - solve i 3 - (λ x y z → (x and y) and z , - x and (y and z)) - (∧-assoc _ _ _) _ _ _ - ; ∧-cong = λ xs≈ys us≈vs → ext λ i → - solve₁ i 4 (λ x y u v → x and y , u and v) - _ _ _ _ - (∧-cong (Pointwise.app xs≈ys i) - (Pointwise.app us≈vs i)) - ; absorptive = - (λ _ _ → ext λ i → - solve i 2 (λ x y → x or (x and y) , x) (∨-absorbs-∧ _ _) _ _) , - (λ _ _ → ext λ i → - solve i 2 (λ x y → x and (x or y) , x) (∧-absorbs-∨ _ _) _ _) - } - ; ∨-distribʳ-∧ = λ _ _ _ → ext λ i → - solve i 3 - (λ x y z → (y and z) or x , - (y or x) and (z or x)) - (∨-∧-distribʳ _ _ _) _ _ _ - } - ; ∨-complementʳ = λ _ → ext λ i → - solve i 1 (λ x → x or (not x) , top) - (∨-complementʳ _) _ - ; ∧-complementʳ = λ _ → ext λ i → - solve i 1 (λ x → x and (not x) , bot) - (∧-complementʳ _) _ - ; ¬-cong = λ xs≈ys → ext λ i → - solve₁ i 2 (λ x y → not x , not y) _ _ - (¬-cong (Pointwise.app xs≈ys i)) - } - } - where - open RawApplicative VecCat.applicative - using (pure; zipWith) renaming (_<$>_ to map) - - ⟦_⟧Id : ∀ {n} → Expr n → Vec Carrier n → Carrier - ⟦_⟧Id = Semantics.⟦_⟧ IdCat.applicative - - ⟦_⟧Vec : ∀ {m n} → Expr n → Vec (Vec Carrier m) n → Vec Carrier m - ⟦_⟧Vec = Semantics.⟦_⟧ VecCat.applicative - - open module R {n} (i : Fin n) = - Reflection setoid var - (λ e ρ → Vec.lookup (⟦ e ⟧Vec ρ) i) - (λ e ρ → ⟦ e ⟧Id (Vec.map (flip Vec.lookup i) ρ)) - (λ e ρ → sym $ reflexive $ - Naturality.natural (VecCat.lookup-morphism i) e ρ) +open import Algebra.Lattice.Properties.BooleanAlgebra.Expression diff --git a/src/Algebra/Properties/DistributiveLattice.agda b/src/Algebra/Properties/DistributiveLattice.agda index af0a9912d1..a9bc518886 100644 --- a/src/Algebra/Properties/DistributiveLattice.agda +++ b/src/Algebra/Properties/DistributiveLattice.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Some derivable properties +-- This module is DEPRECATED. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} @@ -9,74 +9,25 @@ -- Disabled to prevent warnings from deprecated names {-# OPTIONS --warn=noUserWarning #-} -open import Algebra.Bundles +open import Algebra.Lattice.Bundles +open import Algebra.Lattice.Structures.Biased +open import Relation.Binary +open import Function.Equality +open import Function.Equivalence +import Algebra.Construct.Subst.Equality as SubstEq module Algebra.Properties.DistributiveLattice - {dl₁ dl₂} (DL : DistributiveLattice dl₁ dl₂) + {ℓ₁ ℓ₂} (DL : DistributiveLattice ℓ₁ ℓ₂) where +{-# WARNING_ON_IMPORT +"Algebra.Properties.DistributiveLattice was deprecated in v2.0. +Use Algebra.Lattice.Properties.DistributiveLattice instead." +#-} + open DistributiveLattice DL +open import Algebra.Lattice.Properties.DistributiveLattice DL public import Algebra.Properties.Lattice as LatticeProperties -open import Algebra.Structures -open import Algebra.Definitions _≈_ -open import Relation.Binary -open import Relation.Binary.Reasoning.Setoid setoid -open import Function.Base -open import Function.Equality using (_⟨$⟩_) -open import Function.Equivalence using (_⇔_; module Equivalence) -open import Data.Product using (_,_) - ------------------------------------------------------------------------- --- Export properties of lattices - -open LatticeProperties lattice public - hiding (replace-equality) - ------------------------------------------------------------------------- --- Other properties - -∨-distribˡ-∧ : _∨_ DistributesOverˡ _∧_ -∨-distribˡ-∧ x y z = begin - x ∨ y ∧ z ≈⟨ ∨-comm _ _ ⟩ - y ∧ z ∨ x ≈⟨ ∨-distribʳ-∧ _ _ _ ⟩ - (y ∨ x) ∧ (z ∨ x) ≈⟨ ∨-comm _ _ ⟨ ∧-cong ⟩ ∨-comm _ _ ⟩ - (x ∨ y) ∧ (x ∨ z) ∎ - -∨-distrib-∧ : _∨_ DistributesOver _∧_ -∨-distrib-∧ = ∨-distribˡ-∧ , ∨-distribʳ-∧ - -∧-distribˡ-∨ : _∧_ DistributesOverˡ _∨_ -∧-distribˡ-∨ x y z = begin - x ∧ (y ∨ z) ≈⟨ ∧-congʳ $ sym (∧-absorbs-∨ _ _) ⟩ - (x ∧ (x ∨ y)) ∧ (y ∨ z) ≈⟨ ∧-congʳ $ ∧-congˡ $ ∨-comm _ _ ⟩ - (x ∧ (y ∨ x)) ∧ (y ∨ z) ≈⟨ ∧-assoc _ _ _ ⟩ - x ∧ ((y ∨ x) ∧ (y ∨ z)) ≈⟨ ∧-congˡ $ sym (∨-distribˡ-∧ _ _ _) ⟩ - x ∧ (y ∨ x ∧ z) ≈⟨ ∧-congʳ $ sym (∨-absorbs-∧ _ _) ⟩ - (x ∨ x ∧ z) ∧ (y ∨ x ∧ z) ≈⟨ sym $ ∨-distribʳ-∧ _ _ _ ⟩ - x ∧ y ∨ x ∧ z ∎ - -∧-distribʳ-∨ : _∧_ DistributesOverʳ _∨_ -∧-distribʳ-∨ x y z = begin - (y ∨ z) ∧ x ≈⟨ ∧-comm _ _ ⟩ - x ∧ (y ∨ z) ≈⟨ ∧-distribˡ-∨ _ _ _ ⟩ - x ∧ y ∨ x ∧ z ≈⟨ ∧-comm _ _ ⟨ ∨-cong ⟩ ∧-comm _ _ ⟩ - y ∧ x ∨ z ∧ x ∎ - -∧-distrib-∨ : _∧_ DistributesOver _∨_ -∧-distrib-∨ = ∧-distribˡ-∨ , ∧-distribʳ-∨ - --- The dual construction is also a distributive lattice. - -∧-∨-isDistributiveLattice : IsDistributiveLattice _≈_ _∧_ _∨_ -∧-∨-isDistributiveLattice = record - { isLattice = ∧-∨-isLattice - ; ∨-distribʳ-∧ = ∧-distribʳ-∨ - } - -∧-∨-distributiveLattice : DistributiveLattice _ _ -∧-∨-distributiveLattice = record - { isDistributiveLattice = ∧-∨-isDistributiveLattice - } ------------------------------------------------------------------------ -- DEPRECATED NAMES @@ -114,15 +65,15 @@ Please use ∧-distrib-∨ instead." -- Version 1.4 -replace-equality : {_≈′_ : Rel Carrier dl₂} → +replace-equality : {_≈′_ : Rel Carrier ℓ₂} → (∀ {x y} → x ≈ y ⇔ (x ≈′ y)) → DistributiveLattice _ _ replace-equality {_≈′_} ≈⇔≈′ = record - { isDistributiveLattice = record + { isDistributiveLattice = isDistributiveLatticeʳʲᵐ (record { isLattice = Lattice.isLattice (LatticeProperties.replace-equality lattice ≈⇔≈′) ; ∨-distribʳ-∧ = λ x y z → to ⟨$⟩ ∨-distribʳ-∧ x y z - } + }) } where open module E {x y} = Equivalence (≈⇔≈′ {x} {y}) {-# WARNING_ON_USAGE replace-equality "Warning: replace-equality was deprecated in v1.4. diff --git a/src/Algebra/Properties/Lattice.agda b/src/Algebra/Properties/Lattice.agda index 7973a3bced..ee23dac578 100644 --- a/src/Algebra/Properties/Lattice.agda +++ b/src/Algebra/Properties/Lattice.agda @@ -1,183 +1,28 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Some derivable properties +-- This module is DEPRECATED. Please use +-- `Algebra.Lattice.Properties.Lattice` instead. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} -open import Algebra.Bundles - -module Algebra.Properties.Lattice {l₁ l₂} (L : Lattice l₁ l₂) where - -open Lattice L -open import Algebra.Structures _≈_ -open import Algebra.Definitions _≈_ -import Algebra.Properties.Semilattice as SemilatticeProperties +open import Algebra.Lattice.Bundles open import Relation.Binary -import Relation.Binary.Lattice as R -open import Relation.Binary.Reasoning.Setoid setoid open import Function.Base open import Function.Equality using (_⟨$⟩_) open import Function.Equivalence using (_⇔_; module Equivalence) open import Data.Product using (_,_; swap) ------------------------------------------------------------------------- --- _∧_ is a semilattice - -∧-idem : Idempotent _∧_ -∧-idem x = begin - x ∧ x ≈⟨ ∧-congˡ (sym (∨-absorbs-∧ _ _)) ⟩ - x ∧ (x ∨ x ∧ x) ≈⟨ ∧-absorbs-∨ _ _ ⟩ - x ∎ - -∧-isMagma : IsMagma _∧_ -∧-isMagma = record - { isEquivalence = isEquivalence - ; ∙-cong = ∧-cong - } - -∧-isSemigroup : IsSemigroup _∧_ -∧-isSemigroup = record - { isMagma = ∧-isMagma - ; assoc = ∧-assoc - } - -∧-isBand : IsBand _∧_ -∧-isBand = record - { isSemigroup = ∧-isSemigroup - ; idem = ∧-idem - } - -∧-isSemilattice : IsSemilattice _∧_ -∧-isSemilattice = record - { isBand = ∧-isBand - ; comm = ∧-comm - } - -∧-semilattice : Semilattice l₁ l₂ -∧-semilattice = record - { isSemilattice = ∧-isSemilattice - } - -open SemilatticeProperties ∧-semilattice public - using - ( ∧-isOrderTheoreticMeetSemilattice - ; ∧-isOrderTheoreticJoinSemilattice - ; ∧-orderTheoreticMeetSemilattice - ; ∧-orderTheoreticJoinSemilattice - ) - ------------------------------------------------------------------------- --- _∨_ is a semilattice - -∨-idem : Idempotent _∨_ -∨-idem x = begin - x ∨ x ≈⟨ ∨-congˡ (sym (∧-idem _)) ⟩ - x ∨ x ∧ x ≈⟨ ∨-absorbs-∧ _ _ ⟩ - x ∎ - -∨-isMagma : IsMagma _∨_ -∨-isMagma = record - { isEquivalence = isEquivalence - ; ∙-cong = ∨-cong - } - -∨-isSemigroup : IsSemigroup _∨_ -∨-isSemigroup = record - { isMagma = ∨-isMagma - ; assoc = ∨-assoc - } - -∨-isBand : IsBand _∨_ -∨-isBand = record - { isSemigroup = ∨-isSemigroup - ; idem = ∨-idem - } - -∨-isSemilattice : IsSemilattice _∨_ -∨-isSemilattice = record - { isBand = ∨-isBand - ; comm = ∨-comm - } - -∨-semilattice : Semilattice l₁ l₂ -∨-semilattice = record - { isSemilattice = ∨-isSemilattice - } - -open SemilatticeProperties ∨-semilattice public - using () - renaming - ( ∧-isOrderTheoreticMeetSemilattice to ∨-isOrderTheoreticMeetSemilattice - ; ∧-isOrderTheoreticJoinSemilattice to ∨-isOrderTheoreticJoinSemilattice - ; ∧-orderTheoreticMeetSemilattice to ∨-orderTheoreticMeetSemilattice - ; ∧-orderTheoreticJoinSemilattice to ∨-orderTheoreticJoinSemilattice - ) - ------------------------------------------------------------------------- --- The dual construction is also a lattice. - -∧-∨-isLattice : IsLattice _∧_ _∨_ -∧-∨-isLattice = record - { isEquivalence = isEquivalence - ; ∨-comm = ∧-comm - ; ∨-assoc = ∧-assoc - ; ∨-cong = ∧-cong - ; ∧-comm = ∨-comm - ; ∧-assoc = ∨-assoc - ; ∧-cong = ∨-cong - ; absorptive = swap absorptive - } - -∧-∨-lattice : Lattice _ _ -∧-∨-lattice = record - { isLattice = ∧-∨-isLattice - } - ------------------------------------------------------------------------- --- Every algebraic lattice can be turned into an order-theoretic one. - -open SemilatticeProperties ∧-semilattice public using (poset) -open Poset poset using (_≤_; isPartialOrder) - -∨-∧-isOrderTheoreticLattice : R.IsLattice _≈_ _≤_ _∨_ _∧_ -∨-∧-isOrderTheoreticLattice = record - { isPartialOrder = isPartialOrder - ; supremum = supremum - ; infimum = infimum - } - where - open R.MeetSemilattice ∧-orderTheoreticMeetSemilattice using (infimum) - open R.JoinSemilattice ∨-orderTheoreticJoinSemilattice using (x≤x∨y; y≤x∨y; ∨-least) - renaming (_≤_ to _≤′_) - - -- An alternative but equivalent interpretation of the order _≤_. - - sound : ∀ {x y} → x ≤′ y → x ≤ y - sound {x} {y} y≈y∨x = sym $ begin - x ∧ y ≈⟨ ∧-congˡ y≈y∨x ⟩ - x ∧ (y ∨ x) ≈⟨ ∧-congˡ (∨-comm y x) ⟩ - x ∧ (x ∨ y) ≈⟨ ∧-absorbs-∨ x y ⟩ - x ∎ +module Algebra.Properties.Lattice {l₁ l₂} (L : Lattice l₁ l₂) where - complete : ∀ {x y} → x ≤ y → x ≤′ y - complete {x} {y} x≈x∧y = sym $ begin - y ∨ x ≈⟨ ∨-congˡ x≈x∧y ⟩ - y ∨ (x ∧ y) ≈⟨ ∨-congˡ (∧-comm x y) ⟩ - y ∨ (y ∧ x) ≈⟨ ∨-absorbs-∧ y x ⟩ - y ∎ +open import Algebra.Lattice.Properties.Lattice L public - supremum : R.Supremum _≤_ _∨_ - supremum x y = - sound (x≤x∨y x y) , - sound (y≤x∨y x y) , - λ z x≤z y≤z → sound (∨-least (complete x≤z) (complete y≤z)) +{-# WARNING_ON_IMPORT +"Algebra.Properties.Lattice was deprecated in v2.0. +Use Algebra.Lattice.Properties.Lattice instead." +#-} -∨-∧-orderTheoreticLattice : R.Lattice _ _ _ -∨-∧-orderTheoreticLattice = record - { isLattice = ∨-∧-isOrderTheoreticLattice - } ------------------------------------------------------------------------ -- DEPRECATED NAMES @@ -185,6 +30,8 @@ open Poset poset using (_≤_; isPartialOrder) -- Please use the new names as continuing support for the old names is -- not guaranteed. +open Lattice L + -- Version 1.1 ∧-idempotent = ∧-idem diff --git a/src/Algebra/Properties/Semilattice.agda b/src/Algebra/Properties/Semilattice.agda index e95994e450..1ebe9c26a9 100644 --- a/src/Algebra/Properties/Semilattice.agda +++ b/src/Algebra/Properties/Semilattice.agda @@ -1,63 +1,22 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Some derivable properties +-- This module is DEPRECATED. Please use +-- `Algebra.Lattice.Properties.Semilattice` instead. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} -open import Algebra +open import Algebra.Lattice module Algebra.Properties.Semilattice {c ℓ} (L : Semilattice c ℓ) where -open Semilattice L - -open import Algebra.Structures -open import Function -open import Data.Product -open import Relation.Binary -open import Relation.Binary.Reasoning.Setoid setoid -import Relation.Binary.Construct.NaturalOrder.Left _≈_ _∧_ as LeftNaturalOrder -open import Relation.Binary.Lattice -import Relation.Binary.Properties.Poset as PosetProperties -open import Relation.Binary.Reasoning.Setoid setoid - ------------------------------------------------------------------------- --- Every semilattice can be turned into a poset via the left natural --- order. - -poset : Poset c ℓ ℓ -poset = LeftNaturalOrder.poset isSemilattice - -open Poset poset using (_≤_; isPartialOrder) -open PosetProperties poset using (_≥_; ≥-isPartialOrder) - ------------------------------------------------------------------------- --- Every algebraic semilattice can be turned into an order-theoretic one. - -∧-isOrderTheoreticMeetSemilattice : IsMeetSemilattice _≈_ _≤_ _∧_ -∧-isOrderTheoreticMeetSemilattice = record - { isPartialOrder = isPartialOrder - ; infimum = LeftNaturalOrder.infimum isSemilattice - } - -∧-isOrderTheoreticJoinSemilattice : IsJoinSemilattice _≈_ _≥_ _∧_ -∧-isOrderTheoreticJoinSemilattice = record - { isPartialOrder = ≥-isPartialOrder - ; supremum = IsMeetSemilattice.infimum - ∧-isOrderTheoreticMeetSemilattice - } - -∧-orderTheoreticMeetSemilattice : MeetSemilattice c ℓ ℓ -∧-orderTheoreticMeetSemilattice = record - { isMeetSemilattice = ∧-isOrderTheoreticMeetSemilattice - } - -∧-orderTheoreticJoinSemilattice : JoinSemilattice c ℓ ℓ -∧-orderTheoreticJoinSemilattice = record - { isJoinSemilattice = ∧-isOrderTheoreticJoinSemilattice - } +open import Algebra.Lattice.Properties.Semilattice L public +{-# WARNING_ON_IMPORT +"Algebra.Properties.Semilattice was deprecated in v2.0. +Use Algebra.Lattice.Properties.Semilattice instead." +#-} ------------------------------------------------------------------------ -- DEPRECATED NAMES diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 2827a55264..1deeec46a8 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -1,8 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Some algebraic structures (not packed up with sets, operations, --- etc.) +-- Some algebraic structures (not packed up with sets, operations, etc.) ------------------------------------------------------------------------ -- The contents of this module should be accessed via `Algebra`, unless @@ -92,17 +91,6 @@ record IsCommutativeSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ) where ; comm = comm } - -record IsSemilattice (∧ : Op₂ A) : Set (a ⊔ ℓ) where - field - isBand : IsBand ∧ - comm : Commutative ∧ - - open IsBand isBand public - renaming (∙-cong to ∧-cong; ∙-congˡ to ∧-congˡ; ∙-congʳ to ∧-congʳ) - - - ------------------------------------------------------------------------ -- Structures with 1 binary operation & 1 element ------------------------------------------------------------------------ @@ -166,17 +154,8 @@ record IsIdempotentCommutativeMonoid (∙ : Op₂ A) open IsCommutativeMonoid isCommutativeMonoid public - --- Idempotent commutative monoids are also known as bounded lattices. --- Note that the BoundedLattice necessarily uses the notation inherited --- from monoids rather than lattices. - -IsBoundedLattice = IsIdempotentCommutativeMonoid - -module IsBoundedLattice {∙ : Op₂ A} - {ε : A} - (isIdemCommMonoid : IsIdempotentCommutativeMonoid ∙ ε) = - IsIdempotentCommutativeMonoid isIdemCommMonoid + isBand : IsBand ∙ + isBand = record { isSemigroup = isSemigroup ; idem = idem } ------------------------------------------------------------------------ @@ -274,62 +253,6 @@ record IsAbelianGroup (∙ : Op₂ A) using (isCommutativeMagma; isCommutativeSemigroup) ------------------------------------------------------------------------- --- Structures with 2 binary operations ------------------------------------------------------------------------- - --- Note that `IsLattice` is not defined in terms of `IsSemilattice` --- because the idempotence laws of ∨ and ∧ can be derived from the --- absorption laws, which makes the corresponding "idem" fields --- redundant. The derived idempotence laws are stated and proved in --- `Algebra.Properties.Lattice` along with the fact that every lattice --- consists of two semilattices. - -record IsLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where - field - isEquivalence : IsEquivalence _≈_ - ∨-comm : Commutative ∨ - ∨-assoc : Associative ∨ - ∨-cong : Congruent₂ ∨ - ∧-comm : Commutative ∧ - ∧-assoc : Associative ∧ - ∧-cong : Congruent₂ ∧ - absorptive : Absorptive ∨ ∧ - - open IsEquivalence isEquivalence public - - ∨-absorbs-∧ : ∨ Absorbs ∧ - ∨-absorbs-∧ = proj₁ absorptive - - ∧-absorbs-∨ : ∧ Absorbs ∨ - ∧-absorbs-∨ = proj₂ absorptive - - ∧-congˡ : LeftCongruent ∧ - ∧-congˡ y≈z = ∧-cong refl y≈z - - ∧-congʳ : RightCongruent ∧ - ∧-congʳ y≈z = ∧-cong y≈z refl - - ∨-congˡ : LeftCongruent ∨ - ∨-congˡ y≈z = ∨-cong refl y≈z - - ∨-congʳ : RightCongruent ∨ - ∨-congʳ y≈z = ∨-cong y≈z refl - - -record IsDistributiveLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where - field - isLattice : IsLattice ∨ ∧ - ∨-distribʳ-∧ : ∨ DistributesOverʳ ∧ - - open IsLattice isLattice public - - ∨-∧-distribʳ = ∨-distribʳ-∧ - {-# WARNING_ON_USAGE ∨-∧-distribʳ - "Warning: ∨-∧-distribʳ was deprecated in v1.1. - Please use ∨-distribʳ-∧ instead." - #-} - ------------------------------------------------------------------------ -- Structures with 2 binary operations & 1 element ------------------------------------------------------------------------ @@ -627,13 +550,3 @@ record IsCommutativeRing ; *-isCommutativeMonoid ) - -record IsBooleanAlgebra - (∨ ∧ : Op₂ A) (¬ : Op₁ A) (⊤ ⊥ : A) : Set (a ⊔ ℓ) where - field - isDistributiveLattice : IsDistributiveLattice ∨ ∧ - ∨-complementʳ : RightInverse ⊤ ¬ ∨ - ∧-complementʳ : RightInverse ⊥ ¬ ∧ - ¬-cong : Congruent₁ ¬ - - open IsDistributiveLattice isDistributiveLattice public diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda index 73715aac76..e8801d3e3b 100644 --- a/src/Data/Bool/Properties.agda +++ b/src/Data/Bool/Properties.agda @@ -9,6 +9,8 @@ module Data.Bool.Properties where open import Algebra.Bundles +open import Algebra.Lattice.Bundles +import Algebra.Lattice.Properties.BooleanAlgebra as BooleanAlgebraProperties open import Data.Bool.Base open import Data.Empty open import Data.Product @@ -26,6 +28,8 @@ import Relation.Unary as U open import Algebra.Definitions {A = Bool} _≡_ open import Algebra.Structures {A = Bool} _≡_ +open import Algebra.Lattice.Structures {A = Bool} _≡_ + open ≡-Reasoning private @@ -569,8 +573,9 @@ true