Prove one of the absorption laws

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

Lattice/Builder.agda

@@ -148,6 +148,10 @@ record IsPartialSemilattice {a} {A : Set a}
                 with a₁ ⊔? x | refl⇒a₁⊔?x=nothing refl | x-absorbʳ a₁
         ...       | nothing | refl | ()
 
+
+PartialAbsorb : ∀ {a} {A : Set a} (_≈_ : A → A → Set a) (_⊗₁_ : A → A → Maybe A) (_⊗₂_ : A → A → Maybe A) → Set a
+PartialAbsorb {a} {A} _≈_ _⊗₁_ _⊗₂_ = ∀ (x y : A) →  maybe (λ x⊗₂y → lift-≈ _≈_ (x ⊗₁ x⊗₂y) (just x)) (Trivial _) (x ⊗₂ y)
+
 record IsPartialLattice {a} {A : Set a}
     (_≈_ : A → A → Set a)
     (_⊔?_ : A → A → Maybe A)
@@ -157,8 +161,8 @@ record IsPartialLattice {a} {A : Set a}
         {{partialJoinSemilattice}} : IsPartialSemilattice _≈_ _⊔?_
         {{partialMeetSemilattice}} : IsPartialSemilattice _≈_ _⊓?_
 
-        absorb-⊔-⊓ : (x y : A) →  maybe (λ x⊓y → lift-≈ _≈_ (x ⊔? x⊓y) (just x)) (Trivial _) (x ⊓? y)
+        absorb-⊔-⊓ : PartialAbsorb _≈_ _⊔?_ _⊓?_
-        absorb-⊓-⊔ : (x y : A) →  maybe (λ x⊔y → lift-≈ _≈_ (x ⊓? x⊔y) (just x)) (Trivial _) (x ⊔? y)
+        absorb-⊓-⊔ : PartialAbsorb _≈_ _⊓?_ _⊔?_
 
     open IsPartialSemilattice partialJoinSemilattice
         renaming (HasAbsorbingElement to HasGreatestElement)
@@ -609,6 +613,32 @@ lvMeet-comm = lvCombine-comm PartialLatticeType._⊓?_ PartialLatticeType.⊓-co
 lvMeet-idemp : ∀ {a} (L : List (PartialLatticeType a)) → PartialIdemp (eqL L) (lvMeet L)
 lvMeet-idemp = lvCombine-idemp PartialLatticeType._⊓?_ PartialLatticeType.⊓-idemp
 
+lvCombine-absorb : ∀ {a} (f₁ f₂ : CombineForPLT a) →
+                   (∀ plt →  PartialAbsorb (PartialLatticeType._≈_ plt) (f₁ plt) (f₂ plt)) →
+                   ∀ (L : List (PartialLatticeType a)) →
+                   PartialAbsorb (eqL L) (lvCombine f₁ L) (lvCombine f₂ L)
+lvCombine-absorb f₁ f₂ absorb-f₁-f₂ [] ()
+lvCombine-absorb f₁ f₂ absorb-f₁-f₂ (plt ∷ plts) (inj₁ v₁) (inj₁ v₂)
+    with f₂ plt v₁ v₂ | absorb-f₁-f₂ plt v₁ v₂
+...   | nothing | _ = mkTrivial
+...   | just v₁⊗₂v₂ | v₁⊗₁v₁v₂≈?v₁
+        with f₁ plt v₁ v₁⊗₂v₂ | v₁⊗₁v₁v₂≈?v₁
+...       | just _ | ≈-just v₁⊗₁v₁v₂≈v₁ = ≈-just v₁⊗₁v₁v₂≈v₁
+lvCombine-absorb f₁ f₂ absorb-f₁-f₂ (plt ∷ plts) (inj₂ lv₁) (inj₁ v₂) = mkTrivial
+lvCombine-absorb f₁ f₂ absorb-f₁-f₂ (plt ∷ plts) (inj₁ v₁) (inj₂ lv₂) = mkTrivial
+lvCombine-absorb f₁ f₂ absorb-f₁-f₂ (plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂)
+    with lvCombine f₂ plts lv₁ lv₂ | lvCombine-absorb f₁ f₂ absorb-f₁-f₂ plts lv₁ lv₂
+...   | nothing | _ = mkTrivial
+...   | just lv₁⊗₂lv₂ | lv₁⊗₁lv₁lv₂≈?lv₁
+        with lvCombine f₁ plts lv₁ lv₁⊗₂lv₂ | lv₁⊗₁lv₁lv₂≈?lv₁
+...       | just _ | ≈-just lv₁⊗₁lv₁lv₂≈lv₁ = ≈-just lv₁⊗₁lv₁lv₂≈lv₁
+
+absorb-lvJoin-lvMeet : ∀ {a} (L : List (PartialLatticeType a)) → PartialAbsorb (eqL L) (lvJoin L) (lvMeet L)
+absorb-lvJoin-lvMeet = lvCombine-absorb PartialLatticeType._⊔?_ PartialLatticeType._⊓?_ PartialLatticeType.absorb-⊔-⊓
+
+absorb-lvMeet-lvJoin : ∀ {a} (L : List (PartialLatticeType a)) → PartialAbsorb (eqL L) (lvMeet L) (lvJoin L)
+absorb-lvMeet-lvJoin = lvCombine-absorb PartialLatticeType._⊓?_ PartialLatticeType._⊔?_ PartialLatticeType.absorb-⊓-⊔
+
 lvJoin-greatest-total : ∀ {a} {L : Layer a} →  (lv₁ lv₂ : LayerValue L) →  LayerGreatest L →  lvJoin (toList L) lv₁ lv₂ ≡ nothing → ⊥
 lvJoin-greatest-total {L = plt ∷⁺ []} (inj₁ v₁) (inj₁ v₂) (MkLayerGreatest {{hasGreatest = hasGreatest}}) v₁⊔v₂≡nothing
     with IsPartialLattice.HasGreatestElement.not-partial (PartialLatticeType.isPartialLattice plt) hasGreatest v₁ v₂
