From dce21b369639fcadb5735dd9c1642de283e33dab Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 23 Sep 2023 15:34:59 -0700 Subject: [PATCH] Moved the Nat lattice instance into an actual file Signed-off-by: Danila Fedorin --- Lattice.agda | 83 ------------------------------------------------ Lattice/Nat.agda | 83 ++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 83 insertions(+), 83 deletions(-) create mode 100644 Lattice/Nat.agda diff --git a/Lattice.agda b/Lattice.agda index 731e80c..bdd6a35 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -140,44 +140,6 @@ record Lattice {a} (A : Set a) : Set (lsuc a) where open IsLattice isLattice public module IsSemilatticeInstances where - module ForNat where - open Nat - open NatProps - open Eq - - private - ≡-⊔-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≡ a₂ → a₃ ≡ a₄ → (a₁ ⊔ a₃) ≡ (a₂ ⊔ a₄) - ≡-⊔-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl - - ≡-⊓-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≡ a₂ → a₃ ≡ a₄ → (a₁ ⊓ a₃) ≡ (a₂ ⊓ a₄) - ≡-⊓-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl - - NatIsMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_ - NatIsMaxSemilattice = record - { ≈-equiv = record - { ≈-refl = refl - ; ≈-sym = sym - ; ≈-trans = trans - } - ; ≈-⊔-cong = ≡-⊔-cong - ; ⊔-assoc = ⊔-assoc - ; ⊔-comm = ⊔-comm - ; ⊔-idemp = ⊔-idem - } - - NatIsMinSemilattice : IsSemilattice ℕ _≡_ _⊓_ - NatIsMinSemilattice = record - { ≈-equiv = record - { ≈-refl = refl - ; ≈-sym = sym - ; ≈-trans = trans - } - ; ≈-⊔-cong = ≡-⊓-cong - ; ⊔-assoc = ⊓-assoc - ; ⊔-comm = ⊓-comm - ; ⊔-idemp = ⊓-idem - } - module ForProd {a} {A B : Set a} (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a) (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B) @@ -216,51 +178,6 @@ module IsSemilatticeInstances where } module IsLatticeInstances where - module ForNat where - open Nat - open NatProps - open Eq - open IsSemilatticeInstances.ForNat - open Data.Product - - private - max-bound₁ : {x y z : ℕ} → x ⊔ y ≡ z → x ≤ z - max-bound₁ {x} {y} {z} x⊔y≡z - rewrite sym x⊔y≡z - rewrite ⊔-comm x y = m≤n⇒m≤o⊔n y (≤-refl) - - min-bound₁ : {x y z : ℕ} → x ⊓ y ≡ z → z ≤ x - min-bound₁ {x} {y} {z} x⊓y≡z - rewrite sym x⊓y≡z = m≤n⇒m⊓o≤n y (≤-refl) - - minmax-absorb : {x y : ℕ} → x ⊓ (x ⊔ y) ≡ x - minmax-absorb {x} {y} = ≤-antisym x⊓x⊔y≤x (helper x⊓x≤x⊓x⊔y (⊓-idem x)) - where - x⊓x⊔y≤x = min-bound₁ {x} {x ⊔ y} {x ⊓ (x ⊔ y)} refl - x⊓x≤x⊓x⊔y = ⊓-mono-≤ {x} {x} ≤-refl (max-bound₁ {x} {y} {x ⊔ y} refl) - - -- >:( - helper : x ⊓ x ≤ x ⊓ (x ⊔ y) → x ⊓ x ≡ x → x ≤ x ⊓ (x ⊔ y) - helper x⊓x≤x⊓x⊔y x⊓x≡x rewrite x⊓x≡x = x⊓x≤x⊓x⊔y - - maxmin-absorb : {x y : ℕ} → x ⊔ (x ⊓ y) ≡ x - maxmin-absorb {x} {y} = ≤-antisym (helper x⊔x⊓y≤x⊔x (⊔-idem x)) x≤x⊔x⊓y - where - x≤x⊔x⊓y = max-bound₁ {x} {x ⊓ y} {x ⊔ (x ⊓ y)} refl - x⊔x⊓y≤x⊔x = ⊔-mono-≤ {x} {x} ≤-refl (min-bound₁ {x} {y} {x ⊓ y} refl) - - -- >:( - helper : x ⊔ (x ⊓ y) ≤ x ⊔ x → x ⊔ x ≡ x → x ⊔ (x ⊓ y) ≤ x - helper x⊔x⊓y≤x⊔x x⊔x≡x rewrite x⊔x≡x = x⊔x⊓y≤x⊔x - - NatIsLattice : IsLattice ℕ _≡_ _⊔_ _⊓_ - NatIsLattice = record - { joinSemilattice = NatIsMaxSemilattice - ; meetSemilattice = NatIsMinSemilattice - ; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y} - ; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y} - } - module ForProd {a} {A B : Set a} (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a) (_⊔₁_ : A → A → A) (_⊓₁_ : A → A → A) diff --git a/Lattice/Nat.agda b/Lattice/Nat.agda new file mode 100644 index 0000000..c3f760a --- /dev/null +++ b/Lattice/Nat.agda @@ -0,0 +1,83 @@ +module Lattice.Nat where + +open import Equivalence +open import Lattice +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans) +open import Data.Nat using (ℕ; _⊔_; _⊓_; _≤_) +open import Data.Nat.Properties using + ( ⊔-assoc; ⊔-comm; ⊔-idem + ; ⊓-assoc; ⊓-comm; ⊓-idem + ; ⊓-mono-≤; ⊔-mono-≤ + ; m≤n⇒m≤o⊔n; m≤n⇒m⊓o≤n; ≤-refl; ≤-antisym + ) + +private + ≡-⊔-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≡ a₂ → a₃ ≡ a₄ → (a₁ ⊔ a₃) ≡ (a₂ ⊔ a₄) + ≡-⊔-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl + + ≡-⊓-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≡ a₂ → a₃ ≡ a₄ → (a₁ ⊓ a₃) ≡ (a₂ ⊓ a₄) + ≡-⊓-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl + +NatIsMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_ +NatIsMaxSemilattice = record + { ≈-equiv = record + { ≈-refl = refl + ; ≈-sym = sym + ; ≈-trans = trans + } + ; ≈-⊔-cong = ≡-⊔-cong + ; ⊔-assoc = ⊔-assoc + ; ⊔-comm = ⊔-comm + ; ⊔-idemp = ⊔-idem + } + +NatIsMinSemilattice : IsSemilattice ℕ _≡_ _⊓_ +NatIsMinSemilattice = record + { ≈-equiv = record + { ≈-refl = refl + ; ≈-sym = sym + ; ≈-trans = trans + } + ; ≈-⊔-cong = ≡-⊓-cong + ; ⊔-assoc = ⊓-assoc + ; ⊔-comm = ⊓-comm + ; ⊔-idemp = ⊓-idem + } + +private + max-bound₁ : {x y z : ℕ} → x ⊔ y ≡ z → x ≤ z + max-bound₁ {x} {y} {z} x⊔y≡z + rewrite sym x⊔y≡z + rewrite ⊔-comm x y = m≤n⇒m≤o⊔n y (≤-refl) + + min-bound₁ : {x y z : ℕ} → x ⊓ y ≡ z → z ≤ x + min-bound₁ {x} {y} {z} x⊓y≡z + rewrite sym x⊓y≡z = m≤n⇒m⊓o≤n y (≤-refl) + + minmax-absorb : {x y : ℕ} → x ⊓ (x ⊔ y) ≡ x + minmax-absorb {x} {y} = ≤-antisym x⊓x⊔y≤x (helper x⊓x≤x⊓x⊔y (⊓-idem x)) + where + x⊓x⊔y≤x = min-bound₁ {x} {x ⊔ y} {x ⊓ (x ⊔ y)} refl + x⊓x≤x⊓x⊔y = ⊓-mono-≤ {x} {x} ≤-refl (max-bound₁ {x} {y} {x ⊔ y} refl) + + -- >:( + helper : x ⊓ x ≤ x ⊓ (x ⊔ y) → x ⊓ x ≡ x → x ≤ x ⊓ (x ⊔ y) + helper x⊓x≤x⊓x⊔y x⊓x≡x rewrite x⊓x≡x = x⊓x≤x⊓x⊔y + + maxmin-absorb : {x y : ℕ} → x ⊔ (x ⊓ y) ≡ x + maxmin-absorb {x} {y} = ≤-antisym (helper x⊔x⊓y≤x⊔x (⊔-idem x)) x≤x⊔x⊓y + where + x≤x⊔x⊓y = max-bound₁ {x} {x ⊓ y} {x ⊔ (x ⊓ y)} refl + x⊔x⊓y≤x⊔x = ⊔-mono-≤ {x} {x} ≤-refl (min-bound₁ {x} {y} {x ⊓ y} refl) + + -- >:( + helper : x ⊔ (x ⊓ y) ≤ x ⊔ x → x ⊔ x ≡ x → x ⊔ (x ⊓ y) ≤ x + helper x⊔x⊓y≤x⊔x x⊔x≡x rewrite x⊔x≡x = x⊔x⊓y≤x⊔x + +NatIsLattice : IsLattice ℕ _≡_ _⊔_ _⊓_ +NatIsLattice = record + { joinSemilattice = NatIsMaxSemilattice + ; meetSemilattice = NatIsMinSemilattice + ; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y} + ; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y} + }