Write a lemma to wrangle PartialAbsorb proofs

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

Lattice/Builder.agda

@@ -512,6 +512,24 @@ eval _⊔?_ (e₁ ∨ e₂) = (eval _⊔?_ e₁) >>= (λ v₁ →  (eval _⊔?_
 PartiallySubHomo : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (_⊕_ : A → A → Maybe A) (_⊗_ : B → B → Maybe B) → Set (a ⊔ℓ b)
 PartiallySubHomo {A = A} f _⊕_ _⊗_ = ∀ (a₁ a₂ : A) →  (f a₁ ⊗ f a₂) ≡ Maybe.map f (a₁ ⊕ a₂)
 
+PartialAbsorb-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₂) →
+                    ∀ (_⊕₁_ : A → A → Maybe A) (_⊕₂_ : A → A → Maybe A)
+                      (_⊗₁_ : B → B → Maybe B) (_⊗₂_ : B → B → Maybe B) →
+                      PartiallySubHomo f _⊕₁_ _⊗₁_ →
+                      PartiallySubHomo f _⊕₂_ _⊗₂_ →
+                      PartialAbsorb _≈ᵃ_ _⊕₁_ _⊕₂_ →
+                      ∀ (x y : A) →  maybe (λ x⊗₂y → lift-≈ _≈ᵇ_ (f x ⊗₁ x⊗₂y) (just (f x))) (Trivial _) (f x ⊗₂ f y)
+PartialAbsorb-map f _≈ᵃ_ _≈ᵇ_ ≈ᵃ⇒≈ᵇ _⊕₁_ _⊕₂_ _⊗₁_ _⊗₂_ psh₁ psh₂ absorbᵃ x y
+    with x ⊕₂ y | f x ⊗₂ f y | psh₂ x y | absorbᵃ x y
+...   | nothing | nothing | refl | _ = mkTrivial
+...   | just x⊕₂y | just fx⊗₂fy | refl | x⊕₁xy≈?x
+        with x ⊕₁ x⊕₂y | f x ⊗₁ (f x⊕₂y) | psh₁ x x⊕₂y | x⊕₁xy≈?x
+...       |  just x⊕₁xy | just fx⊗₁fx⊕₂y | refl | ≈-just x⊕₁xy≈x = ≈-just (≈ᵃ⇒≈ᵇ _ _ x⊕₁xy≈x)
+
+
 -- this evaluation property, which depends on PartiallySubHomo, effectively makes
 -- it easier to talk about compound operations and the preservation of their
 -- structure when _⊗_ is PartiallySubHomo.
@@ -619,19 +637,17 @@ lvCombine-absorb : ∀ {a} (f₁ f₂ : CombineForPLT 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₂
+    = PartialAbsorb-map inj₁ _ _ (λ _ _ x → x) (f₁ plt) (f₂ plt)
-...   | nothing | _ = mkTrivial
+                                 (lvCombine f₁ (plt ∷ plts)) (lvCombine f₂ (plt ∷ plts))
-...   | just v₁⊗₂v₂ | v₁⊗₁v₁v₂≈?v₁
+                                 (λ _ _ → refl) (λ _ _ → refl)
-        with f₁ plt v₁ v₁⊗₂v₂ | v₁⊗₁v₁v₂≈?v₁
+                                 (absorb-f₁-f₂ plt) 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₂
+    = PartialAbsorb-map inj₂ _ _ (λ _ _ x → x) (lvCombine f₁ plts) (lvCombine f₂ plts)
-...   | nothing | _ = mkTrivial
+                                 (lvCombine f₁ (plt ∷ plts)) (lvCombine f₂ (plt ∷ plts))
-...   | just lv₁⊗₂lv₂ | lv₁⊗₁lv₁lv₂≈?lv₁
+                                 (λ _ _ → refl) (λ _ _ → refl)
-        with lvCombine f₁ plts lv₁ lv₁⊗₂lv₂ | lv₁⊗₁lv₁lv₂≈?lv₁
+                                 (lvCombine-absorb f₁ f₂  absorb-f₁-f₂ plts) 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-⊔-⊓
@@ -978,12 +994,11 @@ pathMeet'-idemp {Ls = add-via-greatest l ls} (inj₂ p) = lift-≈-map inj₂ _
 
 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₂)
+absorb-pathJoin'-pathMeet' {Ls = Ls@(add-via-least l ls)} (inj₁ lv₁) (inj₁ lv₂)
-    with lvMeet (toList l) lv₁ lv₂ | absorb-lvJoin-lvMeet (toList l) lv₁ lv₂
+    = PartialAbsorb-map inj₁ _ _ (λ _ _ x → x) (lvJoin (toList l)) (lvMeet (toList l))
-...   | nothing | _ = mkTrivial
+                                 (pathJoin' Ls) (pathMeet' Ls)
-...   | just lv₁⊓lv₂ | lv₁⊔lv₁lv₂≈?lv₁
+                                 (λ _ _ → refl) (λ _ _ → refl)
-        with lvJoin (toList l) lv₁ lv₁⊓lv₂ | lv₁⊔lv₁lv₂≈?lv₁
+                                 (absorb-lvJoin-lvMeet (toList l)) 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₂)
@@ -1004,12 +1019,11 @@ absorb-pathJoin'-pathMeet' {Ls = add-via-greatest l ls {{greatest}} } (inj₂ p
     = 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₂)
+absorb-pathJoin'-pathMeet' {Ls = Ls@(add-via-greatest l ls)} (inj₂ p₁) (inj₂ p₂)
-    with pathMeet' ls p₁ p₂ | absorb-pathJoin'-pathMeet' {Ls = ls} p₁ p₂
+    = PartialAbsorb-map inj₂ _ _ (λ _ _ x → x) (pathJoin' ls) (pathMeet' ls)
-...   | nothing | _ = mkTrivial
+                                 (pathJoin' Ls) (pathMeet' Ls)
-...   | just p₁⊓p₂ | p₁⊔p₁p₂≈?p₁
+                                 (λ _ _ → refl) (λ _ _ → refl)
-        with pathJoin' ls p₁ p₁⊓p₂ | p₁⊔p₁p₂≈?p₁
+                                 (absorb-pathJoin'-pathMeet' {Ls = ls}) 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-≈