Define "less than or equal" for partial lattices and prove some properties

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Lattice/Builder.agda

@@ -2,26 +2,23 @@ module Lattice.Builder where
 
 open import Lattice
 open import Equivalence
-open import Data.Maybe as Maybe using (Maybe; just; nothing; _>>=_)
+open import Data.Maybe as Maybe using (Maybe; just; nothing; _>>=_; maybe)
 open import Data.Unit using (⊤; tt)
 open import Data.List.NonEmpty using (List⁺; tail; toList) renaming (_∷_ to _∷⁺_)
 open import Data.List using (List; _∷_; [])
 open import Data.Sum using (_⊎_; inj₁; inj₂)
-open import Data.Product using (Σ)
+open import Data.Product using (Σ; _,_)
+open import Data.Empty using (⊥; ⊥-elim)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
 open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
 
+maybe-injection : ∀ {a} {A : Set a} (x : A) → just x ≡ nothing → ⊥
+maybe-injection x ()
+
 data lift-≈ {a} {A : Set a} (_≈_ : A → A → Set a) : Maybe A → Maybe A → Set a where
     ≈-just : ∀ {a₁ a₂ : A} →  a₁ ≈ a₂ →  lift-≈ _≈_ (just a₁) (just a₂)
     ≈-nothing : lift-≈ _≈_ nothing nothing
 
