Prove provenance for intersection

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

Map.agda

@@ -303,6 +303,13 @@ private module ImplInsert (f : B → B → B) where
     ...   | yes _ = refl
     ...   | no _ rewrite update-keys {k} {v} {xs} = refl
 
+    updates-keys : ∀ {l₁ l₂ : List (A × B)} →
+                   keys l₂ ≡ keys (updates l₁ l₂)
+    updates-keys {[]} = refl
+    updates-keys {(k , v) ∷ xs} {l₂}
+        rewrite updates-keys {xs} {l₂}
+        rewrite update-keys {k} {v} {updates xs l₂} = refl
+
     update-preserves-Unique : ∀ {k : A} {v : B} {l : List (A × B)} →
                               Unique (keys l) → Unique (keys (update k v l ))
     update-preserves-Unique {k} {v} {l} u rewrite update-keys {k} {v} {l} = u
@@ -332,6 +339,11 @@ private module ImplInsert (f : B → B → B) where
                                  Unique (keys l₂) → Unique (keys (intersect l₁ l₂))
     intersect-preserves-Unique {l₁} u = restrict-preserves-Unique (updates-preserve-Unique {l₁} u)
 
+    updates-preserve-∉₂ : ∀ {k : A} {l₁ l₂ : List (A × B)} →
+                          ¬ k ∈k l₂ → ¬ k ∈k updates l₁ l₂
+    updates-preserve-∉₂ {k} {l₁} {l₂} k∉kl₁ k∈kl₁l₂
+        rewrite updates-keys {l₁} {l₂} = k∉kl₁ k∈kl₁l₂
+
     restrict-needs-both : ∀ {k : A} {l₁ l₂ : List (A × B)} →
                           k ∈k restrict l₁ l₂ → (k ∈k l₁ × k ∈k l₂)
     restrict-needs-both {k} {l₁} {[]} ()
@@ -347,6 +359,36 @@ private module ImplInsert (f : B → B → B) where
             let (k∈kl₁ , k∈kxs) = restrict-needs-both k∈l₁xs
             in (k∈kl₁ , there k∈kxs)
 
+    restrict-preserves-∉₁ : ∀ {k : A} {l₁ l₂ : List (A × B)} →
+                            ¬ k ∈k l₁ → ¬ k ∈k restrict l₁ l₂
+    restrict-preserves-∉₁ {k} {l₁} {l₂} k∉kl₁ k∈kl₁l₂ =
+        let (k∈kl₁ , _) = restrict-needs-both {l₂ = l₂} k∈kl₁l₂ in k∉kl₁ k∈kl₁
+
+    restrict-preserves-∉₂ : ∀ {k : A} {l₁ l₂ : List (A × B)} →
+                            ¬ k ∈k l₂ → ¬ k ∈k restrict l₁ l₂
+    restrict-preserves-∉₂ {k} {l₁} {l₂} k∉kl₂ k∈kl₁l₂ =
+        let (_ , k∈kl₂) = restrict-needs-both {l₂ = l₂} k∈kl₁l₂ in k∉kl₂ k∈kl₂
+
+    intersect-preserves-∉₁ : ∀ {k : A} {l₁ l₂ : List (A × B)} →
+                             ¬ k ∈k l₁ → ¬ k ∈k intersect l₁ l₂
+    intersect-preserves-∉₁ {k} {l₁} {l₂} = restrict-preserves-∉₁ {k} {l₁} {updates l₁ l₂}
+
+    intersect-preserves-∉₂ : ∀ {k : A} {l₁ l₂ : List (A × B)} →
+                             ¬ k ∈k l₂ → ¬ k ∈k intersect l₁ l₂
+    intersect-preserves-∉₂ {k} {l₁} {l₂} k∉l₂ = restrict-preserves-∉₂ (updates-preserve-∉₂ {l₁ = l₁} k∉l₂ )
+
+    restrict-preserves-∈₂ : ∀ {k : A} {v : B} {l₁ l₂ : List (A × B)} →
+                            k ∈k l₁ → (k , v) ∈ l₂ → (k , v) ∈ restrict l₁ l₂
+    restrict-preserves-∈₂ {k} {v} {l₁} {(k' , v') ∷ xs} k∈kl₁ (here k,v≡k',v')
+        rewrite cong proj₁ k,v≡k',v' rewrite cong proj₂ k,v≡k',v'
+        with ∈k-dec k' l₁
+    ...   | yes _ = here refl
+    ...   | no k'∉kl₁ = absurd (k'∉kl₁ k∈kl₁)
+    restrict-preserves-∈₂ {l₁ = l₁} {l₂ = (k' , v') ∷ xs} k∈kl₁ (there k,v∈xs)
+        with ∈k-dec k' l₁
+    ...   | yes _ = there (restrict-preserves-∈₂ k∈kl₁ k,v∈xs)
+    ...   | no _ = restrict-preserves-∈₂ k∈kl₁ k,v∈xs
+
     update-preserves-∈ : ∀ {k k' : A} {v v' : B} {l : List (A × B)} →
                          ¬ k ≡ k' → (k , v) ∈ l → (k , v) ∈ update k' v' l
     update-preserves-∈ {k} {k'} {v} {v'} {(k'' , v'') ∷ xs} k≢k' (here k,v≡k'',v'')
