Add most of the proof of from distributivity.

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

Lattice/FiniteValueMap.agda

@@ -25,7 +25,7 @@ open import Data.List.Relation.Unary.All using (All)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Relation.Nullary using (¬_)
 
-open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≈-dec-A lB using (subset-impl; locate; forget; _∈_; Map-functional)
+open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≈-dec-A lB using (subset-impl; locate; forget; _∈_; Map-functional; Expr-Provenance; _∩_; _∪_; `_; in₁; in₂; bothᵘ; single)
 open import Lattice.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≈-dec-A lB public
 
 module IterProdIsomorphism where
@@ -57,12 +57,18 @@ module IterProdIsomorphism where
         _≈ᵐ_ : ∀ {ks : List A} → FiniteMap ks → FiniteMap ks → Set
         _≈ᵐ_ {ks} = _≈_ ks
 
+        _⊔ᵐ_ : ∀ {ks : List A} → FiniteMap ks → FiniteMap ks → FiniteMap ks
+        _⊔ᵐ_ {ks} = _⊔_ ks
+
         _⊆ᵐ_ : ∀ {ks₁ ks₂ : List A} → FiniteMap ks₁ → FiniteMap ks₂ → Set
         _⊆ᵐ_ fm₁ fm₂ = subset-impl (proj₁ (proj₁ fm₁)) (proj₁ (proj₁ fm₂))
 
         _≈ⁱᵖ_ : ∀ {ks : List A} → IterProd (length ks) → IterProd (length ks) → Set
         _≈ⁱᵖ_ {ks} = IP._≈_ (length ks)
 
+        _⊔ⁱᵖ_ : ∀ {ks : List A} → IterProd (length ks) → IterProd (length ks) → IterProd (length ks)
+        _⊔ⁱᵖ_ {ks} = IP._⊔_ (length ks)
+
     from-to-inverseˡ : ∀ {ks : List A} (uks : Unique ks) →
                       Inverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {ks}) (from {ks}) (to {ks} uks) -- from (to x) = x
     from-to-inverseˡ {[]} _ _ = IsEquivalence.≈-refl (IP.≈-equiv 0)
@@ -102,9 +108,13 @@ module IterProdIsomorphism where
         first-key-in-map : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → Σ B (λ v → (k , v) ∈ proj₁ fm)
         first-key-in-map (((k , v) ∷ _ , _) , refl) = (v , here refl)
 
-        from-first-value : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → proj₁ (from fm) ≈₂ proj₁ (first-key-in-map fm)
+        from-first-value : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → proj₁ (from fm) ≡ proj₁ (first-key-in-map fm)
-        from-first-value {k} {ks} (((k , v) ∷ _ , push _ _) , refl) = IsLattice.≈-refl lB
+        from-first-value {k} {ks} (((k , v) ∷ _ , push _ _) , refl) = refl
 
+        -- We need pop because reasoning about two distinct 'refl' pattern
+        -- matches is giving us unification errors. So, stash the 'refl' pattern
+        -- matching into a helper functions, and write solutions in terms
+        -- of that.
         pop : ∀ {k : A} {ks : List A} → FiniteMap (k ∷ ks) → FiniteMap ks
         pop (((_ ∷ kvs') , push _ ukvs') , refl) = ((kvs' , ukvs') , refl)
 
@@ -123,6 +133,9 @@ module IterProdIsomorphism where
                 narrow : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} → fm₁ ⊆ᵐ fm₂  → pop fm₁ ⊆ᵐ pop fm₂
                 narrow {fm₁} {fm₂} x = narrow₂ {pop fm₁} (narrow₁ {fm₂ = fm₂} x)
 
+        pop-⊔-distr : ∀ {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ∷ ks)) → pop (fm₁ ⊔ᵐ fm₂) ≈ᵐ (pop fm₁ ⊔ᵐ pop fm₂)
+        pop-⊔-distr = {!!} -- pop (fm₁ ⊔ fm₂) ⊆ pop fm₁ ⊔ pop fm₂ etc.
+
         from-rest : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → proj₂ (from fm) ≡ from (pop fm)
         from-rest (((_ ∷ kvs') , push _ ukvs') , refl) = refl
 
@@ -130,9 +143,46 @@ module IterProdIsomorphism where
     from-preserves-≈ {[]} (([] , _) , _) (([] , _) , _) _ = IsEquivalence.≈-refl ≈ᵘ-equiv
     from-preserves-≈ {k ∷ ks'} fm₁@(m₁ , _) fm₂@(m₂ , _) fm₁≈fm₂@(kvs₁⊆kvs₂ , kvs₂⊆kvs₁)
         with first-key-in-map fm₁ | first-key-in-map fm₂ | from-first-value fm₁ | from-first-value fm₂
-    ...   | (v₁ , k,v₁∈fm₁) | (v₂ , k,v₂∈fm₂) | fv₁≈v₁ | fv₂≈v₂
+    ...   | (v₁ , k,v₁∈fm₁) | (v₂ , k,v₂∈fm₂) | refl | refl
             with kvs₁⊆kvs₂ _ _ k,v₁∈fm₁
     ...       | (v₁' , (v₁≈v₁' , k,v₁'∈fm₂))
                 rewrite Map-functional {m = m₂} k,v₂∈fm₂ k,v₁'∈fm₂
                 rewrite from-rest fm₁ rewrite from-rest fm₂
-                = (≈₂-trans fv₁≈v₁ (≈₂-trans v₁≈v₁' (≈₂-sym fv₂≈v₂)) , from-preserves-≈ (pop fm₁) (pop fm₂) (pop-≈ fm₁ fm₂ fm₁≈fm₂))
+                = (v₁≈v₁' , from-preserves-≈ (pop fm₁) (pop fm₂) (pop-≈ fm₁ fm₂ fm₁≈fm₂))
+
+    to-preserves-≈ : ∀ {ks : List A} (uks : Unique ks) (ip₁ ip₂ : IterProd (length ks)) → _≈ⁱᵖ_ {ks} ip₁ ip₂ → to uks ip₁ ≈ᵐ to uks ip₂
+    to-preserves-≈ {[]} empty tt tt _ = ((λ k v ()), (λ k v ()))
+    to-preserves-≈ {k ∷ ks'} uks@(push k≢ks' uks') ip₁@(v₁ , rest₁) ip₂@(v₂ , rest₂) (v₁≈v₂ , rest₁≈rest₂) = (fm₁⊆fm₂ , fm₂⊆fm₁)
+        where
+            fm₁⊆fm₂ : to uks ip₁ ⊆ᵐ to uks ip₂
+            fm₁⊆fm₂ k v k,v∈kvs₁
+                with ((kvs'₁ , ukvs'₁) , kvs'₁≡ks') ← to uks' rest₁ in p₁
+                with ((kvs'₂ , ukvs'₂) , kvs'₂≡ks') ← to uks' rest₂ in p₂
+                with k,v∈kvs₁
+            ...   | here refl = (v₂ , (v₁≈v₂ , here refl))
+            ...   | there k,v∈kvs'₁ with refl ← p₁ with refl ← p₂ = let (v' , (v≈v' , k,v'∈kvs₁)) = proj₁ (to-preserves-≈ uks' rest₁ rest₂ rest₁≈rest₂) k v k,v∈kvs'₁ in (v' , (v≈v' , there k,v'∈kvs₁))
+
+            fm₂⊆fm₁ : to uks ip₂ ⊆ᵐ to uks ip₁
+            fm₂⊆fm₁ k v k,v∈kvs₂
+                with ((kvs'₁ , ukvs'₁) , kvs'₁≡ks') ← to uks' rest₁ in p₁
+                with ((kvs'₂ , ukvs'₂) , kvs'₂≡ks') ← to uks' rest₂ in p₂
+                with k,v∈kvs₂
+            ...   | here refl = (v₁ , (IsLattice.≈-sym lB v₁≈v₂ , here refl))
+            ...   | there k,v∈kvs'₂ with refl ← p₁ with refl ← p₂ = let (v' , (v≈v' , k,v'∈kvs₂)) = proj₂ (to-preserves-≈ uks' rest₁ rest₂ rest₁≈rest₂) k v k,v∈kvs'₂ in (v' , (v≈v' , there k,v'∈kvs₂))
+
+    from-⊔-distr : ∀ {ks : List A} → (fm₁ fm₂ : FiniteMap ks) → _≈ⁱᵖ_ {ks} (from (fm₁ ⊔ᵐ fm₂)) (_⊔ⁱᵖ_ {ks} (from fm₁) (from fm₂))
+    from-⊔-distr {[]} fm₁ fm₂ = IsEquivalence.≈-refl ≈ᵘ-equiv
+    from-⊔-distr {k ∷ ks} fm₁@(m₁ , _) fm₂@(m₂ , _)
+        with first-key-in-map (fm₁ ⊔ᵐ fm₂) | first-key-in-map fm₁ | first-key-in-map fm₂ | from-first-value (fm₁ ⊔ᵐ fm₂) | from-first-value fm₁ | from-first-value fm₂
+    ...   | (v , k,v∈fm₁fm₂) | (v₁ , k,v₁∈fm₁) | (v₂ , k,v₂∈fm₂) | refl | refl | refl
+            with Expr-Provenance k ((` m₁) ∪ (` m₂)) (forget {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂)
+    ...       | (_ , (in₁ _ k∉km₂ , _)) = ⊥-elim (k∉km₂ (forget {m = m₂} k,v₂∈fm₂))
+    ...       | (_ , (in₂ k∉km₁ _ , _)) = ⊥-elim (k∉km₁ (forget {m = m₁} k,v₁∈fm₁))
+    ...       | (v₁⊔v₂ , (bothᵘ {v₁'} {v₂'} (single k,v₁'∈m₁) (single k,v₂'∈m₂) , k,v₁⊔v₂∈m₁m₂))
+                rewrite Map-functional {m = m₁} k,v₁∈fm₁ k,v₁'∈m₁
+                rewrite Map-functional {m = m₂} k,v₂∈fm₂ k,v₂'∈m₂
+                rewrite Map-functional {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂ k,v₁⊔v₂∈m₁m₂
+                rewrite from-rest (fm₁ ⊔ᵐ fm₂) rewrite from-rest fm₁ rewrite from-rest fm₂
+                = ( IsLattice.≈-refl lB
+                  , IsEquivalence.≈-trans (IP.≈-equiv (length ks)) (from-preserves-≈ (pop (fm₁ ⊔ᵐ fm₂)) (pop fm₁ ⊔ᵐ pop fm₂) (pop-⊔-distr fm₁ fm₂)) ((from-⊔-distr (pop fm₁) (pop fm₂)))
+                  )