DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Prove distributivity in the other direction, too

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-03-01 19:07:59 -08:00
parent 8715d6d89c
commit 52e7a7a208
1 changed files with 90 additions and 48 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

128
Lattice/FiniteValueMap.agda
View File

@ -15,7 +15,8 @@ module Lattice.FiniteValueMap (A : Set) (B : Set)
(≈-dec-A : Decidable (_≡_ {_} {A})) (≈-dec-A : Decidable (_≡_ {_} {A}))
(lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
open import Data.List using (List; length; []; _∷_) open import Data.List using (List; length; []; _∷_; map)
open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_)
open import Data.Product using (Σ; proj₁; proj₂; _×_) open import Data.Product using (Σ; proj₁; proj₂; _×_)
open import Data.Empty using (⊥-elim) open import Data.Empty using (⊥-elim)
open import Utils using (Unique; push; empty; All¬-¬Any) open import Utils using (Unique; push; empty; All¬-¬Any)
@ -36,21 +37,21 @@ module IterProdIsomorphism where
from : ∀ {ks : List A} → FiniteMap ks → IterProd (length ks) from : ∀ {ks : List A} → FiniteMap ks → IterProd (length ks)
from {[]} (([] , _) , _) = tt from {[]} (([] , _) , _) = tt
from {k ∷ ks'} (((k' , v) ∷ kvs' , push _ uks') , refl) = (v , from ((kvs' , uks'), refl)) from {k ∷ ks'} (((k' , v) ∷ fm' , push _ uks') , refl) = (v , from ((fm' , uks'), refl))
to : ∀ {ks : List A} → Unique ks → IterProd (length ks) → FiniteMap ks to : ∀ {ks : List A} → Unique ks → IterProd (length ks) → FiniteMap ks
to {[]} _ ⊤ = (([] , empty) , refl) to {[]} _ ⊤ = (([] , empty) , refl)
to {k ∷ ks'} (push k≢ks' uks') (v , rest) to {k ∷ ks'} (push k≢ks' uks') (v , rest) =
with to uks' rest
... | ((kvs' , ukvs') , kvs'≡ks') =
let let
((fm' , ufm') , fm'≡ks') = to uks' rest
-- This would be easier if we pattern matched on the equiality proof -- This would be easier if we pattern matched on the equiality proof
-- to get refl, but that makes it harder to reason about 'to' when -- to get refl, but that makes it harder to reason about 'to' when
-- the arguments are not known to be refl. -- the arguments are not known to be refl.
k≢kvs' = subst (λ ks → All (λ k' → ¬ k ≡ k') ks) (sym kvs'≡ks') k≢ks' k≢fm' = subst (λ ks → All (λ k' → ¬ k ≡ k') ks) (sym fm'≡ks') k≢ks'
kvs≡ks = cong (k ∷_) kvs'≡ks' kvs≡ks = cong (k ∷_) fm'≡ks'
in in
(((k , v) ∷ kvs' , push k≢kvs' ukvs') , kvs≡ks) (((k , v) ∷ fm' , push k≢fm' ufm') , kvs≡ks)
private private
@ -76,10 +77,10 @@ module IterProdIsomorphism where
Inverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {ks}) (from {ks}) (to {ks} uks) -- from (to x) = x Inverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {ks}) (from {ks}) (to {ks} uks) -- from (to x) = x
from-to-inverseˡ {[]} _ _ = IsEquivalence.≈-refl (IP.≈-equiv 0) from-to-inverseˡ {[]} _ _ = IsEquivalence.≈-refl (IP.≈-equiv 0)
from-to-inverseˡ {k ∷ ks'} (push k≢ks' uks') (v , rest) from-to-inverseˡ {k ∷ ks'} (push k≢ks' uks') (v , rest)
with ((kvs' , ukvs') , refl) ← to uks' rest in p rewrite sym p = with ((fm' , ufm') , refl) ← to uks' rest in p rewrite sym p =
(IsLattice.≈-refl lB , from-to-inverseˡ {ks'} uks' rest) (IsLattice.≈-refl lB , from-to-inverseˡ {ks'} uks' rest)
-- the rewrite here is needed because the IH is in terms of `to uks' rest`, -- the rewrite here is needed because the IH is in terms of `to uks' rest`,
-- but we end up with the 'unpacked' form (kvs', ...). So, put it back -- but we end up with the 'unpacked' form (fm', ...). So, put it back
-- in the 'packed' form after we've performed enough inspection -- in the 'packed' form after we've performed enough inspection
-- to know we take the cons branch of `to`. -- to know we take the cons branch of `to`.
@ -88,24 +89,24 @@ module IterProdIsomorphism where
from-to-inverseʳ : ∀ {ks : List A} (uks : Unique ks) → from-to-inverseʳ : ∀ {ks : List A} (uks : Unique ks) →
Inverseʳ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {ks}) (from {ks}) (to {ks} uks) -- to (from x) = x 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ʳ {[]} _ (([] , empty) , kvs≡ks) rewrite kvs≡ks = ((λ k v ()) , (λ k v ()))
from-to-inverseʳ {k ∷ ks'} uks@(push k≢ks'₁ uks'₁) fm₁@(m₁@((k , v) ∷ kvs'₁ , push k≢ks'₂ uks'₂) , refl) from-to-inverseʳ {k ∷ ks'} uks@(push k≢ks'₁ uks'₁) fm₁@(m₁@((k , v) ∷ fm'₁ , push k≢ks'₂ uks'₂) , refl)
with to uks'₁ (from ((kvs'₁ , uks'₂) , refl)) | from-to-inverseʳ {ks'} uks'₁ ((kvs'₁ , uks'₂) , refl) with to uks'₁ (from ((fm'₁ , uks'₂) , refl)) | from-to-inverseʳ {ks'} uks'₁ ((fm'₁ , uks'₂) , refl)
... | ((kvs'₂ , ukvs'₂) , _) | (kvs'₂⊆kvs'₁ , kvs'₁⊆kvs'₂) = (m₂⊆m₁ , m₁⊆m₂) ... | ((fm'₂ , ufm'₂) , _) | (fm'₂⊆fm'₁ , fm'₁⊆fm'₂) = (m₂⊆m₁ , m₁⊆m₂)
where where
kvs₁ = (k , v) ∷ kvs'₁ kvs₁ = (k , v) ∷ fm'₁
kvs₂ = (k , v) ∷ kvs'₂ kvs₂ = (k , v) ∷ fm'₂
m₁⊆m₂ : subset-impl kvs₁ kvs₂ 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'∈kvs'₁) = m₁⊆m₂ k' v' (there k',v'∈fm'₁) =
let (v'' , (v'≈v'' , k',v''∈kvs'₂)) = kvs'₁⊆kvs'₂ k' v' k',v'∈kvs'₁ let (v'' , (v'≈v'' , k',v''∈fm'₂)) = fm'₁⊆fm'₂ k' v' k',v'∈fm'₁
in (v'' , (v'≈v'' , there k',v''∈kvs'₂)) in (v'' , (v'≈v'' , there k',v''∈fm'₂))
m₂⊆m₁ : subset-impl kvs₂ kvs₁ 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'∈kvs'₂) = m₂⊆m₁ k' v' (there k',v'∈fm'₂) =
let (v'' , (v'≈v'' , k',v''∈kvs'₁)) = kvs'₂⊆kvs'₁ k' v' k',v'∈kvs'₂ let (v'' , (v'≈v'' , k',v''∈fm'₁)) = fm'₂⊆fm'₁ k' v' k',v'∈fm'₂
in (v'' , (v'≈v'' , there k',v''∈kvs'₁)) in (v'' , (v'≈v'' , there k',v''∈fm'₁))
private 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)
@ -119,40 +120,39 @@ module IterProdIsomorphism where
-- matching into a helper functions, and write solutions in terms -- matching into a helper functions, and write solutions in terms
-- of that. -- of that.
pop : ∀ {k : A} {ks : List A} → FiniteMap (k ∷ ks) → FiniteMap ks pop : ∀ {k : A} {ks : List A} → FiniteMap (k ∷ ks) → FiniteMap ks
pop (((_ ∷ kvs') , push _ ukvs') , refl) = ((kvs' , ukvs') , refl) 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 : 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} {ks} fm₁ fm₂ (fm₁⊆fm₂ , fm₂⊆fm₁) = (narrow fm₁⊆fm₂ , narrow fm₂⊆fm₁)
where where
narrow₁ : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} → fm₁ ⊆ᵐ fm₂ → pop fm₁ ⊆ᵐ fm₂ 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₁ {(_ ∷ _ , 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₂ = (_ ∷ kvs'₂ , push k≢ks _) , kvs≡ks@refl} kvs₁⊆kvs₂ k' v' k',v'∈kvs'₁ narrow₂ {fm₁} {fm₂ = (_ ∷ fm'₂ , push k≢ks _) , kvs≡ks@refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁
with kvs₁⊆kvs₂ k' v' k',v'∈kvs'₁ 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'∈kvs'₁)) ... | (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'∈kvs'₂)) = (v'' , (v'≈v'' , k',v'∈kvs'₂)) ... | (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) 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 , _) ∷ kvs' , push k≢ks uks') , refl) 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 = (kvs' , 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 : 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 , _) ∷ kvs' , 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' (here refl) = ⊥-elim (k≢k' refl)
k,v∈⇒k,v∈pop {k} {ks} {k'} {v} (m@((k , _) ∷ kvs' , push k≢ks uks') , refl) k≢k' (there k,v'∈kvs') = k,v'∈kvs' 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'
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₂))) 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₂)))
Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) k v 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₂) 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₁ (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₂ 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₂)) ... | (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 : 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} {ks} fm₁@(m₁ , _) fm₂@(m₂ , _) = (pfm₁fm₂⊆pfm₁pfm₂ , pfm₁pfm₂⊆pfm₁fm₂)
where where
@ -160,20 +160,20 @@ module IterProdIsomorphism where
pfm₁fm₂⊆pfm₁pfm₂ : pop (fm₁ ⊔ᵐ fm₂) ⊆ᵐ (pop fm₁ ⊔ᵐ pop fm₂) pfm₁fm₂⊆pfm₁pfm₂ : pop (fm₁ ⊔ᵐ fm₂) ⊆ᵐ (pop fm₁ ⊔ᵐ pop fm₂)
pfm₁fm₂⊆pfm₁pfm₂ k' v' k',v'∈pfm₁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 (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' 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₁
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₂ : (pop fm₁ ⊔ᵐ pop fm₂) ⊆ᵐ pop (fm₁ ⊔ᵐ fm₂)
pfm₁pfm₂⊆pfm₁fm₂ k' v' k',v'∈pfm₁pfm₂ 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' 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≢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₂ 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 (((_ ∷ kvs') , push _ ukvs') , refl) = refl 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-≈ : ∀ {ks : List A} → (fm₁ fm₂ : FiniteMap ks) → fm₁ ≈ᵐ fm₂ → (_≈ⁱᵖ_ {ks}) (from fm₁) (from fm₂)
from-preserves-≈ {[]} (([] , _) , _) (([] , _) , _) _ = IsEquivalence.≈-refl ≈ᵘ-equiv from-preserves-≈ {[]} (([] , _) , _) (([] , _) , _) _ = IsEquivalence.≈-refl ≈ᵘ-equiv
@ -192,19 +192,19 @@ module IterProdIsomorphism where
where where
fm₁⊆fm₂ : to uks ip₁ ⊆ᵐ to uks ip₂ fm₁⊆fm₂ : to uks ip₁ ⊆ᵐ to uks ip₂
fm₁⊆fm₂ k v k,v∈kvs₁ fm₁⊆fm₂ k v k,v∈kvs₁
with ((kvs'₁ , ukvs'₁) , kvs'₁≡ks') ← to uks' rest₁ in p₁ with ((fm'₁ , ufm'₁) , fm'₁≡ks') ← to uks' rest₁ in p₁
with ((kvs'₂ , ukvs'₂) , kvs'₂≡ks') ← to uks' rest₂ in p₂ with ((fm'₂ , ufm'₂) , fm'₂≡ks') ← to uks' rest₂ in p₂
with k,v∈kvs₁ with k,v∈kvs₁
... | here refl = (v₂ , (v₁≈v₂ , here refl)) ... | 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₁)) ... | 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₁ : to uks ip₂ ⊆ᵐ to uks ip₁ fm₂⊆fm₁ : to uks ip₂ ⊆ᵐ to uks ip₁
fm₂⊆fm₁ k v k,v∈kvs₂ fm₂⊆fm₁ k v k,v∈kvs₂
with ((kvs'₁ , ukvs'₁) , kvs'₁≡ks') ← to uks' rest₁ in p₁ with ((fm'₁ , ufm'₁) , fm'₁≡ks') ← to uks' rest₁ in p₁
with ((kvs'₂ , ukvs'₂) , kvs'₂≡ks') ← to uks' rest₂ in p₂ with ((fm'₂ , ufm'₂) , fm'₂≡ks') ← to uks' rest₂ in p₂
with k,v∈kvs₂ with k,v∈kvs₂
... | here refl = (v₁ , (IsLattice.≈-sym lB v₁≈v₂ , here refl)) ... | 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₂)) ... | 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₂))
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) → _≈ⁱᵖ_ {ks} (from (fm₁ ⊔ᵐ fm₂)) (_⊔ⁱᵖ_ {ks} (from fm₁) (from fm₂))
from-⊔-distr {[]} fm₁ fm₂ = IsEquivalence.≈-refl ≈ᵘ-equiv from-⊔-distr {[]} fm₁ fm₂ = IsEquivalence.≈-refl ≈ᵘ-equiv
@ -222,3 +222,45 @@ module IterProdIsomorphism where
= ( IsLattice.≈-refl lB = ( 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₂)))
) )
-- 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₂)))
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
fm₁ = to uks ip₁
fm₁' = to uks' rest₁
fm₂ = to uks ip₂
fm₂' = to uks' rest₂
fm = to uks (_⊔ⁱᵖ_ {k ∷ ks'} ip₁ ip₂)
fm⊆fm₁fm₂ : fm ⊆ᵐ (fm₁ ⊔ᵐ fm₂)
fm⊆fm₁fm₂ k v (here refl) =
(v₁ ⊔₂ v₂
, (IsLattice.≈-refl lB
, ⊔-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'₂)))
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 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₁')))
... | 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₂'
in
(v' , (v₁⊔v₂≈v' , there v'∈fm'))