DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Clean up AboveBelow slightly

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-03-02 14:34:15 -08:00
parent 8516f58b1d
commit 112dcb2208
1 changed files with 7 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
Lattice/AboveBelow.agda
View File

@ -10,7 +10,9 @@ module Lattice.AboveBelow {a} (A : Set a)
open import Data.Empty using (⊥-elim) open import Data.Empty using (⊥-elim)
open import Data.Product using (_,_) open import Data.Product using (_,_)
open import Data.Nat using (_≤_; ℕ; z≤n; s≤s; suc) 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) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; subst; refl)
import Chain import Chain
open IsEquivalence ≈₁-equiv using () renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans) open IsEquivalence ≈₁-equiv using () renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
@ -61,6 +63,9 @@ data _≈_ : AboveBelow → AboveBelow → Set a where
≈-dec [ x ] ⊥ = 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.
module Plain where module Plain where
_⊔_ : AboveBelow → AboveBelow → AboveBelow _⊔_ : AboveBelow → AboveBelow → AboveBelow
⊥ ⊔ x = x ⊥ ⊔ x = x
@ -126,7 +131,7 @@ module Plain where
with ≈₁-dec x₂ x₃ | ≈₁-dec x₁ x₂ with ≈₁-dec x₂ x₃ | ≈₁-dec x₁ x₂
... | no x₂̷≈x₃ | no _ rewrite x̷≈y⇒[x]⊔[y]≡⊤ 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₃ ... | 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₃) = ≈-⊤-⊤ 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₃ ... | 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] x₁≈x₂
rewrite x≈y⇒[x]⊔[y]≡[x] (≈₁-trans x₁≈x₂ x₂≈x₃) = ≈-refl rewrite x≈y⇒[x]⊔[y]≡[x] (≈₁-trans x₁≈x₂ x₂≈x₃) = ≈-refl
@ -139,7 +144,7 @@ module Plain where
⊔-comm x ⊥ rewrite x⊔⊥≡x x = ≈-refl ⊔-comm x ⊥ rewrite x⊔⊥≡x x = ≈-refl
⊔-comm [ x₁ ] [ x₂ ] with ≈₁-dec x₁ x₂ ⊔-comm [ x₁ ] [ x₂ ] with ≈₁-dec x₁ x₂
... | yes x₁≈x₂ rewrite x≈y⇒[x]⊔[y]≡[x] (≈₁-sym x₁≈x₂) = ≈-lift 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₁)) = ≈-⊤-⊤ ... | no x₁̷≈x₂ rewrite x̷≈y⇒[x]⊔[y]≡⊤ (x₁̷≈x₂ ∘ ≈₁-sym) = ≈-⊤-⊤
⊔-idemp : ∀ ab → (ab ⊔ ab) ≈ ab ⊔-idemp : ∀ ab → (ab ⊔ ab) ≈ ab
⊔-idemp ⊤ = ≈-⊤-⊤ ⊔-idemp ⊤ = ≈-⊤-⊤