107 lines
3.0 KiB
Agda
107 lines
3.0 KiB
Agda
|
module Lattice.Unit where
|
|||
|
|
|
|||
|
|
open import Data.Empty using (⊥-elim)
|
|||
|
|
open import Data.Product using (_,_)
|
|||
|
|
open import Data.Nat using (ℕ; _≤_; z≤n)
|
|||
|
|
open import Data.Unit using (⊤; tt)
|
|||
|
|
open import Data.Unit.Properties using (_≟_; ≡-setoid)
|
|||
|
|
open import Relation.Binary using (Setoid)
|
|||
|
|
open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
|
|||
|
|
open import Relation.Nullary using (Dec; ¬_; yes; no)
|
|||
|
|
open import Equivalence
|
|||
|
|
open import Lattice
|
|||
|
|
import Chain
|
|||
|
|
|
|||
|
|
open Setoid ≡-setoid using (refl; sym; trans)
|
|||
|
|
|
|||
|
|
_≈_ : ⊤ → ⊤ → Set
|
|||
|
|
_≈_ = _≡_
|
|||
|
|
|
|||
|
|
≈-equiv : IsEquivalence ⊤ _≈_
|
|||
|
|
≈-equiv = record
|
|||
|
|
{ ≈-refl = refl
|
|||
|
|
; ≈-sym = sym
|
|||
|
|
; ≈-trans = trans
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
≈-dec : IsDecidable _≈_
|
|||
|
|
≈-dec = _≟_
|
|||
|
|
|
|||
|
|
_⊔_ : ⊤ → ⊤ → ⊤
|
|||
|
|
tt ⊔ tt = tt
|
|||
|
|
|
|||
|
|
_⊓_ : ⊤ → ⊤ → ⊤
|
|||
|
|
tt ⊓ tt = tt
|
|||
|
|
|
|||
|
|
≈-⊔-cong : ∀ {ab₁ ab₂ ab₃ ab₄} → ab₁ ≈ ab₂ → ab₃ ≈ ab₄ → (ab₁ ⊔ ab₃) ≈ (ab₂ ⊔ ab₄)
|
|||
|
|
≈-⊔-cong {tt} {tt} {tt} {tt} _ _ = Eq.refl
|
|||
|
|
|
|||
|
|
⊔-assoc : (x y z : ⊤) → ((x ⊔ y) ⊔ z) ≈ (x ⊔ (y ⊔ z))
|
|||
|
|
⊔-assoc tt tt tt = Eq.refl
|
|||
|
|
|
|||
|
|
⊔-comm : (x y : ⊤) → (x ⊔ y) ≈ (y ⊔ x)
|
|||
|
|
⊔-comm tt tt = Eq.refl
|
|||
|
|
|
|||
|
|
⊔-idemp : (x : ⊤) → (x ⊔ x) ≈ x
|
|||
|
|
⊔-idemp tt = Eq.refl
|
|||
|
|
|
|||
|
|
isJoinSemilattice : IsSemilattice ⊤ _≈_ _⊔_
|
|||
|
|
isJoinSemilattice = record
|
|||
|
|
{ ≈-equiv = ≈-equiv
|
|||
|
|
; ≈-⊔-cong = ≈-⊔-cong
|
|||
|
|
; ⊔-assoc = ⊔-assoc
|
|||
|
|
; ⊔-comm = ⊔-comm
|
|||
|
|
; ⊔-idemp = ⊔-idemp
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
≈-⊓-cong : ∀ {ab₁ ab₂ ab₃ ab₄} → ab₁ ≈ ab₂ → ab₃ ≈ ab₄ → (ab₁ ⊓ ab₃) ≈ (ab₂ ⊓ ab₄)
|
|||
|
|
≈-⊓-cong {tt} {tt} {tt} {tt} _ _ = Eq.refl
|
|||
|
|
|
|||
|
|
⊓-assoc : (x y z : ⊤) → ((x ⊓ y) ⊓ z) ≈ (x ⊓ (y ⊓ z))
|
|||
|
|
⊓-assoc tt tt tt = Eq.refl
|
|||
|
|
|
|||
|
|
⊓-comm : (x y : ⊤) → (x ⊓ y) ≈ (y ⊓ x)
|
|||
|
|
⊓-comm tt tt = Eq.refl
|
|||
|
|
|
|||
|
|
⊓-idemp : (x : ⊤) → (x ⊓ x) ≈ x
|
|||
|
|
⊓-idemp tt = Eq.refl
|
|||
|
|
|
|||
|
|
isMeetSemilattice : IsSemilattice ⊤ _≈_ _⊓_
|
|||
|
|
isMeetSemilattice = record
|
|||
|
|
{ ≈-equiv = ≈-equiv
|
|||
|
|
; ≈-⊔-cong = ≈-⊓-cong
|
|||
|
|
; ⊔-assoc = ⊓-assoc
|
|||
|
|
; ⊔-comm = ⊓-comm
|
|||
|
|
; ⊔-idemp = ⊓-idemp
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
absorb-⊔-⊓ : (x y : ⊤) → (x ⊔ (x ⊓ y)) ≈ x
|
|||
|
|
absorb-⊔-⊓ tt tt = Eq.refl
|
|||
|
|
|
|||
|
|
absorb-⊓-⊔ : (x y : ⊤) → (x ⊓ (x ⊔ y)) ≈ x
|
|||
|
|
absorb-⊓-⊔ tt tt = Eq.refl
|
|||
|
|
|
|||
|
|
isLattice : IsLattice ⊤ _≈_ _⊔_ _⊓_
|
|||
|
|
isLattice = record
|
|||
|
|
{ joinSemilattice = isJoinSemilattice
|
|||
|
|
; meetSemilattice = isMeetSemilattice
|
|||
|
|
; absorb-⊔-⊓ = absorb-⊔-⊓
|
|||
|
|
; absorb-⊓-⊔ = absorb-⊓-⊔
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
open Chain _≈_ ≈-equiv (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice)
|
|||
|
|
|
|||
|
|
private
|
|||
|
|
longestChain : Chain tt tt 0
|
|||
|
|
longestChain = done refl
|
|||
|
|
|
|||
|
|
isLongest : ∀ {t₁ t₂ : ⊤} {n : ℕ} → Chain t₁ t₂ n → n ≤ 0
|
|||
|
|
isLongest {tt} {tt} (step ((tt , tt⊔tt≈tt) , tt≈tt) _ _) = ⊥-elim (tt≈tt refl)
|
|||
|
|
isLongest (done _) = z≤n
|
|||
|
|
|
|||
|
|
isFiniteHeightLattice : IsFiniteHeightLattice ⊤ 0 _≈_ _⊔_ _⊓_
|
|||
|
|
isFiniteHeightLattice = record
|
|||
|
|
{ isLattice = isLattice
|
|||
|
|
; fixedHeight = (((tt , tt) , longestChain) , isLongest)
|
|||
|
|
}
|