From bac68b95f17343e491f461f0c1c51e55f25cb577 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Fri, 14 Jul 2023 18:18:17 -0700
Subject: [PATCH] Add a Lattice instance for natural numbers.

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

diff --git a/Lattice.agda b/Lattice.agda
index c514f4d..057f754 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -154,6 +154,27 @@ private module NatInstances where
             }
         }
 
+    private
+        minmax-absorb : {x y : ℕ} → x ⊓ (x ⊔ y) ≡ x
+        minmax-absorb {x} {y} = ≤-antisym x⊓x⊔y≤x (helper x⊓x≤x⊓x⊔y (⊓-idem x))
+            where
+                x⊓x⊔y≤x = min-bound₁ {x} {x ⊔ y} {x ⊓ (x ⊔ y)} refl
+                x⊓x≤x⊓x⊔y = ⊓-mono-≤ {x} {x} ≤-refl (max-bound₁ {x} {y} {x ⊔ y} refl)
+
+                -- >:(
+                helper : x ⊓ x ≤ x ⊓ (x ⊔ y) → x ⊓ x ≡ x → x ≤ x ⊓ (x ⊔ y)
+                helper x⊓x≤x⊓x⊔y x⊓x≡x rewrite x⊓x≡x = x⊓x≤x⊓x⊔y
+
+        maxmin-absorb : {x y : ℕ} → x ⊔ (x ⊓ y) ≡ x
+        maxmin-absorb {x} {y} = ≤-antisym (helper x⊔x⊓y≤x⊔x (⊔-idem x)) x≤x⊔x⊓y
+            where
+                x≤x⊔x⊓y = max-bound₁ {x} {x ⊓ y} {x ⊔ (x ⊓ y)} refl
+                x⊔x⊓y≤x⊔x = ⊔-mono-≤ {x} {x} ≤-refl (min-bound₁ {x} {y} {x ⊓ y} refl)
+
+                -- >:(
+                helper : x ⊔ (x ⊓ y) ≤ x ⊔ x  → x ⊔ x ≡ x → x ⊔ (x ⊓ y) ≤ x
+                helper x⊔x⊓y≤x⊔x x⊔x≡x rewrite x⊔x≡x = x⊔x⊓y≤x⊔x
+
     NatLattice : Lattice ℕ
     NatLattice = record
         { _≼_ = _≤_
@@ -162,5 +183,7 @@ private module NatInstances where
         ; isLattice = record
             { joinSemilattice = Semilattice.isSemilattice NatMaxSemilattice
             ; meetSemilattice = Semilattice.isSemilattice NatMinSemilattice
+            ; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y}
+            ; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y}
             }
         }