From 91bc16d54ec0a6e5d904673951fe091a9973d9b4 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Tue, 18 Jan 2022 22:01:46 +0000
Subject: Define the semantics of pseudocode data types.

---
 src/Helium/Algebra/Decidable/Structures.agda | 87 ++++++++++++++++++++++++++++
 1 file changed, 87 insertions(+)
 create mode 100644 src/Helium/Algebra/Decidable/Structures.agda

(limited to 'src/Helium/Algebra/Decidable/Structures.agda')

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
-- 
cgit v1.2.3