From 422ea93edb22caae84e36430ed35d34ea5e99109 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Thu, 13 Jul 2023 21:50:27 -0700
Subject: [PATCH] Finish up the Nat semilattices

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice.agda | 71 +++++++++++++++++++++++++++++++++++++++++-----------
 1 file changed, 56 insertions(+), 15 deletions(-)

diff --git a/Lattice.agda b/Lattice.agda
index bf35b3d..6b3ef05 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -5,7 +5,8 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
 open import Relation.Binary.Definitions
 open import Data.Nat as Nat using (ℕ; _≤_)
 open import Data.Product using (_×_; _,_)
-open import Agda.Primitive using (lsuc)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Agda.Primitive using (lsuc; Level)
 
 open import NatMap using (NatMap)
 
@@ -15,6 +16,13 @@ record IsPreorder {a} (A : Set a) (_≼_ : A → A → Set a) : Set a where
         ≼-trans : Transitive (_≼_)
         ≼-antisym : Antisymmetric (_≡_) (_≼_)
 
+isPreorderFlip : {a : Level} → {A : Set a} → {_≼_ : A → A → Set a} → IsPreorder A _≼_ → IsPreorder A (λ x y → y ≼ x)
+isPreorderFlip isPreorder = record
+    { ≼-refl = IsPreorder.≼-refl isPreorder
+    ; ≼-trans = λ {x} {y} {z} x≽y y≽z → IsPreorder.≼-trans isPreorder y≽z x≽y
+    ; ≼-antisym = λ {x} {y} x≽y y≽x → IsPreorder.≼-antisym isPreorder y≽x x≽y
+    }
+
 record Preorder {a} (A : Set a) : Set (lsuc a) where
     field
         _≼_ : A → A → Set a
