agda-spa/Lattice/AboveBelow.agda
Danila Fedorin 512cd22be5 Fix definition of 'less than' to not involve a third variable.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-07 21:04:13 -08:00

332 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 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 λ ()
module Plain 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₃ 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
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-⊓-⊔
}
open IsLattice isLattice using (_≼_; _≺_)
⊥≺[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)
module _ (x : A) where
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)
}