Prove that 'first' presrves equality

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

Lattice/FiniteValueMap.agda

@@ -16,20 +16,23 @@ module Lattice.FiniteValueMap (A : Set) (B : Set)
     (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
 
 open import Data.List using (List; length; []; _∷_)
-open import Utils using (Unique; push; empty)
+open import Data.Product using (Σ; proj₁; proj₂; _×_)
+open import Data.Empty using (⊥-elim)
+open import Utils using (Unique; push; empty; All¬-¬Any)
 open import Data.Product using (_,_)
 open import Data.List.Properties using (∷-injectiveʳ)
 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)
+open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≈-dec-A lB using (subset-impl; locate; forget; _∈_; Map-functional)
 open import Lattice.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≈-dec-A lB public
 
 module IterProdIsomorphism where
     open import Data.Unit using (⊤; tt)
-    open import Lattice.Unit using () renaming (_≈_ to _≈ᵘ_; _⊔_ to _⊔ᵘ_; _⊓_ to _⊓ᵘ_; ≈-dec to ≈ᵘ-dec; isLattice to isLatticeᵘ)
+    open import Lattice.Unit using () renaming (_≈_ to _≈ᵘ_; _⊔_ to _⊔ᵘ_; _⊓_ to _⊓ᵘ_; ≈-dec to ≈ᵘ-dec; isLattice to isLatticeᵘ; ≈-equiv to ≈ᵘ-equiv)
     open import Lattice.IterProd _≈₂_ _≈ᵘ_ _⊔₂_ _⊔ᵘ_ _⊓₂_ _⊓ᵘ_ lB isLatticeᵘ as IP using (IterProd)
+    open IsLattice lB using () renaming (≈-trans to ≈₂-trans; ≈-sym to ≈₂-sym)
 
     from : ∀ {ks : List A} → FiniteMap ks → IterProd (length ks)
     from {[]} (([] , _) , _) = tt
@@ -54,6 +57,9 @@ module IterProdIsomorphism where
         _≈ᵐ_ : ∀ {ks : List A} → FiniteMap ks → FiniteMap ks → Set
         _≈ᵐ_ {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)
 
