374 lines
17 KiB
Plaintext
374 lines
17 KiB
Plaintext
open import Lattice
|
||
open import Equivalence
|
||
open import Relation.Nullary using (Dec; ¬_; yes; no)
|
||
|
||
module Lattice.AboveBelow {a} (A : Set a)
|
||
(_≈₁_ : A → A → Set a)
|
||
(≈₁-equiv : IsEquivalence A _≈₁_)
|
||
(≈₁-dec : IsDecidable _≈₁_) where
|
||
|
||
open import Data.Empty using (⊥-elim)
|
||
open import Data.Product using (_,_)
|
||
open import Data.Nat using (_≤_; ℕ; z≤n; s≤s; suc)
|
||
open import Function using (_∘_)
|
||
open import Showable using (Showable; show)
|
||
open import Relation.Binary.PropositionalEquality as Eq
|
||
using (_≡_; sym; subst; refl)
|
||
|
||
import Chain
|
||
|
||
open IsEquivalence ≈₁-equiv using ()
|
||
renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
|
||
|
||
data AboveBelow : Set a where
|
||
⊥ : AboveBelow
|
||
⊤ : AboveBelow
|
||
[_] : A → AboveBelow
|
||
|
||
instance
|
||
showable : {{ showableA : Showable A }} → Showable AboveBelow
|
||
showable = record
|
||
{ show = (λ
|
||
{ ⊥ → "⊥"
|
||
; ⊤ → "⊤"
|
||
; [ a ] → show a
|
||
})
|
||
}
|
||
|
||
data _≈_ : AboveBelow → AboveBelow → Set a where
|
||
≈-⊥-⊥ : ⊥ ≈ ⊥
|
||
≈-⊤-⊤ : ⊤ ≈ ⊤
|
||
≈-lift : ∀ {x y : A} → x ≈₁ y → [ x ] ≈ [ y ]
|
||
|
||
≈-refl : ∀ {ab : AboveBelow} → ab ≈ ab
|
||
≈-refl {⊥} = ≈-⊥-⊥
|
||
≈-refl {⊤} = ≈-⊤-⊤
|
||
≈-refl {[ x ]} = ≈-lift ≈₁-refl
|
||
|
||
≈-sym : ∀ {ab₁ ab₂ : AboveBelow} → ab₁ ≈ ab₂ → ab₂ ≈ ab₁
|
||
≈-sym ≈-⊥-⊥ = ≈-⊥-⊥
|
||
≈-sym ≈-⊤-⊤ = ≈-⊤-⊤
|
||
≈-sym (≈-lift x≈₁y) = ≈-lift (≈₁-sym x≈₁y)
|
||
|
||
≈-trans : ∀ {ab₁ ab₂ ab₃ : AboveBelow} → ab₁ ≈ ab₂ → ab₂ ≈ ab₃ → ab₁ ≈ ab₃
|
||
≈-trans ≈-⊥-⊥ ≈-⊥-⊥ = ≈-⊥-⊥
|
||
≈-trans ≈-⊤-⊤ ≈-⊤-⊤ = ≈-⊤-⊤
|
||
≈-trans (≈-lift a₁≈a₂) (≈-lift a₂≈a₃) = ≈-lift (≈₁-trans a₁≈a₂ a₂≈a₃)
|
||
|
||
≈-equiv : IsEquivalence AboveBelow _≈_
|
||
≈-equiv = record
|
||
{ ≈-refl = ≈-refl
|
||
; ≈-sym = ≈-sym
|
||
; ≈-trans = ≈-trans
|
||
}
|
||
|
||
≈-dec : IsDecidable _≈_
|
||
≈-dec ⊥ ⊥ = yes ≈-⊥-⊥
|
||
≈-dec ⊤ ⊤ = yes ≈-⊤-⊤
|
||
≈-dec [ x ] [ y ]
|
||
with ≈₁-dec x y
|
||
... | yes x≈y = yes (≈-lift x≈y)
|
||
... | no x̷≈y = no (λ { (≈-lift x≈y) → x̷≈y x≈y })
|
||
≈-dec ⊤ ⊥ = no λ ()
|
||
≈-dec ⊤ [ x ] = no λ ()
|
||
≈-dec ⊥ ⊤ = no λ ()
|
||
≈-dec ⊥ [ x ] = no λ ()
|
||
≈-dec [ x ] ⊥ = no λ ()
|
||
≈-dec [ x ] ⊤ = no λ ()
|
||
|
||
-- Any object can be wrapped in an 'above below' to make it a lattice,
|
||
-- since ⊤ and ⊥ are the largest and least elements, and the rest are left
|
||
-- unordered. That's what this module does.
|
||
--
|
||
-- For convenience, ask for the underlying type to always be inhabited, to
|
||
-- avoid requiring additional constraints in some of the proofs below.
|
||
module Plain (x : A) where
|
||
_⊔_ : AboveBelow → AboveBelow → AboveBelow
|
||
⊥ ⊔ x = x
|
||
⊤ ⊔ x = ⊤
|
||
[ x ] ⊔ [ y ] with ≈₁-dec x y
|
||
... | yes _ = [ x ]
|
||
... | no _ = ⊤
|
||
x ⊔ ⊥ = x
|
||
x ⊔ ⊤ = ⊤
|
||
|
||
⊤⊔x≡⊤ : ∀ (x : AboveBelow) → ⊤ ⊔ x ≡ ⊤
|
||
⊤⊔x≡⊤ _ = refl
|
||
|
||
x⊔⊤≡⊤ : ∀ (x : AboveBelow) → x ⊔ ⊤ ≡ ⊤
|
||
x⊔⊤≡⊤ ⊤ = refl
|
||
x⊔⊤≡⊤ ⊥ = refl
|
||
x⊔⊤≡⊤ [ x ] = refl
|
||
|
||
⊥⊔x≡x : ∀ (x : AboveBelow) → ⊥ ⊔ x ≡ x
|
||
⊥⊔x≡x _ = refl
|
||
|
||
x⊔⊥≡x : ∀ (x : AboveBelow) → x ⊔ ⊥ ≡ x
|
||
x⊔⊥≡x ⊤ = refl
|
||
x⊔⊥≡x ⊥ = refl
|
||
x⊔⊥≡x [ x ] = refl
|
||
|
||
x≈y⇒[x]⊔[y]≡[x] : ∀ {x y : A} → x ≈₁ y → [ x ] ⊔ [ y ] ≡ [ x ]
|
||
x≈y⇒[x]⊔[y]≡[x] {x} {y} x≈₁y
|
||
with ≈₁-dec x y
|
||
... | yes _ = refl
|
||
... | no x̷≈₁y = ⊥-elim (x̷≈₁y x≈₁y)
|
||
|
||
x̷≈y⇒[x]⊔[y]≡⊤ : ∀ {x y : A} → ¬ x ≈₁ y → [ x ] ⊔ [ y ] ≡ ⊤
|
||
x̷≈y⇒[x]⊔[y]≡⊤ {x} {y} x̷≈₁y
|
||
with ≈₁-dec x y
|
||
... | yes x≈₁y = ⊥-elim (x̷≈₁y x≈₁y)
|
||
... | no x̷≈₁y = refl
|
||
|
||
≈-⊔-cong : ∀ {ab₁ ab₂ ab₃ ab₄} → ab₁ ≈ ab₂ → ab₃ ≈ ab₄ →
|
||
(ab₁ ⊔ ab₃) ≈ (ab₂ ⊔ ab₄)
|
||
≈-⊔-cong ≈-⊤-⊤ ≈-⊤-⊤ = ≈-⊤-⊤
|
||
≈-⊔-cong ≈-⊤-⊤ ≈-⊥-⊥ = ≈-⊤-⊤
|
||
≈-⊔-cong ≈-⊥-⊥ ≈-⊤-⊤ = ≈-⊤-⊤
|
||
≈-⊔-cong ≈-⊥-⊥ ≈-⊥-⊥ = ≈-⊥-⊥
|
||
≈-⊔-cong ≈-⊥-⊥ (≈-lift x≈y) = ≈-lift x≈y
|
||
≈-⊔-cong (≈-lift x≈y) ≈-⊥-⊥ = ≈-lift x≈y
|
||
≈-⊔-cong ≈-⊤-⊤ (≈-lift x≈y) = ≈-⊤-⊤
|
||
≈-⊔-cong (≈-lift x≈y) ≈-⊤-⊤ = ≈-⊤-⊤
|
||
≈-⊔-cong (≈-lift {a₁} {a₂} a₁≈a₂) (≈-lift {a₃} {a₄} a₃≈a₄)
|
||
with ≈₁-dec a₁ a₃ | ≈₁-dec a₂ a₄
|
||
... | yes a₁≈a₃ | yes a₂≈a₄ = ≈-lift a₁≈a₂
|
||
... | yes a₁≈a₃ | no a₂̷≈a₄ = ⊥-elim (a₂̷≈a₄ (≈₁-trans (≈₁-sym a₁≈a₂) (≈₁-trans (a₁≈a₃) a₃≈a₄)))
|
||
... | no a₁̷≈a₃ | yes a₂≈a₄ = ⊥-elim (a₁̷≈a₃ (≈₁-trans a₁≈a₂ (≈₁-trans a₂≈a₄ (≈₁-sym a₃≈a₄))))
|
||
... | no _ | no _ = ≈-⊤-⊤
|
||
|
||
⊔-assoc : ∀ (ab₁ ab₂ ab₃ : AboveBelow) →
|
||
((ab₁ ⊔ ab₂) ⊔ ab₃) ≈ (ab₁ ⊔ (ab₂ ⊔ ab₃))
|
||
⊔-assoc ⊤ ab₂ ab₃ = ≈-⊤-⊤
|
||
⊔-assoc ⊥ ab₂ ab₃ = ≈-refl
|
||
⊔-assoc [ x₁ ] ⊤ ab₃ = ≈-⊤-⊤
|
||
⊔-assoc [ x₁ ] ⊥ ab₃ = ≈-refl
|
||
⊔-assoc [ x₁ ] [ x₂ ] ⊤ rewrite x⊔⊤≡⊤ ([ x₁ ] ⊔ [ x₂ ]) = ≈-⊤-⊤
|
||
⊔-assoc [ x₁ ] [ x₂ ] ⊥ rewrite x⊔⊥≡x ([ x₁ ] ⊔ [ x₂ ]) = ≈-refl
|
||
⊔-assoc [ x₁ ] [ x₂ ] [ x₃ ]
|
||
with ≈₁-dec x₂ x₃ | ≈₁-dec x₁ x₂
|
||
... | no x₂̷≈x₃ | no _ rewrite x̷≈y⇒[x]⊔[y]≡⊤ x₂̷≈x₃ = ≈-⊤-⊤
|
||
... | no x₂̷≈x₃ | yes x₁≈x₂ rewrite x̷≈y⇒[x]⊔[y]≡⊤ x₂̷≈x₃
|
||
rewrite x̷≈y⇒[x]⊔[y]≡⊤ (x₂̷≈x₃ ∘ (≈₁-trans (≈₁-sym x₁≈x₂))) = ≈-⊤-⊤
|
||
... | yes x₂≈x₃ | yes x₁≈x₂ rewrite x≈y⇒[x]⊔[y]≡[x] x₂≈x₃
|
||
rewrite x≈y⇒[x]⊔[y]≡[x] x₁≈x₂
|
||
rewrite x≈y⇒[x]⊔[y]≡[x] (≈₁-trans x₁≈x₂ x₂≈x₃) = ≈-refl
|
||
... | yes x₂≈x₃ | no x₁̷≈x₂ rewrite x̷≈y⇒[x]⊔[y]≡⊤ x₁̷≈x₂ = ≈-⊤-⊤
|
||
|
||
⊔-comm : ∀ (ab₁ ab₂ : AboveBelow) → (ab₁ ⊔ ab₂) ≈ (ab₂ ⊔ ab₁)
|
||
⊔-comm ⊤ x rewrite x⊔⊤≡⊤ x = ≈-refl
|
||
⊔-comm ⊥ x rewrite x⊔⊥≡x x = ≈-refl
|
||
⊔-comm x ⊤ rewrite x⊔⊤≡⊤ x = ≈-refl
|
||
⊔-comm x ⊥ rewrite x⊔⊥≡x x = ≈-refl
|
||
⊔-comm [ x₁ ] [ x₂ ] with ≈₁-dec x₁ x₂
|
||
... | yes x₁≈x₂ rewrite x≈y⇒[x]⊔[y]≡[x] (≈₁-sym x₁≈x₂) = ≈-lift x₁≈x₂
|
||
... | no x₁̷≈x₂ rewrite x̷≈y⇒[x]⊔[y]≡⊤ (x₁̷≈x₂ ∘ ≈₁-sym) = ≈-⊤-⊤
|
||
|
||
⊔-idemp : ∀ ab → (ab ⊔ ab) ≈ ab
|
||
⊔-idemp ⊤ = ≈-⊤-⊤
|
||
⊔-idemp ⊥ = ≈-⊥-⊥
|
||
⊔-idemp [ x ] rewrite x≈y⇒[x]⊔[y]≡[x] (≈₁-refl {x}) = ≈-refl
|
||
|
||
isJoinSemilattice : IsSemilattice AboveBelow _≈_ _⊔_
|
||
isJoinSemilattice = record
|
||
{ ≈-equiv = ≈-equiv
|
||
; ≈-⊔-cong = ≈-⊔-cong
|
||
; ⊔-assoc = ⊔-assoc
|
||
; ⊔-comm = ⊔-comm
|
||
; ⊔-idemp = ⊔-idemp
|
||
}
|
||
|
||
_⊓_ : AboveBelow → AboveBelow → AboveBelow
|
||
⊥ ⊓ x = ⊥
|
||
⊤ ⊓ x = x
|
||
[ x ] ⊓ [ y ] with ≈₁-dec x y
|
||
... | yes _ = [ x ]
|
||
... | no _ = ⊥
|
||
x ⊓ ⊥ = ⊥
|
||
x ⊓ ⊤ = x
|
||
|
||
⊥⊓x≡⊥ : ∀ (x : AboveBelow) → ⊥ ⊓ x ≡ ⊥
|
||
⊥⊓x≡⊥ _ = refl
|
||
|
||
x⊓⊥≡⊥ : ∀ (x : AboveBelow) → x ⊓ ⊥ ≡ ⊥
|
||
x⊓⊥≡⊥ ⊤ = refl
|
||
x⊓⊥≡⊥ ⊥ = refl
|
||
x⊓⊥≡⊥ [ x ] = refl
|
||
|
||
⊤⊓x≡x : ∀ (x : AboveBelow) → ⊤ ⊓ x ≡ x
|
||
⊤⊓x≡x _ = refl
|
||
|
||
x⊓⊤≡x : ∀ (x : AboveBelow) → x ⊓ ⊤ ≡ x
|
||
x⊓⊤≡x ⊤ = refl
|
||
x⊓⊤≡x ⊥ = refl
|
||
x⊓⊤≡x [ x ] = refl
|
||
|
||
x≈y⇒[x]⊓[y]≡[x] : ∀ {x y : A} → x ≈₁ y → [ x ] ⊓ [ y ] ≡ [ x ]
|
||
x≈y⇒[x]⊓[y]≡[x] {x} {y} x≈₁y
|
||
with ≈₁-dec x y
|
||
... | yes _ = refl
|
||
... | no x̷≈₁y = ⊥-elim (x̷≈₁y x≈₁y)
|
||
|
||
x̷≈y⇒[x]⊓[y]≡⊥ : ∀ {x y : A} → ¬ x ≈₁ y → [ x ] ⊓ [ y ] ≡ ⊥
|
||
x̷≈y⇒[x]⊓[y]≡⊥ {x} {y} x̷≈₁y
|
||
with ≈₁-dec x y
|
||
... | yes x≈₁y = ⊥-elim (x̷≈₁y x≈₁y)
|
||
... | no x̷≈₁y = refl
|
||
|
||
≈-⊓-cong : ∀ {ab₁ ab₂ ab₃ ab₄} → ab₁ ≈ ab₂ → ab₃ ≈ ab₄ → (ab₁ ⊓ ab₃) ≈ (ab₂ ⊓ ab₄)
|
||
≈-⊓-cong ≈-⊤-⊤ ≈-⊤-⊤ = ≈-⊤-⊤
|
||
≈-⊓-cong ≈-⊤-⊤ ≈-⊥-⊥ = ≈-⊥-⊥
|
||
≈-⊓-cong ≈-⊥-⊥ ≈-⊤-⊤ = ≈-⊥-⊥
|
||
≈-⊓-cong ≈-⊥-⊥ ≈-⊥-⊥ = ≈-⊥-⊥
|
||
≈-⊓-cong ≈-⊤-⊤ (≈-lift x≈y) = ≈-lift x≈y
|
||
≈-⊓-cong (≈-lift x≈y) ≈-⊤-⊤ = ≈-lift x≈y
|
||
≈-⊓-cong ≈-⊥-⊥ (≈-lift x≈y) = ≈-⊥-⊥
|
||
≈-⊓-cong (≈-lift x≈y) ≈-⊥-⊥ = ≈-⊥-⊥
|
||
≈-⊓-cong (≈-lift {a₁} {a₂} a₁≈a₂) (≈-lift {a₃} {a₄} a₃≈a₄)
|
||
with ≈₁-dec a₁ a₃ | ≈₁-dec a₂ a₄
|
||
... | yes a₁≈a₃ | yes a₂≈a₄ = ≈-lift a₁≈a₂
|
||
... | yes a₁≈a₃ | no a₂̷≈a₄ = ⊥-elim (a₂̷≈a₄ (≈₁-trans (≈₁-sym a₁≈a₂) (≈₁-trans (a₁≈a₃) a₃≈a₄)))
|
||
... | no a₁̷≈a₃ | yes a₂≈a₄ = ⊥-elim (a₁̷≈a₃ (≈₁-trans a₁≈a₂ (≈₁-trans a₂≈a₄ (≈₁-sym a₃≈a₄))))
|
||
... | no _ | no _ = ≈-⊥-⊥
|
||
|
||
⊓-assoc : ∀ (ab₁ ab₂ ab₃ : AboveBelow) → ((ab₁ ⊓ ab₂) ⊓ ab₃) ≈ (ab₁ ⊓ (ab₂ ⊓ ab₃))
|
||
⊓-assoc ⊥ ab₂ ab₃ = ≈-⊥-⊥
|
||
⊓-assoc ⊤ ab₂ ab₃ = ≈-refl
|
||
⊓-assoc [ x₁ ] ⊥ ab₃ = ≈-⊥-⊥
|
||
⊓-assoc [ x₁ ] ⊤ ab₃ = ≈-refl
|
||
⊓-assoc [ x₁ ] [ x₂ ] ⊥ rewrite x⊓⊥≡⊥ ([ x₁ ] ⊓ [ x₂ ]) = ≈-⊥-⊥
|
||
⊓-assoc [ x₁ ] [ x₂ ] ⊤ rewrite x⊓⊤≡x ([ x₁ ] ⊓ [ x₂ ]) = ≈-refl
|
||
⊓-assoc [ x₁ ] [ x₂ ] [ x₃ ]
|
||
with ≈₁-dec x₂ x₃ | ≈₁-dec x₁ x₂
|
||
... | no x₂̷≈x₃ | no _ rewrite x̷≈y⇒[x]⊓[y]≡⊥ x₂̷≈x₃ = ≈-⊥-⊥
|
||
... | no x₂̷≈x₃ | yes x₁≈x₂ rewrite x̷≈y⇒[x]⊓[y]≡⊥ x₂̷≈x₃
|
||
rewrite x̷≈y⇒[x]⊓[y]≡⊥ λ x₁≈x₃ → x₂̷≈x₃ (≈₁-trans (≈₁-sym x₁≈x₂) x₁≈x₃) = ≈-⊥-⊥
|
||
... | yes x₂≈x₃ | yes x₁≈x₂ rewrite x≈y⇒[x]⊓[y]≡[x] x₂≈x₃
|
||
rewrite x≈y⇒[x]⊓[y]≡[x] x₁≈x₂
|
||
rewrite x≈y⇒[x]⊓[y]≡[x] (≈₁-trans x₁≈x₂ x₂≈x₃) = ≈-refl
|
||
... | yes x₂≈x₃ | no x₁̷≈x₂ rewrite x̷≈y⇒[x]⊓[y]≡⊥ x₁̷≈x₂ = ≈-⊥-⊥
|
||
|
||
⊓-comm : ∀ (ab₁ ab₂ : AboveBelow) → (ab₁ ⊓ ab₂) ≈ (ab₂ ⊓ ab₁)
|
||
⊓-comm ⊥ x rewrite x⊓⊥≡⊥ x = ≈-refl
|
||
⊓-comm ⊤ x rewrite x⊓⊤≡x x = ≈-refl
|
||
⊓-comm x ⊥ rewrite x⊓⊥≡⊥ x = ≈-refl
|
||
⊓-comm x ⊤ rewrite x⊓⊤≡x x = ≈-refl
|
||
⊓-comm [ x₁ ] [ x₂ ] with ≈₁-dec x₁ x₂
|
||
... | yes x₁≈x₂ rewrite x≈y⇒[x]⊓[y]≡[x] (≈₁-sym x₁≈x₂) = ≈-lift x₁≈x₂
|
||
... | no x₁̷≈x₂ rewrite x̷≈y⇒[x]⊓[y]≡⊥ λ x₂≈x₁ → (x₁̷≈x₂ (≈₁-sym x₂≈x₁)) = ≈-⊥-⊥
|
||
|
||
⊓-idemp : ∀ ab → (ab ⊓ ab) ≈ ab
|
||
⊓-idemp ⊥ = ≈-⊥-⊥
|
||
⊓-idemp ⊤ = ≈-⊤-⊤
|
||
⊓-idemp [ x ] rewrite x≈y⇒[x]⊓[y]≡[x] (≈₁-refl {x}) = ≈-refl
|
||
|
||
isMeetSemilattice : IsSemilattice AboveBelow _≈_ _⊓_
|
||
isMeetSemilattice = record
|
||
{ ≈-equiv = ≈-equiv
|
||
; ≈-⊔-cong = ≈-⊓-cong
|
||
; ⊔-assoc = ⊓-assoc
|
||
; ⊔-comm = ⊓-comm
|
||
; ⊔-idemp = ⊓-idemp
|
||
}
|
||
|
||
absorb-⊔-⊓ : ∀ (ab₁ ab₂ : AboveBelow) → (ab₁ ⊔ (ab₁ ⊓ ab₂)) ≈ ab₁
|
||
absorb-⊔-⊓ ⊥ ab₂ rewrite ⊥⊓x≡⊥ ab₂ = ≈-⊥-⊥
|
||
absorb-⊔-⊓ ⊤ _ = ≈-⊤-⊤
|
||
absorb-⊔-⊓ [ x ] ⊥ rewrite x⊓⊥≡⊥ [ x ]
|
||
rewrite x⊔⊥≡x [ x ] = ≈-refl
|
||
absorb-⊔-⊓ [ x ] ⊤ rewrite x⊓⊤≡x [ x ] = ⊔-idemp _
|
||
absorb-⊔-⊓ [ x ] [ y ]
|
||
with ≈₁-dec x y
|
||
... | yes x≈y rewrite x≈y⇒[x]⊓[y]≡[x] x≈y = ⊔-idemp _
|
||
... | no x̷≈y rewrite x̷≈y⇒[x]⊓[y]≡⊥ x̷≈y rewrite x⊔⊥≡x [ x ] = ≈-refl
|
||
|
||
absorb-⊓-⊔ : ∀ (ab₁ ab₂ : AboveBelow) → (ab₁ ⊓ (ab₁ ⊔ ab₂)) ≈ ab₁
|
||
absorb-⊓-⊔ ⊤ ab₂ rewrite ⊤⊔x≡⊤ ab₂ = ≈-⊤-⊤
|
||
absorb-⊓-⊔ ⊥ _ = ≈-⊥-⊥
|
||
absorb-⊓-⊔ [ x ] ⊤ rewrite x⊔⊤≡⊤ [ x ]
|
||
rewrite x⊓⊤≡x [ x ] = ≈-refl
|
||
absorb-⊓-⊔ [ x ] ⊥ rewrite x⊔⊥≡x [ x ] = ⊓-idemp _
|
||
absorb-⊓-⊔ [ x ] [ y ]
|
||
with ≈₁-dec x y
|
||
... | yes x≈y rewrite x≈y⇒[x]⊔[y]≡[x] x≈y = ⊓-idemp _
|
||
... | no x̷≈y rewrite x̷≈y⇒[x]⊔[y]≡⊤ x̷≈y rewrite x⊓⊤≡x [ x ] = ≈-refl
|
||
|
||
|
||
isLattice : IsLattice AboveBelow _≈_ _⊔_ _⊓_
|
||
isLattice = record
|
||
{ joinSemilattice = isJoinSemilattice
|
||
; meetSemilattice = isMeetSemilattice
|
||
; absorb-⊔-⊓ = absorb-⊔-⊓
|
||
; absorb-⊓-⊔ = absorb-⊓-⊔
|
||
}
|
||
|
||
lattice : Lattice AboveBelow
|
||
lattice = record
|
||
{ _≈_ = _≈_
|
||
; _⊔_ = _⊔_
|
||
; _⊓_ = _⊓_
|
||
; isLattice = isLattice
|
||
}
|
||
|
||
open IsLattice isLattice using (_≼_; _≺_; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
|
||
|
||
⊥≺[x] : ∀ (x : A) → ⊥ ≺ [ x ]
|
||
⊥≺[x] x = (≈-refl , λ ())
|
||
|
||
x≺[y]⇒x≡⊥ : ∀ (x : AboveBelow) (y : A) → x ≺ [ y ] → x ≡ ⊥
|
||
x≺[y]⇒x≡⊥ x y ((x⊔[y]≈[y]) , x̷≈[y]) with x
|
||
... | ⊥ = refl
|
||
... | ⊤ with () ← x⊔[y]≈[y]
|
||
... | [ b ] with ≈₁-dec b y
|
||
... | yes b≈y = ⊥-elim (x̷≈[y] (≈-lift b≈y))
|
||
... | no _ with () ← x⊔[y]≈[y]
|
||
|
||
[x]≺⊤ : ∀ (x : A) → [ x ] ≺ ⊤
|
||
[x]≺⊤ x rewrite x⊔⊤≡⊤ [ x ] = (≈-⊤-⊤ , λ ())
|
||
|
||
[x]≺y⇒y≡⊤ : ∀ (x : A) (y : AboveBelow) → [ x ] ≺ y → y ≡ ⊤
|
||
[x]≺y⇒y≡⊤ x y ([x]⊔y≈y , [x]̷≈y) with y
|
||
... | ⊥ with () ← [x]⊔y≈y
|
||
... | ⊤ = refl
|
||
... | [ a ] with ≈₁-dec x a
|
||
... | yes x≈a = ⊥-elim ([x]̷≈y (≈-lift x≈a))
|
||
... | no _ with () ← [x]⊔y≈y
|
||
|
||
open Chain _≈_ ≈-equiv (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice)
|
||
|
||
longestChain : Chain ⊥ ⊤ 2
|
||
longestChain = step (⊥≺[x] x) ≈-refl (step ([x]≺⊤ x) ≈-⊤-⊤ (done ≈-⊤-⊤))
|
||
|
||
¬-Chain-⊤ : ∀ {ab : AboveBelow} {n : ℕ} → ¬ Chain ⊤ ab (suc n)
|
||
¬-Chain-⊤ {x} (step (⊤⊔x≈x , ⊤̷≈x) _ _) rewrite ⊤⊔x≡⊤ x = ⊥-elim (⊤̷≈x ⊤⊔x≈x)
|
||
|
||
isLongest : ∀ {ab₁ ab₂ : AboveBelow} {n : ℕ} → Chain ab₁ ab₂ n → n ≤ 2
|
||
isLongest (done _) = z≤n
|
||
isLongest (step _ _ (done _)) = s≤s z≤n
|
||
isLongest (step _ _ (step _ _ (done _))) = s≤s (s≤s z≤n)
|
||
isLongest {⊤} c@(step _ _ _) = ⊥-elim (¬-Chain-⊤ c)
|
||
isLongest {[ x ]} (step {_} {y} [x]≺y y≈y' c@(step _ _ _))
|
||
rewrite [x]≺y⇒y≡⊤ x y [x]≺y with ≈-⊤-⊤ ← y≈y' = ⊥-elim (¬-Chain-⊤ c)
|
||
isLongest {⊥} (step {_} {⊥} (_ , ⊥̷≈⊥) _ _) = ⊥-elim (⊥̷≈⊥ ≈-⊥-⊥)
|
||
isLongest {⊥} (step {_} {⊤} _ ≈-⊤-⊤ c@(step _ _ _)) = ⊥-elim (¬-Chain-⊤ c)
|
||
isLongest {⊥} (step {_} {[ x ]} _ (≈-lift _) (step [x]≺y y≈z c@(step _ _ _)))
|
||
rewrite [x]≺y⇒y≡⊤ _ _ [x]≺y with ≈-⊤-⊤ ← y≈z = ⊥-elim (¬-Chain-⊤ c)
|
||
|
||
fixedHeight : IsLattice.FixedHeight isLattice 2
|
||
fixedHeight = (((⊥ , ⊤) , longestChain) , isLongest)
|
||
|
||
isFiniteHeightLattice : IsFiniteHeightLattice AboveBelow 2 _≈_ _⊔_ _⊓_
|
||
isFiniteHeightLattice = record
|
||
{ isLattice = isLattice
|
||
; fixedHeight = fixedHeight
|
||
}
|
||
|
||
finiteHeightLattice : FiniteHeightLattice AboveBelow
|
||
finiteHeightLattice = record
|
||
{ height = 2
|
||
; _≈_ = _≈_
|
||
; _⊔_ = _⊔_
|
||
; _⊓_ = _⊓_
|
||
; isFiniteHeightLattice = isFiniteHeightLattice
|
||
}
|