--- lift-≈-to-≈' : ∀ {a} {A : Set a} (_≈_ : A → A → Set a) (_≈'_ : A → A → Set a) →
---                (∀ x y → (x ≈ y) ≡ (x ≈' y)) →
---                ∀ m₁ m₂ → lift-≈ _≈_ m₁ m₂ → lift-≈ _≈'_ m₁ m₂
--- lift-≈-to-≈' _≈_ _≈'_ ≈≡≈' (just x₁) (just x₂) (≈-just x₁≈x₂)
---     rewrite ≈≡≈' x₁ x₂ = ≈-just x₁≈x₂
--- lift-≈-to-≈' _≈_ _≈'_ ≈≡≈' m₁ m₂ ≈-nothing = ≈-nothing
-
 lift-≈-map : ∀ {a b} {A : Set a} {B : Set b} (f : A → B)
                (_≈ᵃ_ : A → A → Set a) (_≈ᵇ_ : B → B → Set b) →
                (∀ a₁ a₂ → a₁ ≈ᵃ a₂ → f a₁ ≈ᵇ f a₂) →
@@ -54,6 +51,12 @@ PartialComm {a} {A} _≈_ _⊗_ = ∀ (x y : A) →  lift-≈ _≈_ (x ⊗ y) (y
 PartialIdemp : ∀ {a} {A : Set a} (_≈_ : A → A → Set a) (_⊗_ : A → A → Maybe A) → Set a
 PartialIdemp {a} {A} _≈_ _⊗_ = ∀ (x : A) →  lift-≈ _≈_ (x ⊗ x) (just x)
 
+data Trivial a : Set a where
+    instance
+        mkTrivial : Trivial a
+
+data Empty a : Set a where
+
 record IsPartialSemilattice {a} {A : Set a}
     (_≈_ : A → A → Set a)
     (_⊔?_ : A → A → Maybe A) : Set a where
@@ -61,6 +64,9 @@ record IsPartialSemilattice {a} {A : Set a}
     _≈?_ : Maybe A → Maybe A → Set a
     _≈?_ = lift-≈ _≈_
 
+    _≼_ : A → A → Set a
+    _≼_ x y = (x ⊔? y) ≈? (just y)
+
     field
         ≈-equiv : IsEquivalence A _≈_
         ≈-⊔-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈ a₂ → a₃ ≈ a₄ → (a₁ ⊔? a₃) ≈? (a₂ ⊔? a₄)
@@ -69,18 +75,60 @@ record IsPartialSemilattice {a} {A : Set a}
         ⊔-comm : PartialComm _≈_ _⊔?_
         ⊔-idemp : PartialIdemp _≈_ _⊔?_
 
+    open IsEquivalence ≈-equiv public
+    open IsEquivalence (lift-≈-Equivalence {{≈-equiv}}) public using ()
+        renaming (≈-trans to ≈?-trans; ≈-sym to ≈?-sym; ≈-refl to ≈?-refl)
+
+    ≈-≼-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈ a₂ → a₃ ≈ a₄ →  a₁ ≼ a₃ → a₂ ≼ a₄
+    ≈-≼-cong {a₁} {a₂} {a₃} {a₄} a₁≈a₂ a₃≈a₄ a₁≼a₃
+        with a₁ ⊔? a₃ | a₂ ⊔? a₄ | ≈-⊔-cong a₁≈a₂ a₃≈a₄ | a₁≼a₃
+    ...   | just a₁⊔a₃ | just a₂⊔a₄ | ≈-just a₁⊔a₃≈a₂≈a₄ | ≈-just a₁⊔a₃≈a₃
+          = ≈-just (≈-trans (≈-trans (≈-sym a₁⊔a₃≈a₂≈a₄) a₁⊔a₃≈a₃) a₃≈a₄)
+
+    -- curious: similar property (properties?) to partial commutative monoids (PCMs)
+    -- from Iris.
+    ≼-partialˡ : ∀ {a a₁ a₂} → a₁ ≼ a₂ →  (a ⊔? a₁) ≡ nothing → (a ⊔? a₂) ≡ nothing
+    ≼-partialˡ {a} {a₁} {a₂} a₁≼a₂ a⊔a₁≡nothing
+        with a₁ ⊔? a₂ | a₁≼a₂ | a ⊔? a₁ | a⊔a₁≡nothing | ⊔-assoc a a₁ a₂
+    ...   | just a₁⊔a₂ | ≈-just a₁⊔a₂≈a₂ | nothing | refl | aa₁⊔a₂≈a⊔a₁a₂
+            with a ⊔? a₁⊔a₂ | aa₁⊔a₂≈a⊔a₁a₂ | a ⊔? a₂ | ≈-⊔-cong (≈-refl {a = a}) a₁⊔a₂≈a₂
+    ...       | nothing | ≈-nothing | nothing | ≈-nothing = refl
+
+    ≼-partialʳ : ∀ {a a₁ a₂} → a₁ ≼ a₂ →  (a₁ ⊔? a) ≡ nothing → (a₂ ⊔? a) ≡ nothing
+    ≼-partialʳ {a} {a₁} {a₂} a₁≼a₂ a₁⊔a≡nothing
+        with a₁ ⊔? a | a ⊔? a₁ | a₁⊔a≡nothing | ⊔-comm a₁ a | ≼-partialˡ {a} {a₁} {a₂} a₁≼a₂
+    ...   | nothing | nothing | refl | ≈-nothing | refl⇒a⊔a₂=nothing
+            with a₂ ⊔? a | a ⊔? a₂ | ⊔-comm a₂ a | refl⇒a⊔a₂=nothing refl
+    ...       | nothing | nothing | ≈-nothing | refl = refl
+
+    ≼-refl : ∀ (x : A) →  x ≼ x
+    ≼-refl x = ⊔-idemp x
+
+    ≼-refl' : ∀ {a₁ a₂ : A} → a₁ ≈ a₂ → a₁ ≼ a₂
+    ≼-refl' {a₁} {a₂} a₁≈a₂ = ≈-≼-cong ≈-refl a₁≈a₂ (≼-refl a₁)
+
+    x⊔?x≼x : ∀ (x : A) →  maybe (λ x⊔x →  x⊔x ≼ x) (Empty a) (x ⊔? x)
+    x⊔?x≼x x
+        with x ⊔? x | ⊔-idemp x
+    ...   | just x⊔x | ≈-just x⊔x≈x = ≈-≼-cong (≈-sym x⊔x≈x) ≈-refl (≼-refl x)
+
+    x≼x⊔?y : ∀ (x y : A) →  maybe (λ x⊔y →  x ≼ x⊔y) (Trivial a) (x ⊔? y)
+    x≼x⊔?y x y
+        with x ⊔? y in x⊔?y= | x ⊔? x | ⊔-idemp x | ⊔-assoc x x y | x⊔?x≼x x
+    ...   | nothing  | _ | _ | _ | _ = mkTrivial
+    ...   | just x⊔y | just x⊔x | ≈-just x⊔x≈x | ⊔-assoc-xxy | x⊔x≼x
+            with x⊔x ⊔? y in xx⊔?y= | x ⊔? x⊔y
+    ...       | nothing | nothing =
+                ⊥-elim (maybe-injection _ (trans (sym x⊔?y=) (≼-partialʳ x⊔x≼x xx⊔?y=)))
+    ...       | just xx⊔y | just x⊔xy rewrite (sym xx⊔?y=) rewrite (sym x⊔?y=) =
+                ≈?-trans (≈?-sym ⊔-assoc-xxy) (≈-⊔-cong x⊔x≈x (≈-refl {a = y}))
+
     record HasIdentityElement : Set a where
         field
             x : A
             not-partial : ∀ (a₁ a₂ : A) →  Σ A (λ a₃ →  (a₁ ⊔? a₂) ≡ just a₃)
             x-identity : (a : A) → (x ⊔? a) ≈? just a
 
-data Trivial a : Set a where
-    instance
-        mkTrivial : Trivial a
-
-data Empty a : Set a where
-
 Maybe-≈ : ∀ {a} {A : Set a} → (_≈_ : A → A → Set a) → Maybe A →  A → Set a
 Maybe-≈ _≈_ (just a₁) a₂ = a₁ ≈ a₂
 Maybe-≈ {a} _≈_ nothing a₂ = Trivial a