agda-spa/Lattice/AboveBelow.agda
Danila Fedorin 8515491327 Simplify AboveBelow a bit to avoid nested modules
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-10 18:43:10 -07:00

360 lines
16 KiB
Agda
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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 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
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 (_≼_; _≺_) 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)
isFiniteHeightLattice : IsFiniteHeightLattice AboveBelow 2 _≈_ _⊔_ _⊓_
isFiniteHeightLattice = record
{ isLattice = isLattice
; fixedHeight = ((( , ) , longestChain) , isLongest)
}
finiteHeightLattice : FiniteHeightLattice AboveBelow
finiteHeightLattice = record
{ height = 2
; _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isFiniteHeightLattice = isFiniteHeightLattice
}