From 3b29ee0f749b92a27d0f30c172694ea9ae789b49 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Fri, 14 Jul 2023 21:20:16 -0700
Subject: [PATCH] Add a Semilattice isntance for Products.

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

diff --git a/Lattice.agda b/Lattice.agda
index bde9fcd..920a4cd 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -99,7 +99,7 @@ module PreorderInstances where
                 }
             }
 
-    module ForProd {a} {A B : Set a} {{ pA : Preorder A }} {{ pB : Preorder B }} where
+    module ForProd {a} {A B : Set a} (pA : Preorder A) (pB : Preorder B) where
         open Eq
 
         private
@@ -188,6 +188,74 @@ module SemilatticeInstances where
                 }
             }
 
+    module ForProd {a} {A B : Set a} (sA : Semilattice A) (sB : Semilattice B) where
+        private
+            _≼₁_ = Semilattice._≼_ sA
+            _≼₂_ = Semilattice._≼_ sB
+
+            pA = record { _≼_ = _≼₁_; isPreorder = Semilattice.isPreorder sA }
+            pB = record { _≼_ = _≼₂_; isPreorder = Semilattice.isPreorder sB }
+
+        open PreorderInstances.ForProd pA pB
+        open Eq
+        open Data.Product
+
+        private
+            _≼_ = Preorder._≼_ ProdPreorder
+
+            _⊔_ : A × B → A × B → A × B
+            (a₁ , b₁) ⊔ (a₂ , b₂) = (Semilattice._⊔_ sA a₁ a₂ , Semilattice._⊔_ sB b₁ b₂)
+
+            ⊔-assoc : (p₁ p₂ p₃ : A × B) → (p₁ ⊔ p₂) ⊔ p₃ ≡ p₁ ⊔ (p₂ ⊔ p₃)
+            ⊔-assoc (a₁ , b₁) (a₂ , b₂) (a₃ , b₃)
+                rewrite Semilattice.⊔-assoc sA a₁ a₂ a₃
+                rewrite Semilattice.⊔-assoc sB b₁ b₂ b₃ = refl
+
+            ⊔-comm : (p₁ p₂ : A × B) → p₁ ⊔ p₂ ≡ p₂ ⊔ p₁
+            ⊔-comm (a₁ , b₁) (a₂ , b₂)
+                rewrite Semilattice.⊔-comm sA a₁ a₂
+                rewrite Semilattice.⊔-comm sB b₁ b₂ = refl
+
+            ⊔-idemp : (p : A × B) → p ⊔ p ≡ p
+            ⊔-idemp (a , b)
+                rewrite Semilattice.⊔-idemp sA a
+                rewrite Semilattice.⊔-idemp sB b = refl
+
+            ⊔-bound₁ : {p₁ p₂ p₃ : A × B} → p₁ ⊔ p₂ ≡ p₃ → p₁ ≼ p₃
+            ⊔-bound₁ {(a₁ , b₁)} {(a₂ , b₂)} {(a₃ , b₃)} p₁⊔p₂≡p₃ = (⊔-bound-a , ⊔-bound-b)
+                where
+                    ⊔-bound-a = proj₁ (Semilattice.⊔-bound sA a₁ a₂ a₃ (cong proj₁ p₁⊔p₂≡p₃))
+                    ⊔-bound-b = proj₁ (Semilattice.⊔-bound sB b₁ b₂ b₃ (cong proj₂ p₁⊔p₂≡p₃))
+
+            ⊔-bound₂ : {p₁ p₂ p₃ : A × B} → p₁ ⊔ p₂ ≡ p₃ → p₂ ≼ p₃
+            ⊔-bound₂ {(a₁ , b₁)} {(a₂ , b₂)} {(a₃ , b₃)} p₁⊔p₂≡p₃ = (⊔-bound-a , ⊔-bound-b)
+                where
+                    ⊔-bound-a = proj₂ (Semilattice.⊔-bound sA a₁ a₂ a₃ (cong proj₁ p₁⊔p₂≡p₃))
+                    ⊔-bound-b = proj₂ (Semilattice.⊔-bound sB b₁ b₂ b₃ (cong proj₂ p₁⊔p₂≡p₃))
+
+            ⊔-least : (p₁ p₂ p₃ : A × B) → p₁ ⊔ p₂ ≡ p₃ → ∀ (p₃' : A × B) → (p₁ ≼ p₃' × p₂ ≼ p₃') → p₃ ≼ p₃'
+            ⊔-least (a₁ , b₁) (a₂ , b₂) (a₃ , b₃) p₁⊔p₂≡p₃ (a₃' , b₃') (p₁≼p₃' , p₂≼p₃') = (⊔-least-a , ⊔-least-b)
+                where
+                    ⊔-least-a : a₃ ≼₁ a₃'
+                    ⊔-least-a = Semilattice.⊔-least sA a₁ a₂ a₃ (cong proj₁ p₁⊔p₂≡p₃) a₃' (proj₁ p₁≼p₃' , proj₁ p₂≼p₃')
+
+                    ⊔-least-b : b₃ ≼₂ b₃'
+                    ⊔-least-b = Semilattice.⊔-least sB b₁ b₂ b₃ (cong proj₂ p₁⊔p₂≡p₃) b₃' (proj₂ p₁≼p₃' , proj₂ p₂≼p₃')
+
+        ProdSemilattice : Semilattice (A × B)
+        ProdSemilattice = record
+            { _≼_ = _≼_
+            ; _⊔_ = _⊔_
+            ; isSemilattice = record
+                { isPreorder = Preorder.isPreorder ProdPreorder
+                ; ⊔-assoc = ⊔-assoc
+                ; ⊔-comm = ⊔-comm
+                ; ⊔-idemp = ⊔-idemp
+                ; ⊔-bound = λ x y z x⊓y≡z → (⊔-bound₁ x⊓y≡z , ⊔-bound₂ x⊓y≡z)
+                ; ⊔-least = ⊔-least
+                }
+            }
+
 private module NatInstances where
     open Nat
     open NatProps
@@ -230,11 +298,11 @@ private module NatInstances where
             }
         }
 
-    ProdSemilattice : {a : Level} → {A B : Set a} → {{ Semilattice A }} → {{ Semilattice B }} → Semilattice (A × B)
-    ProdSemilattice {a} {A} {B} {{slA}} {{slB}} = record
-        { _≼_ = λ (a₁ ,  b₁) (a₂ , b₂) → Semilattice._≼_ slA a₁ a₂ × Semilattice._≼_ slB b₁ b₂
-        ; _⊔_ = λ (a₁ ,  b₁) (a₂ , b₂) → (Semilattice._⊔_ slA a₁ a₂ , Semilattice._⊔_ slB b₁ b₂)
-        ; isSemilattice = record
-            {
-            }
-        }
+    -- ProdSemilattice : {a : Level} → {A B : Set a} → {{ Semilattice A }} → {{ Semilattice B }} → Semilattice (A × B)
+    -- ProdSemilattice {a} {A} {B} {{slA}} {{slB}} = record
+    --     { _≼_ = λ (a₁ ,  b₁) (a₂ , b₂) → Semilattice._≼_ slA a₁ a₂ × Semilattice._≼_ slB b₁ b₂
+    --     ; _⊔_ = λ (a₁ ,  b₁) (a₂ , b₂) → (Semilattice._⊔_ slA a₁ a₂ , Semilattice._⊔_ slB b₁ b₂)
+    --     ; isSemilattice = record
+    --         {
+    --         }
+    --     }