@@ -91,3 +97,42 @@ module IterProdIsomorphism where
                     m₂⊆m₁ k' v' (there k',v'∈kvs'₂) =
                         let (v'' , (v'≈v'' , k',v''∈kvs'₁)) = kvs'₂⊆kvs'₁ k' v' k',v'∈kvs'₂
                         in (v'' , (v'≈v'' , there k',v''∈kvs'₁))
+
+    private
+        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} {ks} (((k , v) ∷ _ , push _ _) , refl) = IsLattice.≈-refl lB
+
+        pop : ∀ {k : A} {ks : List A} → FiniteMap (k ∷ ks) → FiniteMap ks
+        pop (((_ ∷ kvs') , push _ ukvs') , refl) = ((kvs' , ukvs') , refl)
+
+        pop-≈ :  ∀ {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ∷ ks)) → fm₁ ≈ᵐ fm₂ → pop fm₁ ≈ᵐ pop fm₂
+        pop-≈ {k} {ks} fm₁ fm₂ (fm₁⊆fm₂ , fm₂⊆fm₁) = (narrow fm₁⊆fm₂ , narrow fm₂⊆fm₁)
+            where
+                narrow₁ : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} → fm₁ ⊆ᵐ fm₂  → pop fm₁ ⊆ᵐ fm₂
+                narrow₁ {(_ ∷ _ , push _ _) , refl} kvs₁⊆kvs₂ k' v' k',v'∈kvs'₁ = kvs₁⊆kvs₂ k' v' (there k',v'∈kvs'₁)
+
+                narrow₂ : ∀ {fm₁ : FiniteMap ks} {fm₂ : FiniteMap (k ∷ ks)} → fm₁ ⊆ᵐ fm₂  → fm₁ ⊆ᵐ pop fm₂
+                narrow₂ {fm₁} {fm₂ = (_ ∷ kvs'₂ , push k≢ks _) , kvs≡ks@refl} kvs₁⊆kvs₂ k' v' k',v'∈kvs'₁
+                    with kvs₁⊆kvs₂ k' v' k',v'∈kvs'₁
+                ...   | (v'' , (v'≈v'' , here refl)) rewrite sym (proj₂ fm₁) = ⊥-elim (All¬-¬Any k≢ks (forget {m = proj₁ fm₁} k',v'∈kvs'₁))
+                ...   | (v'' , (v'≈v'' , there k',v'∈kvs'₂)) = (v'' , (v'≈v'' , k',v'∈kvs'₂))
+
+                narrow : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} → fm₁ ⊆ᵐ fm₂  → pop fm₁ ⊆ᵐ pop fm₂
+                narrow {fm₁} {fm₂} x = narrow₂ {pop fm₁} (narrow₁ {fm₂ = fm₂} x)
+
+        from-rest : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → proj₂ (from fm) ≡ from (pop fm)
+        from-rest (((_ ∷ kvs') , push _ ukvs') , refl) = refl
+
+    from-preserves-≈ : ∀ {ks : List A} → (fm₁ fm₂ : FiniteMap ks) → fm₁ ≈ᵐ fm₂ → (_≈ⁱᵖ_ {ks}) (from fm₁) (from fm₂)
+    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₂
+            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₂))

Lattice/Map.agda

@@ -73,9 +73,9 @@ private module _ where
     ∈-cong f (here c≡c') = here (cong f c≡c')
     ∈-cong f (there c∈xs) = there (∈-cong f c∈xs)
 
-    locate : ∀ {k : A} {l : List (A × B)} → k ∈ keys l → Σ B (λ v → (k , v) ∈ l)
-    locate {k} {(k' , v) ∷ xs} (here k≡k') rewrite k≡k' = (v , here refl)
-    locate {k} {(k' , v) ∷ xs} (there k∈kxs) = let (v , k,v∈xs) = locate k∈kxs in (v , there k,v∈xs)
+    locate-impl : ∀ {k : A} {l : List (A × B)} → k ∈ keys l → Σ B (λ v → (k , v) ∈ l)
+    locate-impl {k} {(k' , v) ∷ xs} (here k≡k') rewrite k≡k' = (v , here refl)
+    locate-impl {k} {(k' , v) ∷ xs} (there k∈kxs) = let (v , k,v∈xs) = locate-impl k∈kxs in (v , there k,v∈xs)
 
 private module ImplRelation where
     open MemProp using (_∈_)
@@ -476,6 +476,12 @@ _∈_ p (kvs , _) = MemProp._∈_ p kvs
 _∈k_ : A → Map → Set a
 _∈k_ k m = MemProp._∈_ k (keys m)
 
+locate : ∀ {k : A} {m : Map} → k ∈k m → Σ B (λ v → (k , v) ∈ m)
+locate k∈km = locate-impl k∈km
+
+forget : ∀ {k : A} {v : B} {m : Map} → (k , v) ∈ m → k ∈k m
+forget = ∈-cong proj₁
+
 Map-functional : ∀ {k : A} {v v' : B} {m : Map} → (k , v) ∈ m → (k , v') ∈ m → v ≡ v'
 Map-functional {m = (l , ul)} k,v∈m k,v'∈m = ListAB-functional ul k,v∈m k,v'∈m
 
@@ -549,7 +555,7 @@ data Provenance (k : A) : B → Expr → Set (a ⊔ℓ b) where
     bothⁱ : ∀ {v₁ v₂ : B} {e₁ e₂ : Expr} → Provenance k v₁ e₁ → Provenance k v₂ e₂ → Provenance k (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))
+Expr-Provenance k (` m) k∈km = let (v , k,v∈m) = locate-impl k∈km in (v , (single k,v∈m , k,v∈m))
 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₂ =
@@ -582,7 +588,7 @@ module _ (≈₂-dec : ∀ (b₁ b₂ : B) → Dec (b₁ ≈₂ b₂)) where
 
         SubsetInfo-to-dec : ∀ {m₁ m₂ : Map} → SubsetInfo m₁ m₂ → Dec (m₁ ⊆ m₂)
         SubsetInfo-to-dec (extra k k∈km₁ k∉km₂) =
-            let (v , k,v∈m₁) = locate k∈km₁
+            let (v , k,v∈m₁) = locate-impl k∈km₁
             in no (λ m₁⊆m₂ →
                    let (v' , (_ , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁
                    in k∉km₂ (∈-cong proj₁ k,v'∈m₂))
@@ -601,7 +607,7 @@ module _ (≈₂-dec : ∀ (b₁ b₂ : B) → Dec (b₁ ≈₂ b₂)) where
                 mismatch k' v₁ v₂ (there k',v₁∈xs₁) k',v₂∈m₂ v₁̷≈v₂
         ...   | fine xs₁⊆m₂ with ∈k-dec k l₂
         ...       | no k∉km₂ = extra k (here refl) k∉km₂
-        ...       | yes k∈km₂ with locate k∈km₂
+        ...       | yes k∈km₂ with locate-impl k∈km₂
         ...           | (v' , k,v'∈m₂) with ≈₂-dec v v'
         ...               | no v̷≈v' = mismatch k v v' (here refl) (k,v'∈m₂) v̷≈v'
         ...               | yes v≈v' = fine m₁⊆m₂
@@ -635,7 +641,7 @@ private module I⊓ = ImplInsert _⊓₂_
     where
         ≈-∉-cong : ∀ {m₁ m₂ : Map} {k : A} → m₁ ≈ m₂ → ¬ k ∈k m₁ → ¬ k ∈k m₂
         ≈-∉-cong (m₁⊆m₂ , m₂⊆m₁) k∉km₁ k∈km₂ =
-            let (v₂ , k,v₂∈m₂) = locate k∈km₂
+            let (v₂ , k,v₂∈m₂) = locate-impl k∈km₂
                 (_ , (_ , k,v₁∈m₁)) = m₂⊆m₁ _ v₂ k,v₂∈m₂
             in k∉km₁ (∈-cong proj₁ k,v₁∈m₁)
 
@@ -825,7 +831,7 @@ absorb-⊓-⊔ m₁@(l₁ , u₁) m₂@(l₂ , u₂) = (absorb-⊓-⊔¹ , absor
         absorb-⊓-⊔² k v k,v∈m₁
             with ∈k-dec k l₂
         ...   | yes k∈km₂ =
-                let (v₂ , k,v₂∈m₂) = locate k∈km₂
+                let (v₂ , k,v₂∈m₂) = locate-impl k∈km₂
                 in (v ⊓₂ (v ⊔₂ v₂) , (≈₂-sym (absorb-⊓₂-⊔₂ v v₂) , I⊓.intersect-combines u₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) k,v∈m₁ (I⊔.union-combines u₁ u₂ k,v∈m₁ k,v₂∈m₂)))
         ...   | no k∉km₂ = (v ⊓₂ v , (≈₂-sym (⊓₂-idemp v) , I⊓.intersect-combines u₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) k,v∈m₁ (I⊔.union-preserves-∈₁ u₁ k,v∈m₁ k∉km₂)))
 
@@ -852,7 +858,7 @@ absorb-⊔-⊓ m₁@(l₁ , u₁) m₂@(l₂ , u₂) = (absorb-⊔-⊓¹ , absor
         absorb-⊔-⊓² k v k,v∈m₁
             with ∈k-dec k l₂
         ...   | yes k∈km₂ =
-                let (v₂ , k,v₂∈m₂) = locate k∈km₂
+                let (v₂ , k,v₂∈m₂) = locate-impl k∈km₂
                 in (v ⊔₂ (v ⊓₂ v₂) , (≈₂-sym (absorb-⊔₂-⊓₂ v v₂) , I⊔.union-combines u₁ (I⊓.intersect-preserves-Unique {l₁} {l₂} u₂) k,v∈m₁ (I⊓.intersect-combines u₁ u₂ k,v∈m₁ k,v₂∈m₂)))
         ...   | no k∉km₂ = (v , (≈₂-refl , I⊔.union-preserves-∈₁ u₁ k,v∈m₁ (I⊓.intersect-preserves-∉₂ {k} {l₁} {l₂} k∉km₂)))