agda-spa/Lattice/AboveBelow.agda
Danila Fedorin d338241319 Add a meet operation, too
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-09-17 20:01:32 -07:00

247 lines
11 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 Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; subst; refl)
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
}