@@ -27,13 +35,12 @@ record IsSemilattice {a} (A : Set a) (_≼_ : A → A → Set a) (_⊔_ : A →
     field
         isPreorder : IsPreorder A _≼_
 
-        ⊔-assoc : (x : A) → (y : A) → (z : A) → (x ⊔ y) ⊔ z ≡ x ⊔ (y ⊔ z)
-        ⊔-comm : (x : A) → (y : A) → x ⊔ y ≡ y ⊔ x
+        ⊔-assoc : (x y z : A) → (x ⊔ y) ⊔ z ≡ x ⊔ (y ⊔ z)
+        ⊔-comm : (x y : A) → x ⊔ y ≡ y ⊔ x
         ⊔-idemp : (x : A) → x ⊔ x ≡ x
 
-        ⊔-bound : (x : A) → (y : A) → (z : A) → x ⊔ y ≡ z → (x ≼ z × y ≼ z)
-        ⊔-least : (x : A) → (y : A) → (z : A) → x ⊔ y ≡ z →
-                  ∀ (z' : A) → (x ≼ z' × y ≼ z') → z ≼ z'
+        ⊔-bound : (x y z : A) → x ⊔ y ≡ z → (x ≼ z × y ≼ z)
+        ⊔-least : (x y z : A) → x ⊔ y ≡ z → ∀ (z' : A) → (x ≼ z' × y ≼ z') → z ≼ z'
 
     open IsPreorder isPreorder public
 
@@ -55,8 +62,8 @@ record IsLattice {a} (A : Set a) (_≼_ : A → A → Set a) (_⊔_ : A → A 
         joinSemilattice : IsSemilattice A _≼_ _⊔_
         meetSemilattice : IsSemilattice A _≽_ _⊓_
 
-        absorb-⊔-⊓ : (x : A) → (y : A) → x ⊔ (x ⊓ y) ≡ x
-        absorb-⊓-⊔ : (x : A) → (y : A) → x ⊓ (x ⊔ y) ≡ x
+        absorb-⊔-⊓ : (x y : A) → x ⊔ (x ⊓ y) ≡ x
+        absorb-⊓-⊔ : (x y : A) → x ⊓ (x ⊔ y) ≡ x
 
     open IsSemilattice joinSemilattice public
     open IsSemilattice meetSemilattice public renaming
@@ -82,6 +89,7 @@ private module NatInstances where
     open Nat
     open NatProps
     open Eq
+    open Data.Sum
 
     NatPreorder : Preorder ℕ
     NatPreorder = record
@@ -94,14 +102,19 @@ private module NatInstances where
         }
 
     private
-        max-bound₁ : (x : ℕ) → (y : ℕ) → (z : ℕ) → x ⊔ y ≡ z → x ≤ z
-        max-bound₁ x y z x⊔y≡z rewrite sym x⊔y≡z rewrite ⊔-comm x y = m≤n⇒m≤o⊔n y (≤-refl)
+        max-bound₁ : {x y z : ℕ} → x ⊔ y ≡ z → x ≤ z
+        max-bound₁ {x} {y} {z} x⊔y≡z rewrite sym x⊔y≡z rewrite ⊔-comm x y = m≤n⇒m≤o⊔n y (≤-refl)
 
-        max-bound₂ : (x : ℕ) → (y : ℕ) → (z : ℕ) → x ⊔ y ≡ z → y ≤ z
-        max-bound₂ x y z x⊔y≡z rewrite sym x⊔y≡z = m≤n⇒m≤o⊔n x (≤-refl)
+        max-bound₂ : {x y z : ℕ} → x ⊔ y ≡ z → y ≤ z
+        max-bound₂ {x} {y} {z} x⊔y≡z rewrite sym x⊔y≡z = m≤n⇒m≤o⊔n x (≤-refl)
 
-    NatMinSemilattice : Semilattice ℕ
-    NatMinSemilattice = record
+        max-least : (x y z : ℕ) → x ⊔ y ≡ z → ∀ (z' : ℕ) → (x ≤ z' × y ≤ z') → z ≤ z'
+        max-least x y z x⊔y≡z z' (x≤z' , y≤z') with (⊔-sel x y)
+        ...                                    | inj₁ x⊔y≡x rewrite trans (sym x⊔y≡z) (x⊔y≡x) = x≤z'
+        ...                                    | inj₂ x⊔y≡y rewrite trans (sym x⊔y≡z) (x⊔y≡y) = y≤z'
+
+    NatMaxSemilattice : Semilattice ℕ
+    NatMaxSemilattice = record
         { _≼_ = _≤_
         ; _⊔_ = _⊔_
         ; isSemilattice = record
@@ -109,6 +122,34 @@ private module NatInstances where
             ; ⊔-assoc = ⊔-assoc
             ; ⊔-comm = ⊔-comm
             ; ⊔-idemp = ⊔-idem
-            ; ⊔-bound = λ x y z x⊔y≡z → (max-bound₁ x y z x⊔y≡z , max-bound₂ x y z x⊔y≡z)
+            ; ⊔-bound = λ x y z x⊔y≡z → (max-bound₁ x⊔y≡z , max-bound₂ x⊔y≡z)
+            ; ⊔-least = max-least
+            }
+        }
+
+    private
+        min-bound₁ : {x y z : ℕ} → x ⊓ y ≡ z → z ≤ x
+        min-bound₁ {x} {y} {z} x⊓y≡z rewrite sym x⊓y≡z = m≤n⇒m⊓o≤n y (≤-refl)
+
+        min-bound₂ : {x y z : ℕ} → x ⊓ y ≡ z → z ≤ y
+        min-bound₂ {x} {y} {z} x⊓y≡z rewrite sym x⊓y≡z rewrite ⊓-comm x y = m≤n⇒m⊓o≤n x (≤-refl)
+
+        min-greatest : (x y z : ℕ) → x ⊓ y ≡ z → ∀ (z' : ℕ) → (z' ≤ x × z' ≤ y) → z' ≤ z
+        min-greatest x y z x⊓y≡z z' (z'≤x , z'≤y) with (⊓-sel x y)
+        ...                                    | inj₁ x⊓y≡x rewrite trans (sym x⊓y≡z) (x⊓y≡x) = z'≤x
+        ...                                    | inj₂ x⊓y≡y rewrite trans (sym x⊓y≡z) (x⊓y≡y) = z'≤y
+
+
+    NatMinSemilattice : Semilattice ℕ
+    NatMinSemilattice = record
+        { _≼_ = _≥_
+        ; _⊔_ = _⊓_
+        ; isSemilattice = record
+            { isPreorder = isPreorderFlip (Preorder.isPreorder NatPreorder)
+            ; ⊔-assoc = ⊓-assoc
+            ; ⊔-comm = ⊓-comm
+            ; ⊔-idemp = ⊓-idem
+            ; ⊔-bound = λ x y z x⊓y≡z → (min-bound₁ x⊓y≡z , min-bound₂ x⊓y≡z)
+            ; ⊔-least = min-greatest
             }
         }