diff --git a/Lattice/FiniteValueMap.agda b/Lattice/FiniteValueMap.agda index 1e5dfaf..cffc277 100644 --- a/Lattice/FiniteValueMap.agda +++ b/Lattice/FiniteValueMap.agda @@ -93,17 +93,20 @@ module IterProdIsomorphism where _⊆ᵐ_ : ∀ {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) + _≈ⁱᵖ_ : ∀ {n : ℕ} → IterProd n → IterProd n → Set + _≈ⁱᵖ_ {n} = IP._≈_ n - _⊔ⁱᵖ_ : ∀ {ks : List A} → IterProd (length ks) → IterProd (length ks) → IterProd (length ks) + _⊔ⁱᵖ_ : ∀ {ks : List A} → + IterProd (length ks) → IterProd (length ks) → IterProd (length ks) _⊔ⁱᵖ_ {ks} = IP._⊔_ (length ks) _∈ᵐ_ : ∀ {ks : List A} → A × B → FiniteMap ks → Set _∈ᵐ_ {ks} k,v fm = k,v ∈ proj₁ fm + -- The left inverse is: from (to x) = x from-to-inverseˡ : ∀ {ks : List A} (uks : Unique ks) → - Inverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {ks}) (from {ks}) (to {ks} uks) -- from (to x) = x + Inverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks}) + (from {ks}) (to {ks} uks) from-to-inverseˡ {[]} _ _ = IsEquivalence.≈-refl (IP.≈-equiv 0) from-to-inverseˡ {k ∷ ks'} (push k≢ks' uks') (v , rest) with ((fm' , ufm') , refl) ← to uks' rest in p rewrite sym p = @@ -115,33 +118,47 @@ module IterProdIsomorphism where -- The map has its own uniqueness proof, but the call to 'to' needs a standalone -- uniqueness proof too. Work with both proofs as needed to thread things through. + -- + -- The right inverse is: to (from x) = x from-to-inverseʳ : ∀ {ks : List A} (uks : Unique ks) → - Inverseʳ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {ks}) (from {ks}) (to {ks} uks) -- to (from x) = x - from-to-inverseʳ {[]} _ (([] , empty) , kvs≡ks) rewrite kvs≡ks = ((λ k v ()) , (λ k v ())) - from-to-inverseʳ {k ∷ ks'} uks@(push k≢ks'₁ uks'₁) fm₁@(m₁@((k , v) ∷ fm'₁ , push k≢ks'₂ uks'₂) , refl) - with to uks'₁ (from ((fm'₁ , uks'₂) , refl)) | from-to-inverseʳ {ks'} uks'₁ ((fm'₁ , uks'₂) , refl) - ... | ((fm'₂ , ufm'₂) , _) | (fm'₂⊆fm'₁ , fm'₁⊆fm'₂) = (m₂⊆m₁ , m₁⊆m₂) + Inverseʳ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks}) + (from {ks}) (to {ks} uks) + from-to-inverseʳ {[]} _ (([] , empty) , kvs≡ks) rewrite kvs≡ks = + ( (λ k v ()) + , (λ k v ()) + ) + from-to-inverseʳ {k ∷ ks'} uks@(push _ uks'₁) fm₁@(((k , v) ∷ fm'₁ , push _ uks'₂) , refl) + with to uks'₁ (from ((fm'₁ , uks'₂) , refl)) + | from-to-inverseʳ {ks'} uks'₁ ((fm'₁ , uks'₂) , refl) + ... | ((fm'₂ , ufm'₂) , _) + | (fm'₂⊆fm'₁ , fm'₁⊆fm'₂) = (m₂⊆m₁ , m₁⊆m₂) where kvs₁ = (k , v) ∷ fm'₁ kvs₂ = (k , v) ∷ fm'₂ m₁⊆m₂ : subset-impl kvs₁ kvs₂ - m₁⊆m₂ k' v' (here refl) = (v' , (IsLattice.≈-refl lB , here refl)) + m₁⊆m₂ k' v' (here refl) = + (v' , (IsLattice.≈-refl lB , here refl)) m₁⊆m₂ k' v' (there k',v'∈fm'₁) = - let (v'' , (v'≈v'' , k',v''∈fm'₂)) = fm'₁⊆fm'₂ k' v' k',v'∈fm'₁ + let (v'' , (v'≈v'' , k',v''∈fm'₂)) = + fm'₁⊆fm'₂ k' v' k',v'∈fm'₁ in (v'' , (v'≈v'' , there k',v''∈fm'₂)) m₂⊆m₁ : subset-impl kvs₂ kvs₁ - m₂⊆m₁ k' v' (here refl) = (v' , (IsLattice.≈-refl lB , here refl)) + m₂⊆m₁ k' v' (here refl) = + (v' , (IsLattice.≈-refl lB , here refl)) m₂⊆m₁ k' v' (there k',v'∈fm'₂) = - let (v'' , (v'≈v'' , k',v''∈fm'₁)) = fm'₂⊆fm'₁ k' v' k',v'∈fm'₂ + let (v'' , (v'≈v'' , k',v''∈fm'₁)) = + fm'₂⊆fm'₁ k' v' k',v'∈fm'₂ in (v'' , (v'≈v'' , there k',v''∈fm'₁)) 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 : 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) = refl -- We need pop because reasoning about two distinct 'refl' pattern @@ -151,91 +168,151 @@ module IterProdIsomorphism where pop : ∀ {k : A} {ks : List A} → FiniteMap (k ∷ ks) → FiniteMap ks pop (((_ ∷ fm') , push _ ufm') , refl) = ((fm' , ufm') , 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₁) + 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'∈fm'₁ = kvs₁⊆kvs₂ k' v' (there k',v'∈fm'₁) + narrow₁ : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} → + fm₁ ⊆ᵐ fm₂ → pop fm₁ ⊆ᵐ fm₂ + narrow₁ {(_ ∷ _ , push _ _) , refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁ = + kvs₁⊆kvs₂ k' v' (there k',v'∈fm'₁) - narrow₂ : ∀ {fm₁ : FiniteMap ks} {fm₂ : FiniteMap (k ∷ ks)} → fm₁ ⊆ᵐ fm₂ → fm₁ ⊆ᵐ pop fm₂ + narrow₂ : ∀ {fm₁ : FiniteMap ks} {fm₂ : FiniteMap (k ∷ ks)} → + fm₁ ⊆ᵐ fm₂ → fm₁ ⊆ᵐ pop fm₂ narrow₂ {fm₁} {fm₂ = (_ ∷ fm'₂ , push k≢ks _) , kvs≡ks@refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁ with kvs₁⊆kvs₂ k' v' k',v'∈fm'₁ - ... | (v'' , (v'≈v'' , here refl)) rewrite sym (proj₂ fm₁) = ⊥-elim (All¬-¬Any k≢ks (forget {m = proj₁ fm₁} k',v'∈fm'₁)) - ... | (v'' , (v'≈v'' , there k',v'∈fm'₂)) = (v'' , (v'≈v'' , k',v'∈fm'₂)) + ... | (v'' , (v'≈v'' , here refl)) rewrite sym (proj₂ fm₁) = + ⊥-elim (All¬-¬Any k≢ks (forget {m = proj₁ fm₁} k',v'∈fm'₁)) + ... | (v'' , (v'≈v'' , there k',v'∈fm'₂)) = + (v'' , (v'≈v'' , k',v'∈fm'₂)) - narrow : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} → fm₁ ⊆ᵐ fm₂ → pop fm₁ ⊆ᵐ pop fm₂ + narrow : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} → + fm₁ ⊆ᵐ fm₂ → pop fm₁ ⊆ᵐ pop fm₂ narrow {fm₁} {fm₂} x = narrow₂ {pop fm₁} (narrow₁ {fm₂ = fm₂} x) - k,v∈pop⇒k,v∈ : ∀ {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ∷ ks)) → (k' , v) ∈ᵐ pop fm → (¬ k ≡ k' × ((k' , v) ∈ᵐ fm)) + k,v∈pop⇒k,v∈ : ∀ {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ∷ ks)) → + (k' , v) ∈ᵐ pop fm → (¬ k ≡ k' × ((k' , v) ∈ᵐ fm)) k,v∈pop⇒k,v∈ {k} {ks} {k'} {v} (m@((k , _) ∷ fm' , push k≢ks uks') , refl) k',v∈fm = - ((λ { refl → All¬-¬Any k≢ks (forget {m = (fm' , uks')} k',v∈fm) }), there k',v∈fm) + ( (λ { refl → All¬-¬Any k≢ks (forget {m = (fm' , uks')} k',v∈fm) }) + , there k',v∈fm + ) - k,v∈⇒k,v∈pop : ∀ {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ∷ ks)) → ¬ k ≡ k' → (k' , v) ∈ᵐ fm → (k' , v) ∈ᵐ pop fm - k,v∈⇒k,v∈pop {k} {ks} {k'} {v} (m@((k , _) ∷ fm' , push k≢ks uks') , refl) k≢k' (here refl) = ⊥-elim (k≢k' refl) - k,v∈⇒k,v∈pop {k} {ks} {k'} {v} (m@((k , _) ∷ fm' , push k≢ks uks') , refl) k≢k' (there k,v'∈fm') = k,v'∈fm' + k,v∈⇒k,v∈pop : ∀ {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ∷ ks)) → + ¬ k ≡ k' → (k' , v) ∈ᵐ fm → (k' , v) ∈ᵐ pop fm + k,v∈⇒k,v∈pop (m@(_ ∷ _ , push k≢ks _) , refl) k≢k' (here refl) = ⊥-elim (k≢k' refl) + k,v∈⇒k,v∈pop (m@(_ ∷ _ , push k≢ks _) , refl) k≢k' (there k,v'∈fm') = k,v'∈fm' - Provenance-union : ∀ {ks : List A} (fm₁ fm₂ : FiniteMap ks) {k : A} {v : B} → (k , v) ∈ᵐ (fm₁ ⊔ᵐ fm₂) → Σ (B × B) (λ (v₁ , v₂) → ((v ≡ v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ fm₂))) + FromBothMaps : ∀ (k : A) (v : B) {ks : List A} (fm₁ fm₂ : FiniteMap ks) → Set + FromBothMaps k v fm₁ fm₂ = + Σ (B × B) + (λ (v₁ , v₂) → ( (v ≡ v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ fm₂))) + + Provenance-union : ∀ {ks : List A} (fm₁ fm₂ : FiniteMap ks) {k : A} {v : B} → + (k , v) ∈ᵐ (fm₁ ⊔ᵐ fm₂) → FromBothMaps k v fm₁ fm₂ Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) {k} {v} k,v∈fm₁fm₂ with Expr-Provenance k ((` m₁) ∪ (` m₂)) (forget {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂) - ... | (_ , (in₁ (single k,v∈m₁) k∉km₂ , _)) with k∈km₁ ← (forget {m = m₁} k,v∈m₁) rewrite trans ks₁≡ks (sym ks₂≡ks) = ⊥-elim (k∉km₂ k∈km₁) - ... | (_ , (in₂ k∉km₁ (single k,v∈m₂) , _)) with k∈km₂ ← (forget {m = m₂} k,v∈m₂) rewrite trans ks₁≡ks (sym ks₂≡ks) = ⊥-elim (k∉km₁ k∈km₂) + ... | (_ , (in₁ (single k,v∈m₁) k∉km₂ , _)) + with k∈km₁ ← (forget {m = m₁} k,v∈m₁) + rewrite trans ks₁≡ks (sym ks₂≡ks) = + ⊥-elim (k∉km₂ k∈km₁) + ... | (_ , (in₂ k∉km₁ (single k,v∈m₂) , _)) + with k∈km₂ ← (forget {m = m₂} k,v∈m₂) + rewrite trans ks₁≡ks (sym ks₂≡ks) = + ⊥-elim (k∉km₁ k∈km₂) ... | (v₁⊔v₂ , (bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) , k,v₁⊔v₂∈m₁m₂)) - rewrite Map-functional {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂ k,v₁⊔v₂∈m₁m₂ = ((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂))) + rewrite Map-functional {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂ k,v₁⊔v₂∈m₁m₂ = + ((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂))) - pop-⊔-distr : ∀ {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ∷ ks)) → pop (fm₁ ⊔ᵐ fm₂) ≈ᵐ (pop fm₁ ⊔ᵐ pop fm₂) - pop-⊔-distr {k} {ks} fm₁@(m₁ , _) fm₂@(m₂ , _) = (pfm₁fm₂⊆pfm₁pfm₂ , pfm₁pfm₂⊆pfm₁fm₂) + pop-⊔-distr : ∀ {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ∷ ks)) → + pop (fm₁ ⊔ᵐ fm₂) ≈ᵐ (pop fm₁ ⊔ᵐ pop fm₂) + pop-⊔-distr {k} {ks} fm₁@(m₁ , _) fm₂@(m₂ , _) = + (pfm₁fm₂⊆pfm₁pfm₂ , pfm₁pfm₂⊆pfm₁fm₂) where -- pfm₁fm₂⊆pfm₁pfm₂ = {!!} pfm₁fm₂⊆pfm₁pfm₂ : pop (fm₁ ⊔ᵐ fm₂) ⊆ᵐ (pop fm₁ ⊔ᵐ pop fm₂) pfm₁fm₂⊆pfm₁pfm₂ k' v' k',v'∈pfm₁fm₂ with (k≢k' , k',v'∈fm₁fm₂) ← k,v∈pop⇒k,v∈ (fm₁ ⊔ᵐ fm₂) k',v'∈pfm₁fm₂ - with ((v₁ , v₂) , (refl , (k,v₁∈fm₁ , k,v₂∈fm₂))) ← Provenance-union fm₁ fm₂ k',v'∈fm₁fm₂ + with ((v₁ , v₂) , (refl , (k,v₁∈fm₁ , k,v₂∈fm₂))) + ← Provenance-union fm₁ fm₂ k',v'∈fm₁fm₂ with k',v₁∈pfm₁ ← k,v∈⇒k,v∈pop fm₁ k≢k' k,v₁∈fm₁ with k',v₂∈pfm₂ ← k,v∈⇒k,v∈pop fm₂ k≢k' k,v₂∈fm₂ - = (v₁ ⊔₂ v₂ , (IsLattice.≈-refl lB , ⊔-combines {m₁ = proj₁ (pop fm₁)} {m₂ = proj₁ (pop fm₂)} k',v₁∈pfm₁ k',v₂∈pfm₂)) + = + ( v₁ ⊔₂ v₂ + , (IsLattice.≈-refl lB + , ⊔-combines {m₁ = proj₁ (pop fm₁)} + {m₂ = proj₁ (pop fm₂)} + k',v₁∈pfm₁ k',v₂∈pfm₂ + ) + ) pfm₁pfm₂⊆pfm₁fm₂ : (pop fm₁ ⊔ᵐ pop fm₂) ⊆ᵐ pop (fm₁ ⊔ᵐ fm₂) pfm₁pfm₂⊆pfm₁fm₂ k' v' k',v'∈pfm₁pfm₂ - with ((v₁ , v₂) , (refl , (k,v₁∈pfm₁ , k,v₂∈pfm₂))) ← Provenance-union (pop fm₁) (pop fm₂) k',v'∈pfm₁pfm₂ + with ((v₁ , v₂) , (refl , (k,v₁∈pfm₁ , k,v₂∈pfm₂))) + ← Provenance-union (pop fm₁) (pop fm₂) k',v'∈pfm₁pfm₂ with (k≢k' , k',v₁∈fm₁) ← k,v∈pop⇒k,v∈ fm₁ k,v₁∈pfm₁ with (_ , k',v₂∈fm₂) ← k,v∈pop⇒k,v∈ fm₂ k,v₂∈pfm₂ - = (v₁ ⊔₂ v₂ , (IsLattice.≈-refl lB , k,v∈⇒k,v∈pop (fm₁ ⊔ᵐ fm₂) k≢k' (⊔-combines {m₁ = m₁} {m₂ = m₂} k',v₁∈fm₁ k',v₂∈fm₂))) + = + ( v₁ ⊔₂ v₂ + , ( IsLattice.≈-refl lB + , k,v∈⇒k,v∈pop (fm₁ ⊔ᵐ fm₂) k≢k' + (⊔-combines {m₁ = m₁} {m₂ = m₂} + k',v₁∈fm₁ k',v₂∈fm₂) + ) + ) - from-rest : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → proj₂ (from fm) ≡ from (pop fm) + from-rest : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → + proj₂ (from fm) ≡ from (pop fm) from-rest (((_ ∷ fm') , push _ ufm') , 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-≈ : ∀ {ks : List A} → {fm₁ fm₂ : FiniteMap ks} → + fm₁ ≈ᵐ fm₂ → (_≈ⁱᵖ_ {length 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₂ + 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₂) | 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₂ - = (v₁≈v₁' , from-preserves-≈ {ks'} {pop fm₁} {pop fm₂} (pop-≈ fm₁ fm₂ fm₁≈fm₂)) + = + ( v₁≈v₁' + , from-preserves-≈ {ks'} {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-≈ : ∀ {ks : List A} (uks : Unique ks) {ip₁ ip₂ : IterProd (length ks)} → + _≈ⁱᵖ_ {length 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₁ + inductive-step : ∀ {v₁ v₂ : B} {rest₁ rest₂ : IterProd (length ks')} → + v₁ ≈₂ v₂ → _≈ⁱᵖ_ {length ks'} rest₁ rest₂ → + to uks (v₁ , rest₁) ⊆ᵐ to uks (v₂ , rest₂) + inductive-step {v₁} {v₂} {rest₁} {rest₂} v₁≈v₂ rest₁≈rest₂ k v k,v∈kvs₁ with ((fm'₁ , ufm'₁) , fm'₁≡ks') ← to uks' rest₁ in p₁ with ((fm'₂ , ufm'₂) , fm'₂≡ks') ← to uks' rest₂ in p₂ with k,v∈kvs₁ ... | here refl = (v₂ , (v₁≈v₂ , here refl)) - ... | there k,v∈fm'₁ 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∈fm'₁ in (v' , (v≈v' , there k,v'∈kvs₁)) + ... | there k,v∈fm'₁ with refl ← p₁ with refl ← p₂ = + let + (fm'₁⊆fm'₂ , _) = to-preserves-≈ uks' {rest₁} {rest₂} + rest₁≈rest₂ + (v' , (v≈v' , k,v'∈kvs₁)) = fm'₁⊆fm'₂ k v k,v∈fm'₁ + in + (v' , (v≈v' , there k,v'∈kvs₁)) + + fm₁⊆fm₂ : to uks ip₁ ⊆ᵐ to uks ip₂ + fm₁⊆fm₂ = inductive-step v₁≈v₂ rest₁≈rest₂ fm₂⊆fm₁ : to uks ip₂ ⊆ᵐ to uks ip₁ - fm₂⊆fm₁ k v k,v∈kvs₂ - with ((fm'₁ , ufm'₁) , fm'₁≡ks') ← to uks' rest₁ in p₁ - with ((fm'₂ , ufm'₂) , fm'₂≡ks') ← to uks' rest₂ in p₂ - with k,v∈kvs₂ - ... | here refl = (v₁ , (IsLattice.≈-sym lB v₁≈v₂ , here refl)) - ... | there k,v∈fm'₂ 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∈fm'₂ in (v' , (v≈v' , there k,v'∈kvs₂)) + fm₂⊆fm₁ = inductive-step (≈₂-sym v₁≈v₂) + (IP.≈-sym (length ks') rest₁≈rest₂) - from-⊔-distr : ∀ {ks : List A} → (fm₁ fm₂ : FiniteMap ks) → _≈ⁱᵖ_ {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₂