Prove some quasi-homomorphism properties

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

Lattice/Builder.agda

@@ -385,29 +385,42 @@ eval : ∀ {a} {A : Set a} (_⊔?_ : A → A → Maybe A) (e : Expr A) → Maybe
 eval _⊔?_ (` x) = just x
 eval _⊔?_ (e₁ ∨ e₂) = (eval _⊔?_ e₁) >>= (λ v₁ →  (eval _⊔?_ e₂) >>= (v₁ ⊔?_))
 
--- the two lvCombine homomorphism properties essentially say that, when all layer values
+-- a function is "partially sub-homomorphic" for some subset of B (image of f) if
--- are from the same type, the lvCombine preserves the structure of operations
+-- for (f A), it preserves the structure of operations _⊕ on A in B.
--- on these layer values.
+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₂)
+
+-- 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.
+--
+-- i.e., if (f a) ⊗ (f b) = Maybe.map f (a ⊕ b), then we can make similar claims about f (a ⊕ b ⊕ c)
+eval-subHomo : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (_⊕_ : A → A → Maybe A) (_⊗_ : B → B → Maybe B) (e : Expr A) →
+               PartiallySubHomo f _⊕_ _⊗_ →
+               eval _⊗_ (map f e) ≡ Maybe.map f (eval _⊕_ e)
+eval-subHomo f _⊕_ _⊗_ (` _) psh = refl
+eval-subHomo f _⊕_ _⊗_ (e₁ ∨ e₂) psh
+    rewrite eval-subHomo f _⊕_ _⊗_ e₁ psh rewrite eval-subHomo f _⊕_ _⊗_ e₂ psh
+    with eval _⊕_ e₁ | eval _⊕_ e₂
+...   | just x₁ | just x₂ = psh x₁ x₂
+...   | nothing | nothing = refl
+...   | just x₁ | nothing = refl
+...   | nothing | just x₂ = refl
 
 lvCombine-homo₁ : ∀ {a} plt plts (f : CombineForPLT a) (e : Expr (PartialLatticeType.EltType plt)) → eval (lvCombine f (plt ∷ plts)) (map inj₁ e) ≡ Maybe.map inj₁ (eval (f plt) e)
-lvCombine-homo₁ plt plts f (` _) = refl
+lvCombine-homo₁ plt plts f e = eval-subHomo inj₁ (f plt) (lvCombine f (plt ∷ plts)) e (λ a₁ a₂ → refl)
-lvCombine-homo₁ plt plts f (e₁ ∨ e₂)
-    rewrite lvCombine-homo₁ plt plts f e₁ rewrite lvCombine-homo₁ plt plts f e₂
-    with eval (f plt) e₁ | eval (f plt) e₂
-...   | just x₁ | just x₂ = refl
-...   | nothing | nothing = refl
-...   | just x₁ | nothing = refl
-...   | nothing | just x₂ = refl
 
 lvCombine-homo₂ : ∀ {a} plt plts (f : CombineForPLT a) (e : Expr (ListValue plts)) → eval (lvCombine f (plt ∷ plts)) (map inj₂ e) ≡ Maybe.map inj₂ (eval (lvCombine f plts) e)
-lvCombine-homo₂ plt plts f (` _) = refl
+lvCombine-homo₂ plt plts f e = eval-subHomo inj₂ (lvCombine f plts) (lvCombine f (plt ∷ plts)) e (λ a₁ a₂ → refl)
-lvCombine-homo₂ plt plts f (e₁ ∨ e₂)
+
-    rewrite lvCombine-homo₂ plt plts f e₁ rewrite lvCombine-homo₂ plt plts f e₂
+pathJoin'-homo-least₁ : ∀ {a} (l : Layer a) (ls : Layers a) least (e : Expr (LayerValue l)) → eval (pathJoin' (add-via-least l {{least}} ls)) (map inj₁ e) ≡ Maybe.map inj₁ (eval (lvJoin (toList l)) e)
-    with eval (lvCombine f plts) e₁ | eval (lvCombine f plts) e₂
+pathJoin'-homo-least₁ l ls least e = eval-subHomo inj₁ (lvJoin (toList l)) (pathJoin' (add-via-least l {{least}} ls)) e (λ a₁ a₂ → refl)
-...   | just x₁ | just x₂ = refl
+
-...   | nothing | nothing = refl
+pathJoin'-homo-greatest₁ : ∀ {a} (l : Layer a) (ls : Layers a) greatest (e : Expr (LayerValue l)) → eval (pathJoin' (add-via-greatest l ls {{greatest}})) (map inj₁ e) ≡ Maybe.map inj₁ (eval (lvJoin (toList l)) e)
-...   | just x₁ | nothing = refl
+pathJoin'-homo-greatest₁ l ls greatest e = eval-subHomo inj₁ (lvJoin (toList l)) (pathJoin' (add-via-greatest l ls {{greatest}})) e (λ a₁ a₂ → refl)
-...   | nothing | just x₂ = refl
+
+pathJoin'-homo-greatest₂ : ∀ {a} (l : Layer a) (ls : Layers a) greatest (e : Expr (Path' ls)) → eval (pathJoin' (add-via-greatest l ls {{greatest}})) (map inj₂ e) ≡ Maybe.map inj₂ (eval (pathJoin' ls) e)
+pathJoin'-homo-greatest₂ l ls greatest e = eval-subHomo inj₂ (pathJoin' ls) (pathJoin' (add-via-greatest l ls {{greatest}})) e (λ a₁ a₂ → refl)
 
 lvCombine-assoc : ∀ {a} (f : CombineForPLT a) →
                   (∀ plt →  PartialAssoc (PartialLatticeType._≈_ plt) (f plt)) →