Start formalizing the bottom/top lattice

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Lattice/AboveBelow.agda

@@ -0,0 +1,153 @@
+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
+        }