Moved the Nat lattice instance into an actual file

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-09-23 15:34:59 -07:00
parent 5d54e62c3a
commit dce21b3696
2 changed files with 83 additions and 83 deletions
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -140,44 +140,6 @@ record Lattice {a} (A : Set a) : Set (lsuc a) where
    open IsLattice isLattice public

 module IsSemilatticeInstances where
-    module ForNat where
-        open Nat
-        open NatProps
-        open Eq
-
-        private
-            ≡-⊔-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≡ a₂ → a₃ ≡ a₄ → (a₁ ⊔ a₃) ≡ (a₂ ⊔ a₄)
-            ≡-⊔-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl
-
-            ≡-⊓-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≡ a₂ → a₃ ≡ a₄ → (a₁ ⊓ a₃) ≡ (a₂ ⊓ a₄)
-            ≡-⊓-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl
-
-        NatIsMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
-        NatIsMaxSemilattice = record
-            { ≈-equiv = record
-                { ≈-refl = refl
-                ; ≈-sym = sym
-                ; ≈-trans = trans
-                }
-            ; ≈-⊔-cong = ≡-⊔-cong
-            ; ⊔-assoc = ⊔-assoc
-            ; ⊔-comm = ⊔-comm
-            ; ⊔-idemp = ⊔-idem
-            }
-
-        NatIsMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
-        NatIsMinSemilattice = record
-            { ≈-equiv = record
-                { ≈-refl = refl
-                ; ≈-sym = sym
-                ; ≈-trans = trans
-                }
-            ; ≈-⊔-cong = ≡-⊓-cong
-            ; ⊔-assoc = ⊓-assoc
-            ; ⊔-comm = ⊓-comm
-            ; ⊔-idemp = ⊓-idem
-            }
-
    module ForProd {a} {A B : Set a}
        (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
        (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
@@ -216,51 +178,6 @@ module IsSemilatticeInstances where
            }

 module IsLatticeInstances where
-    module ForNat where
-        open Nat
-        open NatProps
-        open Eq
-        open IsSemilatticeInstances.ForNat
-        open Data.Product
-
-        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)
-
-            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)
-
-            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
-
-        NatIsLattice : IsLattice ℕ _≡_ _⊔_ _⊓_
-        NatIsLattice = record
-            { joinSemilattice = NatIsMaxSemilattice
-            ; meetSemilattice = NatIsMinSemilattice
-            ; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y}
-            ; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y}
-            }
-
    module ForProd {a} {A B : Set a}
        (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
        (_⊔₁_ : A → A → A) (_⊓₁_ : A → A → A)
--- a/Lattice/Nat.agda
+++ b/Lattice/Nat.agda
@@ -0,0 +1,83 @@
+module Lattice.Nat where
+
+open import Equivalence
+open import Lattice
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
+open import Data.Nat using (ℕ; _⊔_; _⊓_; _≤_)
+open import Data.Nat.Properties using 
+    ( ⊔-assoc; ⊔-comm; ⊔-idem
+    ; ⊓-assoc; ⊓-comm; ⊓-idem
+    ; ⊓-mono-≤; ⊔-mono-≤
+    ; m≤n⇒m≤o⊔n; m≤n⇒m⊓o≤n; ≤-refl; ≤-antisym
+    )
+
+private
+    ≡-⊔-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≡ a₂ → a₃ ≡ a₄ → (a₁ ⊔ a₃) ≡ (a₂ ⊔ a₄)
+    ≡-⊔-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl
+
+    ≡-⊓-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≡ a₂ → a₃ ≡ a₄ → (a₁ ⊓ a₃) ≡ (a₂ ⊓ a₄)
+    ≡-⊓-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl
+
+NatIsMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
+NatIsMaxSemilattice = record
+    { ≈-equiv = record
+        { ≈-refl = refl
+        ; ≈-sym = sym
+        ; ≈-trans = trans
+        }
+    ; ≈-⊔-cong = ≡-⊔-cong
+    ; ⊔-assoc = ⊔-assoc
+    ; ⊔-comm = ⊔-comm
+    ; ⊔-idemp = ⊔-idem
+    }
+
+NatIsMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
+NatIsMinSemilattice = record
+    { ≈-equiv = record
+        { ≈-refl = refl
+        ; ≈-sym = sym
+        ; ≈-trans = trans
+        }
+    ; ≈-⊔-cong = ≡-⊓-cong
+    ; ⊔-assoc = ⊓-assoc
+    ; ⊔-comm = ⊓-comm
+    ; ⊔-idemp = ⊓-idem
+    }
+
+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)
+
+    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)
+
+    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
+
+NatIsLattice : IsLattice ℕ _≡_ _⊔_ _⊓_
+NatIsLattice = record
+    { joinSemilattice = NatIsMaxSemilattice
+    ; meetSemilattice = NatIsMinSemilattice
+    ; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y}
+    ; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y}
+    }