@@ -433,6 +475,10 @@ module _ (fUnion : B → B → B) (fIntersect : B → B → B) where
     open ImplInsert fIntersect using
         ( restrict-needs-both
         ; updates
+        ; updates-combine
+        ; intersect-preserves-∉₁
+        ; intersect-preserves-∉₂
+        ; restrict-preserves-∈₂
         )
 
     ⟦_⟧ : Expr -> Map
@@ -445,6 +491,7 @@ module _ (fUnion : B → B → B) (fIntersect : B → B → B) where
         in₁ : ∀ {v : B} {e₁ e₂ : Expr} → Provenance k v e₁ → ¬ k ∈k ⟦ e₂ ⟧ → Provenance k v (e₁ ∪ e₂)
         in₂ : ∀ {v : B} {e₁ e₂ : Expr} → ¬ k ∈k ⟦ e₁ ⟧ → Provenance k v e₂ → Provenance k v (e₁ ∪ e₂)
         bothᵘ : ∀ {v₁ v₂ : B} {e₁ e₂ : Expr} → Provenance k v₁ e₁ → Provenance k v₂ e₂ → Provenance k (fUnion v₁ v₂) (e₁ ∪ e₂)
+        bothⁱ : ∀ {v₁ v₂ : B} {e₁ e₂ : Expr} → Provenance k v₁ e₁ → Provenance k v₂ e₂ → Provenance k (fIntersect v₁ v₂) (e₁ ∩ e₂)
 
     Expr-Provenance : ∀ (k : A) (e : Expr) → k ∈k ⟦ e ⟧ → Σ B (λ v → (Provenance k v e × (k , v) ∈ ⟦ e ⟧))
     Expr-Provenance k (` m) k∈km = let (v , k,v∈m) = locate k∈km in (v , (single k,v∈m , k,v∈m))
@@ -463,10 +510,13 @@ module _ (fUnion : B → B → B) (fIntersect : B → B → B) where
     ...   | no k∉ke₁ | no k∉ke₂  = absurd (union-preserves-∉ k∉ke₁ k∉ke₂ k∈ke₁e₂)
     Expr-Provenance k (e₁ ∩ e₂) k∈ke₁e₂
         with ∈k-dec k (proj₁ ⟦ e₁ ⟧) | ∈k-dec k (proj₁ ⟦ e₂ ⟧)
-    ...   | yes k∈ke₁ | yes k∈ke₂ = {!!}
+    ...   | yes k∈ke₁ | yes k∈ke₂ =
-    ...   | yes k∈ke₁ | no k∉ke₂ = {!!}
+            let (v₁ , (g₁ , k,v₁∈e₁)) = Expr-Provenance k e₁ k∈ke₁
-    ...   | no k∉ke₁ | yes k∈ke₂ = {!!}
+                (v₂ , (g₂ , k,v₂∈e₂)) = Expr-Provenance k e₂ k∈ke₂
-    ...   | no k∉ke₁ | no k∉ke₂ = {!!}
+            in (fIntersect v₁ v₂ , (bothⁱ g₁ g₂ , restrict-preserves-∈₂ k∈ke₁ (updates-combine (proj₂ ⟦ e₁ ⟧) (proj₂ ⟦ e₂ ⟧) k,v₁∈e₁ k,v₂∈e₂)))
+    ...   | yes k∈ke₁ | no k∉ke₂ = absurd (intersect-preserves-∉₂ {l₁ = proj₁ ⟦ e₁ ⟧} k∉ke₂ k∈ke₁e₂)
+    ...   | no k∉ke₁ | yes k∈ke₂ = absurd (intersect-preserves-∉₁ {l₂ = proj₁ ⟦ e₂ ⟧} k∉ke₁ k∈ke₁e₂)
+    ...   | no k∉ke₁ | no k∉ke₂ = absurd (intersect-preserves-∉₂ {l₁ = proj₁ ⟦ e₁ ⟧} k∉ke₂ k∈ke₁e₂)
 
 
 module _ (_≈_ : B → B → Set b) where