summaryrefslogtreecommitdiff
path: root/src/Helium/Algebra/Decidable
diff options
context:
space:
mode:
Diffstat (limited to 'src/Helium/Algebra/Decidable')
-rw-r--r--src/Helium/Algebra/Decidable/Bundles.agda108
-rw-r--r--src/Helium/Algebra/Decidable/Construct/Pointwise.agda93
-rw-r--r--src/Helium/Algebra/Decidable/Structures.agda87
3 files changed, 288 insertions, 0 deletions
diff --git a/src/Helium/Algebra/Decidable/Bundles.agda b/src/Helium/Algebra/Decidable/Bundles.agda
new file mode 100644
index 0000000..e446706
--- /dev/null
+++ b/src/Helium/Algebra/Decidable/Bundles.agda
@@ -0,0 +1,108 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Definitions of decidable algebraic structures like monoids and rings
+-- (packed in records together with sets, operations, etc.)
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Helium.Algebra.Decidable.Bundles where
+
+open import Algebra.Bundles using (RawLattice)
+open import Algebra.Core
+open import Helium.Algebra.Decidable.Structures
+open import Level using (suc; _⊔_)
+open import Relation.Binary.Bundles using (DecSetoid)
+open import Relation.Binary.Core using (Rel)
+
+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)
+
+ decSetoid : DecSetoid _ _
+ decSetoid = record { isDecEquivalence = isDecEquivalence }
+
+ open DecSetoid decSetoid public
+ using (_≉_; setoid)
+
+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; decSetoid; ∨-rawMagma; ∧-rawMagma; rawLattice)
+
+record RawBooleanAlgebra 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
+
+ rawLattice : RawLattice c ℓ
+ rawLattice = record { _≈_ = _≈_; _∨_ = _∨_; _∧_ = _∧_ }
+
+ open RawLattice rawLattice public
+ using (_≉_; ∨-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; decSetoid; ∨-rawMagma; ∧-rawMagma; rawLattice; lattice)
diff --git a/src/Helium/Algebra/Decidable/Construct/Pointwise.agda b/src/Helium/Algebra/Decidable/Construct/Pointwise.agda
new file mode 100644
index 0000000..9f067ba
--- /dev/null
+++ b/src/Helium/Algebra/Decidable/Construct/Pointwise.agda
@@ -0,0 +1,93 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Construct algebras of vectors in a pointwise manner
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+module Helium.Algebra.Decidable.Construct.Pointwise where
+
+open import Algebra.Bundles using (RawLattice)
+open import Algebra.Core
+open import Data.Nat using (ℕ)
+open import Data.Product using (_,_)
+open import Data.Vec.Functional using (replicate; map; zipWith)
+open import Data.Vec.Functional.Relation.Binary.Pointwise using (Pointwise)
+import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as Pwₚ
+open import Function using (_$_)
+open import Helium.Algebra.Decidable.Bundles
+open import Helium.Algebra.Decidable.Structures
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Core using (Rel)
+
+module _ {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} where
+ private
+ _≋_ = Pointwise _≈_
+
+ module _ {∨ ∧ : Op₂ A} where
+ isLattice : IsLattice _≈_ ∨ ∧ → ∀ n → IsLattice (_≋_ {n}) (zipWith ∨) (zipWith ∧)
+ isLattice L n = record
+ { isDecEquivalence = Pwₚ.isDecEquivalence isDecEquivalence n
+ ; ∨-comm = λ x y i → ∨-comm (x i) (y i)
+ ; ∨-assoc = λ x y z i → ∨-assoc (x i) (y i) (z i)
+ ; ∨-cong = λ x≈y u≈v i → ∨-cong (x≈y i) (u≈v i)
+ ; ∧-comm = λ x y i → ∧-comm (x i) (y i)
+ ; ∧-assoc = λ x y z i → ∧-assoc (x i) (y i) (z i)
+ ; ∧-cong = λ x≈y u≈v i → ∧-cong (x≈y i) (u≈v i)
+ ; absorptive = (λ x y i → ∨-absorbs-∧ (x i) (y i))
+ , (λ x y i → ∧-absorbs-∨ (x i) (y i))
+ }
+ where open IsLattice L
+
+ isDistributiveLattice : IsDistributiveLattice _≈_ ∨ ∧ → ∀ n → IsDistributiveLattice (_≋_ {n}) (zipWith ∨) (zipWith ∧)
+ isDistributiveLattice L n = record
+ { isLattice = isLattice L.isLattice n
+ ; ∨-distrib-∧ = (λ x y z i → L.∨-distribˡ-∧ (x i) (y i) (z i))
+ , (λ x y z i → L.∨-distribʳ-∧ (x i) (y i) (z i))
+ }
+ where module L = IsDistributiveLattice L
+
+ module _ {∨ ∧ : Op₂ A} {¬ : Op₁ A} {⊤ ⊥ : A} where
+ isBooleanAlgebra : IsBooleanAlgebra _≈_ ∨ ∧ ¬ ⊤ ⊥ → ∀ n → IsBooleanAlgebra (_≋_ {n}) (zipWith ∨) (zipWith ∧) (map ¬) (replicate ⊤) (replicate ⊥)
+ isBooleanAlgebra B n = record
+ { isDistributiveLattice = isDistributiveLattice B.isDistributiveLattice n
+ ; ∨-complement = (λ x i → B.∨-complementˡ (x i))
+ , (λ x i → B.∨-complementʳ (x i))
+ ; ∧-complement = (λ x i → B.∧-complementˡ (x i))
+ , (λ x i → B.∧-complementʳ (x i))
+ ; ¬-cong = λ x≈y i → B.¬-cong (x≈y i)
+ }
+ where module B = IsBooleanAlgebra B
+
+rawLattice : ∀ {a ℓ} → RawLattice a ℓ → ℕ → RawLattice a ℓ
+rawLattice L n = record
+ { _≈_ = Pointwise _≈_ {n}
+ ; _∧_ = zipWith _∧_
+ ; _∨_ = zipWith _∨_
+ }
+ where open RawLattice L
+
+lattice : ∀ {a ℓ} → Lattice a ℓ → ℕ → Lattice a ℓ
+lattice L n = record { isLattice = isLattice (Lattice.isLattice L) n }
+
+distributiveLattice : ∀ {a ℓ} → DistributiveLattice a ℓ → ℕ → DistributiveLattice a ℓ
+distributiveLattice L n = record
+ { isDistributiveLattice =
+ isDistributiveLattice (DistributiveLattice.isDistributiveLattice L) n
+ }
+
+rawBooleanAlgebra : ∀ {a ℓ} → RawBooleanAlgebra a ℓ → ℕ → RawBooleanAlgebra a ℓ
+rawBooleanAlgebra B n = record
+ { _≈_ = Pointwise _≈_ {n}
+ ; _∧_ = zipWith _∧_
+ ; _∨_ = zipWith _∨_
+ ; ¬_ = map ¬_
+ ; ⊤ = replicate ⊤
+ ; ⊥ = replicate ⊥
+ }
+ where open RawBooleanAlgebra B
+
+booleanAlgebra : ∀ {a ℓ} → BooleanAlgebra a ℓ → ℕ → BooleanAlgebra a ℓ
+booleanAlgebra B n = record
+ { isBooleanAlgebra = isBooleanAlgebra (BooleanAlgebra.isBooleanAlgebra B) n }
diff --git a/src/Helium/Algebra/Decidable/Structures.agda b/src/Helium/Algebra/Decidable/Structures.agda
new file mode 100644
index 0000000..4380cc5
--- /dev/null
+++ b/src/Helium/Algebra/Decidable/Structures.agda
@@ -0,0 +1,87 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Some decidable algebraic structures (not packed up with sets,
+-- operations, etc.)
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary.Core using (Rel)
+
+module Helium.Algebra.Decidable.Structures
+ {a ℓ} {A : Set a} -- The underlying set
+ (_≈_ : Rel A ℓ) -- The underlying equality relation
+ where
+
+open import Algebra.Core
+open import Algebra.Definitions (_≈_)
+open import Data.Product using (proj₁; proj₂)
+open import Level using (_⊔_)
+open import Relation.Binary.Structures using (IsDecEquivalence)
+
+record IsLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
+ field
+ isDecEquivalence : IsDecEquivalence _≈_
+ ∨-comm : Commutative ∨
+ ∨-assoc : Associative ∨
+ ∨-cong : Congruent₂ ∨
+ ∧-comm : Commutative ∧
+ ∧-assoc : Associative ∧
+ ∧-cong : Congruent₂ ∧
+ absorptive : Absorptive ∨ ∧
+
+ open IsDecEquivalence isDecEquivalence 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ˡ-∧ : ∨ DistributesOverˡ ∧
+ ∨-distribˡ-∧ = proj₁ ∨-distrib-∧
+
+ ∨-distribʳ-∧ : ∨ DistributesOverʳ ∧
+ ∨-distribʳ-∧ = proj₂ ∨-distrib-∧
+
+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
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 10:22:19 +0000