More cleanup to FiniteValueMap
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
01f4e02026
commit
f00dabfc93
|
|
@ -312,25 +312,39 @@ module IterProdIsomorphism where
|
||||||
fm₂⊆fm₁ = inductive-step (≈₂-sym v₁≈v₂)
|
fm₂⊆fm₁ = inductive-step (≈₂-sym v₁≈v₂)
|
||||||
(IP.≈-sym (length ks') rest₁≈rest₂)
|
(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 {[]} fm₁ fm₂ = IsEquivalence.≈-refl ≈ᵘ-equiv
|
||||||
from-⊔-distr {k ∷ ks} fm₁@(m₁ , _) fm₂@(m₂ , _)
|
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
|
... | (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₂)
|
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₂}
|
||||||
... | (_ , (in₂ k∉km₁ _ , _)) = ⊥-elim (k∉km₁ (forget {m = m₁} k,v₁∈fm₁))
|
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₂))
|
... | (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 = 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 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₂
|
rewrite from-rest (fm₁ ⊔ᵐ fm₂) rewrite from-rest fm₁ rewrite from-rest fm₂
|
||||||
= ( 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₂)))
|
||||||
)
|
)
|
||||||
|
|
||||||
|
|
||||||
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 {[]} 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)
|
to-⊔-distr {ks@(k ∷ ks')} uks@(push k≢ks' uks') ip₁@(v₁ , rest₁) ip₂@(v₂ , rest₂) = (fm⊆fm₁fm₂ , fm₁fm₂⊆fm)
|
||||||
where
|
where
|
||||||
|
|
@ -344,27 +358,45 @@ module IterProdIsomorphism where
|
||||||
fm⊆fm₁fm₂ k v (here refl) =
|
fm⊆fm₁fm₂ k v (here refl) =
|
||||||
(v₁ ⊔₂ v₂
|
(v₁ ⊔₂ v₂
|
||||||
, (IsLattice.≈-refl lB
|
, (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')
|
fm⊆fm₁fm₂ k' v (there k',v∈fm')
|
||||||
with (fm'⊆fm'₁fm'₂ , _) ← to-⊔-distr uks' rest₁ rest₂
|
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 (v' , (v₁⊔v₂≈v' , k',v'∈fm'₁fm'₂))
|
||||||
with (_ , (refl , (v₁∈fm'₁ , v₂∈fm'₂))) ← Provenance-union fm₁' fm₂' k',v'∈fm'₁fm'₂ =
|
← fm'⊆fm'₁fm'₂ k' v k',v∈fm'
|
||||||
(v' , (v₁⊔v₂≈v' , ⊔-combines {m₁ = proj₁ fm₁} {m₂ = proj₁ fm₂} (there v₁∈fm'₁) (there 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 : (fm₁ ⊔ᵐ fm₂) ⊆ᵐ fm
|
||||||
fm₁fm₂⊆fm k' v k',v∈fm₁fm₂
|
fm₁fm₂⊆fm k' v k',v∈fm₁fm₂
|
||||||
with (_ , fm'₁fm'₂⊆fm') ← to-⊔-distr uks' rest₁ rest₂
|
with (_ , fm'₁fm'₂⊆fm')
|
||||||
with (_ , (refl , (v₁∈fm₁ , v₂∈fm₂))) ← Provenance-union fm₁ fm₂ k',v∈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₂
|
with v₁∈fm₁ | v₂∈fm₂
|
||||||
... | here refl | here refl = (v , (IsLattice.≈-refl lB , here refl))
|
... | here refl | 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₂')))
|
(v , (IsLattice.≈-refl lB , here refl))
|
||||||
... | 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 | 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₂' =
|
... | there k',v₁∈fm₁' | there k',v₂∈fm₂' =
|
||||||
let
|
let
|
||||||
k',v₁v₂∈fm₁'fm₂' = ⊔-combines {m₁ = proj₁ fm₁'} {m₂ = proj₁ fm₂'} k',v₁∈fm₁' k',v₂∈fm₂'
|
k',v₁v₂∈fm₁'fm₂' =
|
||||||
(v' , (v₁⊔v₂≈v' , v'∈fm')) = fm'₁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
|
in
|
||||||
(v' , (v₁⊔v₂≈v' , there v'∈fm'))
|
(v' , (v₁⊔v₂≈v' , there v'∈fm'))
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue
Block a user