84 lines
3.1 KiB
Agda
84 lines
3.1 KiB
Agda
|
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}
|
|||
|
|
}
|