From f27dec890422f12edfe0cf5697cdf5e5732f5347 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 23 Sep 2023 12:33:48 -0700
Subject: [PATCH] Add proof of fixed-height chain

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice/Unit.agda | 106 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 106 insertions(+)
 create mode 100644 Lattice/Unit.agda

diff --git a/Lattice/Unit.agda b/Lattice/Unit.agda
new file mode 100644
index 0000000..4c58592
--- /dev/null
+++ b/Lattice/Unit.agda
@@ -0,0 +1,106 @@
+module Lattice.Unit where
+
+open import Data.Empty using (⊥-elim)
+open import Data.Product using (_,_)
+open import Data.Nat using (ℕ; _≤_; z≤n)
+open import Data.Unit using (⊤; tt)
+open import Data.Unit.Properties using (_≟_; ≡-setoid)
+open import Relation.Binary using (Setoid)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
+open import Relation.Nullary using (Dec; ¬_; yes; no)
+open import Equivalence
+open import Lattice
+import Chain
+
+open Setoid ≡-setoid using (refl; sym; trans)
+
+_≈_ : ⊤ → ⊤ → Set
+_≈_ = _≡_
+
+≈-equiv : IsEquivalence ⊤ _≈_
+≈-equiv = record
+    { ≈-refl = refl
+    ; ≈-sym = sym
+    ; ≈-trans = trans
+    }
+
+≈-dec : IsDecidable _≈_
+≈-dec = _≟_
+
+_⊔_ : ⊤ → ⊤ → ⊤
+tt ⊔ tt = tt
+
+_⊓_ : ⊤ → ⊤ → ⊤
+tt ⊓ tt = tt
+
+≈-⊔-cong : ∀ {ab₁ ab₂ ab₃ ab₄} → ab₁ ≈ ab₂ → ab₃ ≈ ab₄ → (ab₁ ⊔ ab₃) ≈ (ab₂ ⊔ ab₄)
+≈-⊔-cong {tt} {tt} {tt} {tt} _ _ = Eq.refl
+
+⊔-assoc : (x y z : ⊤) → ((x ⊔ y) ⊔ z) ≈ (x ⊔ (y ⊔ z))
+⊔-assoc tt tt tt = Eq.refl
+
+⊔-comm : (x y : ⊤) → (x ⊔ y) ≈ (y ⊔ x)
+⊔-comm tt tt = Eq.refl
+
+⊔-idemp : (x : ⊤) → (x ⊔ x) ≈ x
+⊔-idemp tt = Eq.refl
+
+isJoinSemilattice : IsSemilattice ⊤ _≈_ _⊔_
+isJoinSemilattice = record
+    { ≈-equiv = ≈-equiv
+    ; ≈-⊔-cong = ≈-⊔-cong
+    ; ⊔-assoc = ⊔-assoc
+    ; ⊔-comm  = ⊔-comm
+    ; ⊔-idemp = ⊔-idemp
+    }
+
+≈-⊓-cong : ∀ {ab₁ ab₂ ab₃ ab₄} → ab₁ ≈ ab₂ → ab₃ ≈ ab₄ → (ab₁ ⊓ ab₃) ≈ (ab₂ ⊓ ab₄)
+≈-⊓-cong {tt} {tt} {tt} {tt} _ _ = Eq.refl
+
+⊓-assoc : (x y z : ⊤) → ((x ⊓ y) ⊓ z) ≈ (x ⊓ (y ⊓ z))
+⊓-assoc tt tt tt = Eq.refl
+
+⊓-comm : (x y : ⊤) → (x ⊓ y) ≈ (y ⊓ x)
+⊓-comm tt tt = Eq.refl
+
+⊓-idemp : (x : ⊤) → (x ⊓ x) ≈ x
+⊓-idemp tt = Eq.refl
+
+isMeetSemilattice : IsSemilattice ⊤ _≈_ _⊓_
+isMeetSemilattice = record
+    { ≈-equiv = ≈-equiv
+    ; ≈-⊔-cong = ≈-⊓-cong
+    ; ⊔-assoc = ⊓-assoc
+    ; ⊔-comm  = ⊓-comm
+    ; ⊔-idemp = ⊓-idemp
+    }
+
+absorb-⊔-⊓ : (x y : ⊤) → (x ⊔ (x ⊓ y)) ≈ x
+absorb-⊔-⊓ tt tt = Eq.refl
+
+absorb-⊓-⊔ : (x y : ⊤) → (x ⊓ (x ⊔ y)) ≈ x
+absorb-⊓-⊔ tt tt = Eq.refl
+
+isLattice : IsLattice ⊤ _≈_ _⊔_ _⊓_
+isLattice = record
+    { joinSemilattice = isJoinSemilattice
+    ; meetSemilattice = isMeetSemilattice
+    ; absorb-⊔-⊓ = absorb-⊔-⊓
+    ; absorb-⊓-⊔ = absorb-⊓-⊔
+    }
+
+open Chain _≈_ ≈-equiv (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice)
+
+private
+    longestChain : Chain tt tt 0
+    longestChain = done refl
+
+    isLongest : ∀ {t₁ t₂ : ⊤} {n : ℕ} → Chain t₁ t₂ n → n ≤ 0
+    isLongest {tt} {tt} (step ((tt , tt⊔tt≈tt) , tt≈tt) _ _) = ⊥-elim (tt≈tt refl)
+    isLongest (done _) = z≤n
+
+isFiniteHeightLattice : IsFiniteHeightLattice ⊤ 0 _≈_ _⊔_ _⊓_
+isFiniteHeightLattice = record
+    { isLattice = isLattice
+    ; fixedHeight = (((tt , tt) , longestChain) , isLongest)
+    }