@@ -946,6 +976,41 @@ pathMeet'-idemp {Ls = add-via-greatest l ls} (inj₁ lv)
 ...   | just lv⊔lv | ≈-just lv⊔lv≈lv = ≈-just lv⊔lv≈lv
 pathMeet'-idemp {Ls = add-via-greatest l ls} (inj₂ p) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (pathMeet'-idemp {Ls = ls} p)
 
+absorb-pathJoin'-pathMeet' : ∀ {a} {Ls : Layers a} → PartialAbsorb (eqPath' Ls) (pathJoin' Ls) (pathMeet' Ls)
+absorb-pathJoin'-pathMeet' {Ls = single l} lv₁ lv₂ = absorb-lvJoin-lvMeet (toList l) lv₁ lv₂
+absorb-pathJoin'-pathMeet' {Ls = add-via-least l ls} (inj₁ lv₁) (inj₁ lv₂)
+    with lvMeet (toList l) lv₁ lv₂ | absorb-lvJoin-lvMeet (toList l) lv₁ lv₂
+...   | nothing | _ = mkTrivial
+...   | just lv₁⊓lv₂ | lv₁⊔lv₁lv₂≈?lv₁
+        with lvJoin (toList l) lv₁ lv₁⊓lv₂ | lv₁⊔lv₁lv₂≈?lv₁
+...       | just _ | ≈-just lv₁⊔lv₁lv₂≈lv₁ = ≈-just lv₁⊔lv₁lv₂≈lv₁
+absorb-pathJoin'-pathMeet' {Ls = add-via-least l {{least}} ls} (inj₂ p₁) (inj₁ lv₂)
+    = pathJoin'-idemp {Ls = add-via-least l {{least}} ls} (inj₂ p₁)
+absorb-pathJoin'-pathMeet' {Ls = add-via-least l ls} (inj₁ lv₁) (inj₂ p₂)
+    = ≈-just (eqLv-refl l lv₁)
+absorb-pathJoin'-pathMeet' {Ls = add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₂ p₁) (inj₂ p₂)
+    with pathMeet' ls p₁ p₂ | absorb-pathJoin'-pathMeet' {Ls = ls} p₁ p₂
+...   | nothing | _ = mkTrivial
+...   | just p₁⊓p₂ | p₁⊔p₁p₂≈?p₁
+        with pathJoin' ls p₁ p₁⊓p₂ | p₁⊔p₁p₂≈?p₁
+...       | just _ | ≈-just p₁⊔p₁p₂≈p₁ = ≈-just p₁⊔p₁p₂≈p₁
+absorb-pathJoin'-pathMeet' {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂)
+    with lvMeet (toList l) lv₁ lv₂ | absorb-lvJoin-lvMeet (toList l) lv₁ lv₂
+...   | nothing | _ = ≈-just (eqLv-refl l lv₁)
+...   | just lv₁⊓lv₂ | lv₁⊔lv₁lv₂≈?lv₁
+        with lvJoin (toList l) lv₁ lv₁⊓lv₂ | lv₁⊔lv₁lv₂≈?lv₁
+...       | just _ | ≈-just lv₁⊔lv₁lv₂≈lv₁ = ≈-just lv₁⊔lv₁lv₂≈lv₁
+absorb-pathJoin'-pathMeet' {Ls = add-via-greatest l ls {{greatest}} } (inj₂ p₁) (inj₁ lv₂)
+    = pathJoin'-idemp {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁)
+absorb-pathJoin'-pathMeet' {Ls = add-via-greatest l ls} (inj₁ lv₁) (inj₂ p₂)
+    = ≈-just (eqLv-refl l lv₁)
+absorb-pathJoin'-pathMeet' {Ls = add-via-greatest l ls} (inj₂ p₁) (inj₂ p₂)
+    with pathMeet' ls p₁ p₂ | absorb-pathJoin'-pathMeet' {Ls = ls} p₁ p₂
+...   | nothing | _ = mkTrivial
+...   | just p₁⊓p₂ | p₁⊔p₁p₂≈?p₁
+        with pathJoin' ls p₁ p₁⊓p₂ | p₁⊔p₁p₂≈?p₁
+...       | just _ | ≈-just p₁⊔p₁p₂≈p₁ = ≈-just p₁⊔p₁p₂≈p₁
+
 record _≈_ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) : Set a where
     constructor mk-≈
     field pathEq : eqPath' Ls (Path.path p₁) (Path.path p₂)