From f00dabfc930fc4f7ec3552383ce8ac0c81e3e673 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 2 Mar 2024 16:15:20 -0800 Subject: [PATCH] More cleanup to FiniteValueMap Signed-off-by: Danila Fedorin --- Lattice/FiniteValueMap.agda | 66 +++++++++++++++++++++++++++---------- 1 file changed, 49 insertions(+), 17 deletions(-) diff --git a/Lattice/FiniteValueMap.agda b/Lattice/FiniteValueMap.agda index cffc277..32bda52 100644 --- a/Lattice/FiniteValueMap.agda +++ b/Lattice/FiniteValueMap.agda @@ -312,25 +312,39 @@ module IterProdIsomorphism where fm₂⊆fm₁ = inductive-step (≈₂-sym v₁≈v₂) (IP.≈-sym (length ks') rest₁≈rest₂) - from-⊔-distr : ∀ {ks : List A} → (fm₁ fm₂ : FiniteMap ks) → _≈ⁱᵖ_ {length ks} (from (fm₁ ⊔ᵐ fm₂)) (_⊔ⁱᵖ_ {ks} (from fm₁) (from fm₂)) + from-⊔-distr : ∀ {ks : List A} → (fm₁ fm₂ : FiniteMap ks) → + _≈ⁱᵖ_ {length 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₂ + 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₁)) + ... | (_ , (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₂))) + , 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₂))) ) - to-⊔-distr : ∀ {ks : List A} (uks : Unique ks) → (ip₁ ip₂ : IterProd (length ks)) → to uks (_⊔ⁱᵖ_ {ks} ip₁ ip₂) ≈ᵐ (to uks ip₁ ⊔ᵐ to uks ip₂) + to-⊔-distr : ∀ {ks : List A} (uks : Unique ks) → (ip₁ ip₂ : IterProd (length ks)) → + to uks (_⊔ⁱᵖ_ {ks} ip₁ ip₂) ≈ᵐ (to uks ip₁ ⊔ᵐ to uks ip₂) to-⊔-distr {[]} empty tt tt = ((λ k v ()), (λ k v ())) to-⊔-distr {ks@(k ∷ ks')} uks@(push k≢ks' uks') ip₁@(v₁ , rest₁) ip₂@(v₂ , rest₂) = (fm⊆fm₁fm₂ , fm₁fm₂⊆fm) where @@ -344,27 +358,45 @@ module IterProdIsomorphism where fm⊆fm₁fm₂ k v (here refl) = (v₁ ⊔₂ v₂ , (IsLattice.≈-refl lB - , ⊔-combines {k} {v₁} {v₂} {proj₁ fm₁} {proj₁ fm₂} (here refl) (here refl) + , ⊔-combines {k} {v₁} {v₂} {proj₁ fm₁} {proj₁ fm₂} + (here refl) (here refl) ) ) fm⊆fm₁fm₂ k' v (there k',v∈fm') with (fm'⊆fm'₁fm'₂ , _) ← to-⊔-distr uks' rest₁ rest₂ - with (v' , (v₁⊔v₂≈v' , k',v'∈fm'₁fm'₂)) ← fm'⊆fm'₁fm'₂ k' v k',v∈fm' - with (_ , (refl , (v₁∈fm'₁ , v₂∈fm'₂))) ← Provenance-union fm₁' fm₂' k',v'∈fm'₁fm'₂ = - (v' , (v₁⊔v₂≈v' , ⊔-combines {m₁ = proj₁ fm₁} {m₂ = proj₁ fm₂} (there v₁∈fm'₁) (there v₂∈fm'₂))) + with (v' , (v₁⊔v₂≈v' , k',v'∈fm'₁fm'₂)) + ← fm'⊆fm'₁fm'₂ k' v k',v∈fm' + with (_ , (refl , (v₁∈fm'₁ , v₂∈fm'₂))) + ← Provenance-union fm₁' fm₂' k',v'∈fm'₁fm'₂ = + ( v' + , ( v₁⊔v₂≈v' + , ⊔-combines {m₁ = proj₁ fm₁} {m₂ = proj₁ fm₂} + (there v₁∈fm'₁) (there v₂∈fm'₂) + ) + ) fm₁fm₂⊆fm : (fm₁ ⊔ᵐ fm₂) ⊆ᵐ fm fm₁fm₂⊆fm k' v k',v∈fm₁fm₂ - with (_ , fm'₁fm'₂⊆fm') ← to-⊔-distr uks' rest₁ rest₂ - with (_ , (refl , (v₁∈fm₁ , v₂∈fm₂))) ← Provenance-union fm₁ fm₂ k',v∈fm₁fm₂ + with (_ , fm'₁fm'₂⊆fm') + ← to-⊔-distr uks' rest₁ rest₂ + with (_ , (refl , (v₁∈fm₁ , v₂∈fm₂))) + ← Provenance-union fm₁ fm₂ k',v∈fm₁fm₂ with v₁∈fm₁ | v₂∈fm₂ - ... | here refl | here refl = (v , (IsLattice.≈-refl lB , here refl)) - ... | here refl | there k',v₂∈fm₂' = ⊥-elim (All¬-¬Any k≢ks' (subst (λ list → k' ∈ˡ list) (proj₂ fm₂') (forget {m = proj₁ fm₂'} k',v₂∈fm₂'))) - ... | there k',v₁∈fm₁' | here refl = ⊥-elim (All¬-¬Any k≢ks' (subst (λ list → k' ∈ˡ list) (proj₂ fm₁') (forget {m = proj₁ fm₁'} k',v₁∈fm₁'))) + ... | here refl | here refl = + (v , (IsLattice.≈-refl lB , here refl)) + ... | here refl | there k',v₂∈fm₂' = + ⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₂') + (forget {m = proj₁ fm₂'} k',v₂∈fm₂'))) + ... | there k',v₁∈fm₁' | here refl = + ⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₁') + (forget {m = proj₁ fm₁'} k',v₁∈fm₁'))) ... | there k',v₁∈fm₁' | there k',v₂∈fm₂' = let - k',v₁v₂∈fm₁'fm₂' = ⊔-combines {m₁ = proj₁ fm₁'} {m₂ = proj₁ fm₂'} k',v₁∈fm₁' k',v₂∈fm₂' - (v' , (v₁⊔v₂≈v' , v'∈fm')) = fm'₁fm'₂⊆fm' _ _ k',v₁v₂∈fm₁'fm₂' + k',v₁v₂∈fm₁'fm₂' = + ⊔-combines {m₁ = proj₁ fm₁'} {m₂ = proj₁ fm₂'} + k',v₁∈fm₁' k',v₂∈fm₂' + (v' , (v₁⊔v₂≈v' , v'∈fm')) = + fm'₁fm'₂⊆fm' _ _ k',v₁v₂∈fm₁'fm₂' in (v' , (v₁⊔v₂≈v' , there v'∈fm'))