[WIP] Start lattice and semilattice proofs for Nat

Lattice.agda

@@ -1,39 +1,114 @@
 module Lattice where
 
-open import Relation.Binary.PropositionalEquality
+import Data.Nat.Properties as NatProps
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
 open import Relation.Binary.Definitions
-open import Data.Nat using (ℕ; _≤_)
-open import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym)
+open import Data.Nat as Nat using (ℕ; _≤_)
+open import Data.Product using (_×_; _,_)
 open import Agda.Primitive using (lsuc)
 
+open import NatMap using (NatMap)
+
+record IsPreorder {a} (A : Set a) (_≼_ : A → A → Set a) : Set a where
+    field
+        ≼-refl : Reflexive (_≼_)
+        ≼-trans : Transitive (_≼_)
+        ≼-antisym : Antisymmetric (_≡_) (_≼_)
+
 record Preorder {a} (A : Set a) : Set (lsuc a) where
     field
         _≼_ : A → A → Set a
 
-        ≼-refl : Reflexive (_≼_)
-        ≼-trans : Transitive (_≼_)
-        ≼-antisym : Antisymmetric (_≡_) (_≼_)
+        isPreorder : IsPreorder A _≼_
 
-record Semilattice {a} (A : Set a) : Set (lsuc a) where
+    open IsPreorder isPreorder public
+
+record IsSemilattice {a} (A : Set a) (_≼_ : A → A → Set a) (_⊔_ : A → A → A) : Set a where
     field
-        _⊔_ : A → A → A
+        isPreorder : IsPreorder A _≼_
 
-        ⊔-assoc : (x : A) → (y : A) → (z : A) → x ⊔ (y ⊔ z) ≡ (x ⊔ y) ⊔ z
+        ⊔-assoc : (x : A) → (y : A) → (z : A) → (x ⊔ y) ⊔ z ≡ x ⊔ (y ⊔ z)
         ⊔-comm : (x : A) → (y : A) → x ⊔ y ≡ y ⊔ x
         ⊔-idemp : (x : A) → x ⊔ x ≡ x
 
-record Lattice {a} (A : Set a) : Set (lsuc a) where
-    field
-        joinSemilattice : Semilattice A
-        meetSemilattice : Semilattice A
+        ⊔-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'
 
-    _⊔_ = Semilattice._⊔_ joinSemilattice
-    _⊓_ = Semilattice._⊔_ meetSemilattice
+    open IsPreorder isPreorder public
+
+record Semilattice {a} (A : Set a) : Set (lsuc a) where
+    field
+        _≼_ : A → A → Set a
+        _⊔_ : A → A → A
+
+        isSemilattice : IsSemilattice A _≼_ _⊔_
+
+    open IsSemilattice isSemilattice public
+
+record IsLattice {a} (A : Set a) (_≼_ : A → A → Set a) (_⊔_ : A → A → A) (_⊓_ : A → A → A) : Set a where
+
+    _≽_ : A → A → Set a
+    a ≽ b = b ≼ a
 
     field
+        joinSemilattice : IsSemilattice A _≼_ _⊔_
+        meetSemilattice : IsSemilattice A _≽_ _⊓_
+
         absorb-⊔-⊓ : (x : A) → (y : A) → x ⊔ (x ⊓ y) ≡ x
         absorb-⊓-⊔ : (x : A) → (y : A) → x ⊓ (x ⊔ y) ≡ x
 
-instance
+    open IsSemilattice joinSemilattice public
+    open IsSemilattice meetSemilattice public renaming
+        ( ⊔-assoc to ⊓-assoc
+        ; ⊔-comm to ⊓-comm
+        ; ⊔-idemp to ⊓-idemp
+        ; ⊔-bound to ⊓-bound
+        ; ⊔-least to ⊓-least
+        )
+
+
+record Lattice {a} (A : Set a) : Set (lsuc a) where
+    field
+        _≼_ : A → A → Set a
+        _⊔_ : A → A → A
+        _⊓_ : A → A → A
+
+        isLattice : IsLattice A _≼_ _⊔_ _⊓_
+
+    open IsLattice isLattice public
+
+private module NatInstances where
+    open Nat
+    open NatProps
+    open Eq
+
     NatPreorder : Preorder ℕ
-    NatPreorder = record { _≼_ = _≤_; ≼-refl = ≤-refl; ≼-trans = ≤-trans; ≼-antisym = ≤-antisym }
+    NatPreorder = record
+        { _≼_ = _≤_
+        ; isPreorder = record
+            { ≼-refl = ≤-refl
+            ; ≼-trans = ≤-trans
+            ; ≼-antisym = ≤-antisym
+            }
+        }
+
+    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 → 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
+        { _≼_ = _≤_
+        ; _⊔_ = _⊔_
+        ; isSemilattice = record
+            { isPreorder = Preorder.isPreorder NatPreorder
+            ; ⊔-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)
+            }
+        }