Prove commutativity and associativity of value joining

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

Lattice/Builder.agda

@@ -80,10 +80,7 @@ record IsPartialSemilattice {a} {A : Set a}
         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₃
+    ≈-≼-cong {a₁} {a₂} {a₃} {a₄} a₁≈a₂ a₃≈a₄ a₁≼a₃ = ≈?-trans (≈?-trans (≈?-sym (≈-⊔-cong a₁≈a₂ a₃≈a₄)) a₁≼a₃) (≈-just 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.
@@ -242,10 +239,7 @@ CombineForPLT a = ∀ (plt : PartialLatticeType a) → PartialLatticeType.EltTyp
 
 lvCombine : ∀ {a} (f : CombineForPLT a) (l : List (PartialLatticeType a)) (lv₁ lv₂ : ListValue l) →  Maybe (ListValue l)
 lvCombine _ [] _ _ = nothing
-lvCombine f (plt ∷ plts) (inj₁ v₁) (inj₁ v₂)
+lvCombine f (plt ∷ plts) (inj₁ v₁) (inj₁ v₂) = Maybe.map inj₁ (f plt v₁ v₂)
-    with f plt v₁ v₂
-...   | just v = just (inj₁ v)
-...   | nothing = nothing
 lvCombine f (_ ∷ plts) (inj₂ lv₁) (inj₂ lv₂) = Maybe.map inj₂ (lvCombine f plts lv₁ lv₂)
 lvCombine _ (_ ∷ plts) (inj₁ _) (inj₂ _) = nothing
 lvCombine _ (_ ∷ plts) (inj₂ _) (inj₁ _) = nothing
@@ -326,29 +320,95 @@ eqPath'-refl (add-via-greatest l ls) (inj₂ p) = eqPath'-refl ls p
 -- Now that we can compare paths for "equality", we can state and
 -- prove theorems such as commutativity and idempotence.
 
+data Expr {a} (A : Set a) : Set a where
+    `_ : A →  Expr A
+    _∨_ : Expr A → Expr A → Expr A
+
+map : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) → Expr A → Expr B
+map f (` x) = ` (f x)
+map f (e₁ ∨ e₂) = map f e₁ ∨ map f e₂
+
+eval : ∀ {a} {A : Set a} (_⊔?_ : A → A → Maybe A) (e : Expr A) → Maybe A
+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
+-- are from the same type, the lvCombine preserves the structure of operations
+-- on these layer values.
+
+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₁ ∨ 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₁ ∨ e₂)
+    rewrite lvCombine-homo₂ plt plts f e₁ rewrite lvCombine-homo₂ plt plts f e₂
+    with eval (lvCombine f plts) e₁ | eval (lvCombine f plts) e₂
+...   | just x₁ | just x₂ = refl
+...   | nothing | nothing = refl
+...   | just x₁ | nothing = refl
+...   | nothing | just x₂ = refl
+
 lvCombine-comm : ∀ {a} (f : CombineForPLT a) →
                  (∀ plt →  PartialComm (PartialLatticeType._≈_ plt) (f plt)) →
                  ∀ (L : List (PartialLatticeType a)) →
                  PartialComm (eqL L) (lvCombine f L)
 lvCombine-comm f f-comm L@(plt ∷ plts) lv₁@(inj₁ v₁) (inj₁ v₂)
-    with f plt v₁ v₂
+    rewrite lvCombine-homo₁ plt plts f ((` v₁) ∨ (` v₂)) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (f-comm plt v₁ v₂)
-      |  f plt v₂ v₁
+lvCombine-comm f f-comm (plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (lvCombine-comm f f-comm plts lv₁ lv₂)
-      |  f-comm plt v₁ v₂
-...   | _ | _ | ≈-just v₁v₂≈v₂v₁ = ≈-just v₁v₂≈v₂v₁
-...   | _ | _ | ≈-nothing = ≈-nothing
-lvCombine-comm f f-comm (plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂)
-    with lvCombine f plts lv₁ lv₂ | lvCombine f plts lv₂ lv₁ | lvCombine-comm f f-comm plts lv₁ lv₂ 
-...   | _ | _ | ≈-just lv₁lv₂≈lv₂lv₁ = ≈-just lv₁lv₂≈lv₂lv₁
-...   | _ | _ | ≈-nothing = ≈-nothing
 lvCombine-comm f f-comm (plt ∷ plts) (inj₁ v₁) (inj₂ lv₂) = ≈-nothing
 lvCombine-comm f f-comm (plt ∷ plts) (inj₂ lv₁) (inj₁ v₂) = ≈-nothing
 
+lvCombine-assoc : ∀ {a} (f : CombineForPLT a) →
+                  (∀ plt →  PartialAssoc (PartialLatticeType._≈_ plt) (f plt)) →
+                  ∀ (L : List (PartialLatticeType a)) →
+                  PartialAssoc (eqL L) (lvCombine f L)
+lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₁ v₁) (inj₁ v₂) (inj₁ v₃)
+    rewrite lvCombine-homo₁ plt plts f (((` v₁) ∨ (` v₂)) ∨ (` v₃))
+    rewrite lvCombine-homo₁ plt plts f ((` v₁) ∨ ((` v₂) ∨ (` v₃)))
+    = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (f-assoc plt v₁ v₂ v₃)
+lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₂ _) (inj₁ v₂) (inj₁ v₃)
+    with f plt v₂ v₃
+...   | just _ = ≈-nothing
+...   | nothing = ≈-nothing
+lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₁ _) (inj₂ _) (inj₁ _) = ≈-nothing
+lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂) (inj₁ _)
+    with lvCombine f plts lv₁ lv₂
+...   | just _ = ≈-nothing
+...   | nothing = ≈-nothing
+lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₁ v₁) (inj₁ v₂) (inj₂ _)
+    with f plt v₁ v₂
+...   | just _ = ≈-nothing
+...   | nothing = ≈-nothing
+lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₂ _) (inj₁ _) (inj₂ _) = ≈-nothing
+lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₁ _) (inj₂ lv₂) (inj₂ lv₃)
+    with lvCombine f plts lv₂ lv₃
+...   | just _ = ≈-nothing
+...   | nothing = ≈-nothing
+lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂) (inj₂ lv₃)
+    rewrite lvCombine-homo₂ plt plts f (((` lv₁) ∨ (` lv₂)) ∨ (` lv₃))
+    rewrite lvCombine-homo₂ plt plts f ((` lv₁) ∨ ((` lv₂) ∨ (` lv₃)))
+    = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (lvCombine-assoc f f-assoc plts lv₁ lv₂ lv₃)
+
 lvJoin-comm : ∀ {a} (L : List (PartialLatticeType a)) → PartialComm (eqL L) (lvJoin L)
 lvJoin-comm = lvCombine-comm PartialLatticeType._⊔?_ PartialLatticeType.⊔-comm
 
+lvJoin-assoc : ∀ {a} (L : List (PartialLatticeType a)) → PartialAssoc (eqL L) (lvJoin L)
+lvJoin-assoc = lvCombine-assoc PartialLatticeType._⊔?_ PartialLatticeType.⊔-assoc
+
 lvMeet-comm : ∀ {a} (L : List (PartialLatticeType a)) → PartialComm (eqL L) (lvMeet L)
 lvMeet-comm = lvCombine-comm PartialLatticeType._⊓?_ PartialLatticeType.⊓-comm
 
+lvMeet-assoc : ∀ {a} (L : List (PartialLatticeType a)) → PartialAssoc (eqL L) (lvMeet L)
+lvMeet-assoc = lvCombine-assoc PartialLatticeType._⊓?_ PartialLatticeType.⊓-assoc
+
 pathJoin'-comm : ∀ {a} {Ls : Layers a} → PartialComm (eqPath' Ls) (pathJoin' Ls)
 pathJoin'-comm {Ls = single l} lv₁ lv₂ = lvJoin-comm (toList l) lv₁ lv₂
 pathJoin'-comm {Ls = add-via-least l ls} (inj₁ lv₁) (inj₁ lv₂) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvJoin-comm (toList l) lv₁ lv₂)