From fa7e2b5bb6bbc49e3e93400615e25f43bb6d7d7e Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Mon, 18 Sep 2023 22:34:58 -0700
Subject: [PATCH] Add a proof that AboveBelow is a fixed-height lattice (phew!)

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice/AboveBelow.agda | 57 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 57 insertions(+)

diff --git a/Lattice/AboveBelow.agda b/Lattice/AboveBelow.agda
index f410cd5..3abef25 100644
--- a/Lattice/AboveBelow.agda
+++ b/Lattice/AboveBelow.agda
@@ -8,7 +8,10 @@ module Lattice.AboveBelow {a} (A : Set 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)
 
@@ -275,3 +278,57 @@ module Plain where
         ; absorb-⊔-⊓ = absorb-⊔-⊓
         ; absorb-⊓-⊔ = absorb-⊓-⊔
         }
+
+    open IsLattice isLattice using (_≼_; _≺_)
+
+    ⊥≺[x] : ∀ (x : A) → ⊥ ≺ [ x ]
+    ⊥≺[x] x = (([ x ] , ≈-refl) , λ ())
+
+    x≺[y]⇒y≡⊥ : ∀ (x : AboveBelow) (y : A) → x ≺ [ y ] → x ≡ ⊥
+    x≺[y]⇒y≡⊥  x y ((d , x⊔d≈[y]) , x̷≈[y]) with d
+    ... | ⊥ rewrite x⊔⊥≡x x with ≈-lift a≈y ← x⊔d≈[y] = ⊥-elim (x̷≈[y] (≈-lift a≈y))
+    ... | ⊤ rewrite x⊔⊤≡⊤ x with () <- x⊔d≈[y]
+    ... | [ a ] with x
+    ...     | ⊥ = refl
+    ...     | ⊤ with () <- x⊔d≈[y]
+    ...     | [ b ] with ≈₁-dec b a
+    ...         | yes _ with ≈-lift b≈y ← x⊔d≈[y] = ⊥-elim (x̷≈[y] (≈-lift b≈y))
+    ...         | no _ with () <- x⊔d≈[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 ((d , [x]⊔d≈y) , [x]̷≈y) with d
+    ... | ⊥ rewrite x⊔⊥≡x [ x ] with ≈-lift x≈a ← [x]⊔d≈y = ⊥-elim ([x]̷≈y (≈-lift x≈a))
+    ... | ⊤ rewrite x⊔⊤≡⊤ [ x ] with ≈-⊤-⊤ ← [x]⊔d≈y = refl
+    ... | [ a ] with ≈₁-dec x a
+    ...     | yes _   with ≈-lift x≈a ← [x]⊔d≈y = ⊥-elim ([x]̷≈y (≈-lift x≈a))
+    ...     | no _    with ≈-⊤-⊤ ← [x]⊔d≈y = refl
+
+    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-⊤ (step ((d , ⊤⊔d≈x) , ⊤̷≈x) _ _) rewrite ⊤⊔x≡⊤ d = ⊥-elim (⊤̷≈x ⊤⊔d≈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)
+            }