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

Use the new provenance function to clean up some proofs

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-03-07 19:59:14 -08:00
parent 48983c55b1
commit 34203840c8
2 changed files with 67 additions and 97 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
Lattice/FiniteValueMap.agda
View File

@ -36,6 +36,7 @@ open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB
; _∈_
; Map-functional
; Expr-Provenance
; Expr-Provenance-≡
; _∩_; _∪_; `_
; in₁; in₂; bothᵘ; single
; ⊔-combines
@ -212,17 +213,16 @@ module IterProdIsomorphism where
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 Expr-Provenance-≡ ((` m₁) ∪ (` m₂)) 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₂) , _))
... | 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₂ =
... | bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) =
((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂)))
pop-⊔-distr : ∀ {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ∷ ks)) →

154
Lattice/Map.agda
View File

@ -592,8 +592,8 @@ Expr-Provenance k (e₁ ∩ e₂) k∈ke₁e₂
... | no k∉ke₁ | yes k∈ke₂ = ⊥-elim (intersect-preserves-∉₁ {l₂ = proj₁ ⟦ e₂ ⟧} k∉ke₁ k∈ke₁e₂)
... | no k∉ke₁ | no k∉ke₂ = ⊥-elim (intersect-preserves-∉₂ {l₁ = proj₁ ⟦ e₁ ⟧} k∉ke₂ k∈ke₁e₂)
Expr-Provenance-≡ : ∀ (k : A) (v : B) (e : Expr) → (k , v) ∈ ⟦ e ⟧ → Provenance k v e
Expr-Provenance-≡ k v e k,v∈e
Expr-Provenance-≡ : ∀ {k : A} {v : B} (e : Expr) → (k , v) ∈ ⟦ e ⟧ → Provenance k v e
Expr-Provenance-≡ {k} {v} e k,v∈e
with (v' , (p , k,v'∈e)) ← Expr-Provenance k e (forget {m = ⟦ e ⟧} k,v∈e)
rewrite Map-functional {m = ⟦ e ⟧} k,v∈e k,v'∈e = p
@ -665,19 +665,16 @@ private module I⊓ = ImplInsert _⊓₂_
⊔-⊆ : ∀ (m₁ m₂ m₃ m₄ : Map) → m₁ ≈ m₂ → m₃ ≈ m₄ → (m₁ ⊔ m₃) ⊆ (m₂ ⊔ m₄)
⊔-⊆ m₁ m₂ m₃ m₄ m₁≈m₂ m₃≈m₄ k v k,v∈m₁m₃
with Expr-Provenance k ((` m₁) ∪ (` m₃)) (∈-cong proj₁ k,v∈m₁m₃)
... | (_ , (bothᵘ (single {v₁} v₁∈m₁) (single {v₃} v₃∈m₃) , v₁v₃∈m₁m₃))
rewrite Map-functional {m = m₁ ⊔ m₃} k,v∈m₁m₃ v₁v₃∈m₁m₃ =
with Expr-Provenance-≡ ((` m₁) ∪ (` m₃)) k,v∈m₁m₃
... | bothᵘ (single {v₁} v₁∈m₁) (single {v₃} v₃∈m₃) =
let (v₂ , (v₁≈v₂ , k,v₂∈m₂)) = proj₁ m₁≈m₂ k v₁ v₁∈m₁
(v₄ , (v₃≈v₄ , k,v₄∈m₄)) = proj₁ m₃≈m₄ k v₃ v₃∈m₃
in (v₂ ⊔₂ v₄ , (≈₂-⊔₂-cong v₁≈v₂ v₃≈v₄ , I⊔.union-combines (proj₂ m₂) (proj₂ m₄) k,v₂∈m₂ k,v₄∈m₄))
... | (_ , (in₁ (single {v₁} v₁∈m₁) k∉km₃ , v₁∈m₁m₃))
rewrite Map-functional {m = m₁ ⊔ m₃} k,v∈m₁m₃ v₁∈m₁m₃ =
... | in₁ (single {v₁} v₁∈m₁) k∉km₃ =
let (v₂ , (v₁≈v₂ , k,v₂∈m₂)) = proj₁ m₁≈m₂ k v₁ v₁∈m₁
k∉km₄ = ≈-∉-cong {m₃} {m₄} m₃≈m₄ k∉km₃
in (v₂ , (v₁≈v₂ , I⊔.union-preserves-∈₁ (proj₂ m₂) k,v₂∈m₂ k∉km₄))
... | (_ , (in₂ k∉km₁ (single {v₃} v₃∈m₃) , v₃∈m₁m₃))
rewrite Map-functional {m = m₁ ⊔ m₃} k,v∈m₁m₃ v₃∈m₁m₃ =
... | in₂ k∉km₁ (single {v₃} v₃∈m₃) =
let (v₄ , (v₃≈v₄ , k,v₄∈m₄)) = proj₁ m₃≈m₄ k v₃ v₃∈m₃
k∉km₂ = ≈-∉-cong {m₁} {m₂} m₁≈m₂ k∉km₁
in (v₄ , (v₃≈v₄ , I⊔.union-preserves-∈₂ k∉km₂ k,v₄∈m₄))
@ -690,9 +687,8 @@ private module I⊓ = ImplInsert _⊓₂_
where
⊓-⊆ : ∀ (m₁ m₂ m₃ m₄ : Map) → m₁ ≈ m₂ → m₃ ≈ m₄ → (m₁ ⊓ m₃) ⊆ (m₂ ⊓ m₄)
⊓-⊆ m₁ m₂ m₃ m₄ m₁≈m₂ m₃≈m₄ k v k,v∈m₁m₃
with Expr-Provenance k ((` m₁) ∩ (` m₃)) (∈-cong proj₁ k,v∈m₁m₃)
... | (_ , (bothⁱ (single {v₁} v₁∈m₁) (single {v₃} v₃∈m₃) , v₁v₃∈m₁m₃))
rewrite Map-functional {m = m₁ ⊓ m₃} k,v∈m₁m₃ v₁v₃∈m₁m₃ =
with Expr-Provenance-≡ ((` m₁) ∩ (` m₃)) k,v∈m₁m₃
... | bothⁱ (single {v₁} v₁∈m₁) (single {v₃} v₃∈m₃) =
let (v₂ , (v₁≈v₂ , k,v₂∈m₂)) = proj₁ m₁≈m₂ k v₁ v₁∈m₁
(v₄ , (v₃≈v₄ , k,v₄∈m₄)) = proj₁ m₃≈m₄ k v₃ v₃∈m₃
in (v₂ ⊓₂ v₄ , (≈₂-⊓₂-cong v₁≈v₂ v₃≈v₄ , I⊓.intersect-combines (proj₂ m₂) (proj₂ m₄) k,v₂∈m₂ k,v₄∈m₄))
@ -702,13 +698,12 @@ private module I⊓ = ImplInsert _⊓₂_
where
mm-m-⊆ : (m ⊔ m) ⊆ m
mm-m-⊆ k v k,v∈mm
with Expr-Provenance k ((` m) ∪ (` m)) (∈-cong proj₁ k,v∈mm)
... | (_ , (bothᵘ (single {v'} v'∈m) (single {v''} v''∈m) , v'v''∈mm))
rewrite Map-functional {m = m} v'∈m v''∈m
rewrite Map-functional {m = m ⊔ m} k,v∈mm v'v''∈mm =
with Expr-Provenance-≡ ((` m) ∪ (` m)) k,v∈mm
... | bothᵘ (single {v'} v'∈m) (single {v''} v''∈m)
rewrite Map-functional {m = m} v'∈m v''∈m =
(v'' , (⊔₂-idemp v'' , v''∈m))
... | (_ , (in₁ (single {v'} v'∈m) k∉km , _)) = ⊥-elim (k∉km (∈-cong proj₁ v'∈m))
... | (_ , (in₂ k∉km (single {v''} v''∈m) , _)) = ⊥-elim (k∉km (∈-cong proj₁ v''∈m))
... | in₁ (single {v'} v'∈m) k∉km = ⊥-elim (k∉km (∈-cong proj₁ v'∈m))
... | in₂ k∉km (single {v''} v''∈m) = ⊥-elim (k∉km (∈-cong proj₁ v''∈m))
m-mm-⊆ : m ⊆ (m ⊔ m)
m-mm-⊆ k v k,v∈m = (v ⊔₂ v , (≈₂-sym (⊔₂-idemp v) , I⊔.union-combines u u k,v∈m k,v∈m))
@ -718,15 +713,12 @@ private module I⊓ = ImplInsert _⊓₂_
where
⊔-comm-⊆ : ∀ (m₁ m₂ : Map) → (m₁ ⊔ m₂) ⊆ (m₂ ⊔ m₁)
⊔-comm-⊆ m₁@(l₁ , u₁) m₂@(l₂ , u₂) k v k,v∈m₁m₂
with Expr-Provenance k ((` m₁) ∪ (` m₂)) (∈-cong proj₁ k,v∈m₁m₂)
... | (_ , (bothᵘ {v₁} {v₂} (single v₁∈m₁) (single v₂∈m₂) , v₁v₂∈m₁m₂))
rewrite Map-functional {m = m₁ ⊔ m₂} k,v∈m₁m₂ v₁v₂∈m₁m₂ =
with Expr-Provenance-≡ ((` m₁) ∪ (` m₂)) k,v∈m₁m₂
... | bothᵘ {v₁} {v₂} (single v₁∈m₁) (single v₂∈m₂) =
(v₂ ⊔₂ v₁ , (⊔₂-comm v₁ v₂ , I⊔.union-combines u₂ u₁ v₂∈m₂ v₁∈m₁))
... | (_ , (in₁ {v₁} (single v₁∈m₁) k∉km₂ , v₁∈m₁m₂))
rewrite Map-functional {m = m₁ ⊔ m₂} k,v∈m₁m₂ v₁∈m₁m₂ =
... | in₁ {v₁} (single v₁∈m₁) k∉km₂ =
(v₁ , (≈₂-refl , I⊔.union-preserves-∈₂ k∉km₂ v₁∈m₁))
... | (_ , (in₂ {v₂} k∉km₁ (single v₂∈m₂) , v₂∈m₁m₂))
rewrite Map-functional {m = m₁ ⊔ m₂} k,v∈m₁m₂ v₂∈m₁m₂ =
... | in₂ {v₂} k∉km₁ (single v₂∈m₂) =
(v₂ , (≈₂-refl , I⊔.union-preserves-∈₁ u₂ v₂∈m₂ k∉km₁))
⊔-assoc : ∀ (m₁ m₂ m₃ : Map) → ((m₁ ⊔ m₂) ⊔ m₃) ≈ (m₁ ⊔ (m₂ ⊔ m₃))
@ -734,54 +726,40 @@ private module I⊓ = ImplInsert _⊓₂_
where
⊔-assoc₁ : ((m₁ ⊔ m₂) ⊔ m₃) ⊆ (m₁ ⊔ (m₂ ⊔ m₃))
⊔-assoc₁ k v k,v∈m₁₂m₃
with Expr-Provenance k (((` m₁) ∪ (` m₂)) ∪ (` m₃)) (∈-cong proj₁ k,v∈m₁₂m₃)
... | (_ , (in₂ k∉ke₁₂ (single {v₃} v₃∈e₃) , v₃∈m₁₂m₃))
rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₃∈m₁₂m₃ =
with Expr-Provenance-≡ (((` m₁) ∪ (` m₂)) ∪ (` m₃)) k,v∈m₁₂m₃
... | in₂ k∉ke₁₂ (single {v₃} v₃∈e₃) =
let (k∉ke₁ , k∉ke₂) = I⊔.∉-union-∉-either {l₁ = l₁} {l₂ = l₂} k∉ke₁₂
in (v₃ , (≈₂-refl , I⊔.union-preserves-∈₂ k∉ke₁ (I⊔.union-preserves-∈₂ k∉ke₂ v₃∈e₃)))
... | (_ , (in₁ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) k∉ke₃ , v₂∈m₁₂m₃))
rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₂∈m₁₂m₃ =
... | in₁ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) k∉ke₃ =
(v₂ , (≈₂-refl , I⊔.union-preserves-∈₂ k∉ke₁ (I⊔.union-preserves-∈₁ u₂ v₂∈e₂ k∉ke₃)))
... | (_ , (bothᵘ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₂v₃∈m₁₂m₃))
rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₂v₃∈m₁₂m₃ =
... | bothᵘ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) =
(v₂ ⊔₂ v₃ , (≈₂-refl , I⊔.union-preserves-∈₂ k∉ke₁ (I⊔.union-combines u₂ u₃ v₂∈e₂ v₃∈e₃)))
... | (_ , (in₁ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) k∉ke₃ , v₁∈m₁₂m₃))
rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₁∈m₁₂m₃ =
... | in₁ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) k∉ke₃ =
(v₁ , (≈₂-refl , I⊔.union-preserves-∈₁ u₁ v₁∈e₁ (I⊔.union-preserves-∉ k∉ke₂ k∉ke₃)))
... | (_ , (bothᵘ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) (single {v₃} v₃∈e₃) , v₁v₃∈m₁₂m₃))
rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₁v₃∈m₁₂m₃ =
... | bothᵘ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) (single {v₃} v₃∈e₃) =
(v₁ ⊔₂ v₃ , (≈₂-refl , I⊔.union-combines u₁ (I⊔.union-preserves-Unique l₂ l₃ u₃) v₁∈e₁ (I⊔.union-preserves-∈₂ k∉ke₂ v₃∈e₃)))
... | (_ , (in₁ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) k∉ke₃), v₁v₂∈m₁₂m₃)
rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₁v₂∈m₁₂m₃ =
... | in₁ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) k∉ke₃ =
(v₁ ⊔₂ v₂ , (≈₂-refl , I⊔.union-combines u₁ (I⊔.union-preserves-Unique l₂ l₃ u₃) v₁∈e₁ (I⊔.union-preserves-∈₁ u₂ v₂∈e₂ k∉ke₃)))
... | (_ , (bothᵘ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₁v₂v₃∈m₁₂m₃))
rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₁v₂v₃∈m₁₂m₃ =
... | bothᵘ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) =
(v₁ ⊔₂ (v₂ ⊔₂ v₃) , (⊔₂-assoc v₁ v₂ v₃ , I⊔.union-combines u₁ (I⊔.union-preserves-Unique l₂ l₃ u₃) v₁∈e₁ (I⊔.union-combines u₂ u₃ v₂∈e₂ v₃∈e₃)))
⊔-assoc₂ : (m₁ ⊔ (m₂ ⊔ m₃)) ⊆ ((m₁ ⊔ m₂) ⊔ m₃)
⊔-assoc₂ k v k,v∈m₁m₂₃
with Expr-Provenance k ((` m₁) ∪ ((` m₂) ∪ (` m₃))) (∈-cong proj₁ k,v∈m₁m₂₃)
... | (_ , (in₂ k∉ke₁ (in₂ k∉ke₂ (single {v₃} v₃∈e₃)) , v₃∈m₁m₂₃))
rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₃∈m₁m₂₃ =
with Expr-Provenance-≡ ((` m₁) ∪ ((` m₂) ∪ (` m₃))) k,v∈m₁m₂₃
... | in₂ k∉ke₁ (in₂ k∉ke₂ (single {v₃} v₃∈e₃)) =
(v₃ , (≈₂-refl , I⊔.union-preserves-∈₂ (I⊔.union-preserves-∉ k∉ke₁ k∉ke₂) v₃∈e₃))
... | (_ , (in₂ k∉ke₁ (in₁ (single {v₂} v₂∈e₂) k∉ke₃) , v₂∈m₁m₂₃))
rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₂∈m₁m₂₃ =
... | in₂ k∉ke₁ (in₁ (single {v₂} v₂∈e₂) k∉ke₃) =
(v₂ , (≈₂-refl , I⊔.union-preserves-∈₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) (I⊔.union-preserves-∈₂ k∉ke₁ v₂∈e₂) k∉ke₃))
... | (_ , (in₂ k∉ke₁ (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) , v₂v₃∈m₁m₂₃))
rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₂v₃∈m₁m₂₃ =
... | in₂ k∉ke₁ (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) =
(v₂ ⊔₂ v₃ , (≈₂-refl , I⊔.union-combines (I⊔.union-preserves-Unique l₁ l₂ u₂) u₃ (I⊔.union-preserves-∈₂ k∉ke₁ v₂∈e₂) v₃∈e₃))
... | (_ , (in₁ (single {v₁} v₁∈e₁) k∉ke₂₃ , v₁∈m₁m₂₃))
rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₁∈m₁m₂₃ =
... | in₁ (single {v₁} v₁∈e₁) k∉ke₂₃ =
let (k∉ke₂ , k∉ke₃) = I⊔.∉-union-∉-either {l₁ = l₂} {l₂ = l₃} k∉ke₂₃
in (v₁ , (≈₂-refl , I⊔.union-preserves-∈₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) (I⊔.union-preserves-∈₁ u₁ v₁∈e₁ k∉ke₂) k∉ke₃))
... | (_ , (bothᵘ (single {v₁} v₁∈e₁) (in₂ k∉ke₂ (single {v₃} v₃∈e₃)) , v₁v₃∈m₁m₂₃))
rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₁v₃∈m₁m₂₃ =
... | bothᵘ (single {v₁} v₁∈e₁) (in₂ k∉ke₂ (single {v₃} v₃∈e₃)) =
(v₁ ⊔₂ v₃ , (≈₂-refl , I⊔.union-combines (I⊔.union-preserves-Unique l₁ l₂ u₂) u₃ (I⊔.union-preserves-∈₁ u₁ v₁∈e₁ k∉ke₂) v₃∈e₃))
... | (_ , (bothᵘ (single {v₁} v₁∈e₁) (in₁ (single {v₂} v₂∈e₂) k∉ke₃) , v₁v₂∈m₁m₂₃))
rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₁v₂∈m₁m₂₃ =
... | bothᵘ (single {v₁} v₁∈e₁) (in₁ (single {v₂} v₂∈e₂) k∉ke₃) =
(v₁ ⊔₂ v₂ , (≈₂-refl , I⊔.union-preserves-∈₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) (I⊔.union-combines u₁ u₂ v₁∈e₁ v₂∈e₂) k∉ke₃))
... | (_ , (bothᵘ (single {v₁} v₁∈e₁) (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) , v₁v₂v₃∈m₁m₂₃))
rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₁v₂v₃∈m₁m₂₃ =
... | bothᵘ (single {v₁} v₁∈e₁) (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) =
((v₁ ⊔₂ v₂) ⊔₂ v₃ , (≈₂-sym (⊔₂-assoc v₁ v₂ v₃) , I⊔.union-combines (I⊔.union-preserves-Unique l₁ l₂ u₂) u₃ (I⊔.union-combines u₁ u₂ v₁∈e₁ v₂∈e₂) v₃∈e₃))
⊓-idemp : ∀ (m : Map) → (m ⊓ m) ≈ m
@ -789,10 +767,9 @@ private module I⊓ = ImplInsert _⊓₂_
where
mm-m-⊆ : (m ⊓ m) ⊆ m
mm-m-⊆ k v k,v∈mm
with Expr-Provenance k ((` m) ∩ (` m)) (∈-cong proj₁ k,v∈mm)
... | (_ , (bothⁱ (single {v'} v'∈m) (single {v''} v''∈m) , v'v''∈mm))
rewrite Map-functional {m = m} v'∈m v''∈m
rewrite Map-functional {m = m ⊓ m} k,v∈mm v'v''∈mm =
with Expr-Provenance-≡ ((` m) ∩ (` m)) k,v∈mm
... | bothⁱ (single {v'} v'∈m) (single {v''} v''∈m)
rewrite Map-functional {m = m} v'∈m v''∈m =
(v'' , (⊓₂-idemp v'' , v''∈m))
m-mm-⊆ : m ⊆ (m ⊓ m)
@ -803,9 +780,8 @@ private module I⊓ = ImplInsert _⊓₂_
where
⊓-comm-⊆ : ∀ (m₁ m₂ : Map) → (m₁ ⊓ m₂) ⊆ (m₂ ⊓ m₁)
⊓-comm-⊆ m₁@(l₁ , u₁) m₂@(l₂ , u₂) k v k,v∈m₁m₂
with Expr-Provenance k ((` m₁) ∩ (` m₂)) (∈-cong proj₁ k,v∈m₁m₂)
... | (_ , (bothⁱ {v₁} {v₂} (single v₁∈m₁) (single v₂∈m₂) , v₁v₂∈m₁m₂))
rewrite Map-functional {m = m₁ ⊓ m₂} k,v∈m₁m₂ v₁v₂∈m₁m₂ =
with Expr-Provenance-≡ ((` m₁) ∩ (` m₂)) k,v∈m₁m₂
... | bothⁱ {v₁} {v₂} (single v₁∈m₁) (single v₂∈m₂) =
(v₂ ⊓₂ v₁ , (⊓₂-comm v₁ v₂ , I⊓.intersect-combines u₂ u₁ v₂∈m₂ v₁∈m₁))
⊓-assoc : ∀ (m₁ m₂ m₃ : Map) → ((m₁ ⊓ m₂) ⊓ m₃) ≈ (m₁ ⊓ (m₂ ⊓ m₃))
@ -813,16 +789,14 @@ private module I⊓ = ImplInsert _⊓₂_
where
⊓-assoc₁ : ((m₁ ⊓ m₂) ⊓ m₃) ⊆ (m₁ ⊓ (m₂ ⊓ m₃))
⊓-assoc₁ k v k,v∈m₁₂m₃
with Expr-Provenance k (((` m₁) ∩ (` m₂)) ∩ (` m₃)) (∈-cong proj₁ k,v∈m₁₂m₃)
... | (_ , (bothⁱ (bothⁱ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₁v₂v₃∈m₁₂m₃))
rewrite Map-functional {m = (m₁ ⊓ m₂) ⊓ m₃} k,v∈m₁₂m₃ v₁v₂v₃∈m₁₂m₃ =
with Expr-Provenance-≡ (((` m₁) ∩ (` m₂)) ∩ (` m₃)) k,v∈m₁₂m₃
... | bothⁱ (bothⁱ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) =
(v₁ ⊓₂ (v₂ ⊓₂ v₃) , (⊓₂-assoc v₁ v₂ v₃ , I⊓.intersect-combines u₁ (I⊓.intersect-preserves-Unique {l₂} {l₃} u₃) v₁∈e₁ (I⊓.intersect-combines u₂ u₃ v₂∈e₂ v₃∈e₃)))
⊓-assoc₂ : (m₁ ⊓ (m₂ ⊓ m₃)) ⊆ ((m₁ ⊓ m₂) ⊓ m₃)
⊓-assoc₂ k v k,v∈m₁m₂₃
with Expr-Provenance k ((` m₁) ∩ ((` m₂) ∩ (` m₃))) (∈-cong proj₁ k,v∈m₁m₂₃)
... | (_ , (bothⁱ (single {v₁} v₁∈e₁) (bothⁱ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) , v₁v₂v₃∈m₁m₂₃))
rewrite Map-functional {m = m₁ ⊓ (m₂ ⊓ m₃)} k,v∈m₁m₂₃ v₁v₂v₃∈m₁m₂₃ =
with Expr-Provenance-≡ ((` m₁) ∩ ((` m₂) ∩ (` m₃))) k,v∈m₁m₂₃
... | bothⁱ (single {v₁} v₁∈e₁) (bothⁱ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) =
((v₁ ⊓₂ v₂) ⊓₂ v₃ , (≈₂-sym (⊓₂-assoc v₁ v₂ v₃) , I⊓.intersect-combines (I⊓.intersect-preserves-Unique {l₁} {l₂} u₂) u₃ (I⊓.intersect-combines u₁ u₂ v₁∈e₁ v₂∈e₂) v₃∈e₃))
absorb-⊓-⊔ : ∀ (m₁ m₂ : Map) → (m₁ ⊓ (m₁ ⊔ m₂)) ≈ m₁
@ -830,20 +804,18 @@ absorb-⊓-⊔ m₁@(l₁ , u₁) m₂@(l₂ , u₂) = (absorb-⊓-⊔¹ , absor
where
absorb-⊓-⊔¹ : (m₁ ⊓ (m₁ ⊔ m₂)) ⊆ m₁
absorb-⊓-⊔¹ k v k,v∈m₁m₁₂
with Expr-Provenance k ((` m₁) ∩ ((` m₁) ∪ (` m₂))) (∈-cong proj₁ k,v∈m₁m₁₂)
... | (_ , (bothⁱ (single {v₁} k,v₁∈m₁)
(bothᵘ (single {v₁'} k,v₁'∈m₁)
(single {v₂} v₂∈m₂)) , v₁v₁'v₂∈m₁m₁₂))
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁
rewrite Map-functional {m = m₁ ⊓ (m₁ ⊔ m₂)} k,v∈m₁m₁₂ v₁v₁'v₂∈m₁m₁₂ =
with Expr-Provenance-≡ ((` m₁) ∩ ((` m₁) ∪ (` m₂))) k,v∈m₁m₁₂
... | bothⁱ (single {v₁} k,v₁∈m₁)
(bothᵘ (single {v₁'} k,v₁'∈m₁)
(single {v₂} v₂∈m₂))
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁ =
(v₁' , (absorb-⊓₂-⊔₂ v₁' v₂ , k,v₁'∈m₁))
... | (_ , (bothⁱ (single {v₁} k,v₁∈m₁)
(in₁ (single {v₁'} k,v₁'∈m₁) _) , v₁v₁'∈m₁m₁₂))
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁
rewrite Map-functional {m = m₁ ⊓ (m₁ ⊔ m₂)} k,v∈m₁m₁₂ v₁v₁'∈m₁m₁₂ =
... | bothⁱ (single {v₁} k,v₁∈m₁)
(in₁ (single {v₁'} k,v₁'∈m₁) _)
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁ =
(v₁' , (⊓₂-idemp v₁' , k,v₁'∈m₁))
... | (_ , (bothⁱ (single {v₁} k,v₁∈m₁)
(in₂ k∉m₁ _ ) , _)) = ⊥-elim (k∉m₁ (∈-cong proj₁ k,v₁∈m₁))
... | bothⁱ (single {v₁} k,v₁∈m₁)
(in₂ k∉m₁ _ ) = ⊥-elim (k∉m₁ (∈-cong proj₁ k,v₁∈m₁))
absorb-⊓-⊔² : m₁ ⊆ (m₁ ⊓ (m₁ ⊔ m₂))
absorb-⊓-⊔² k v k,v∈m₁
@ -858,18 +830,16 @@ absorb-⊔-⊓ m₁@(l₁ , u₁) m₂@(l₂ , u₂) = (absorb-⊔-⊓¹ , absor
where
absorb-⊔-⊓¹ : (m₁ ⊔ (m₁ ⊓ m₂)) ⊆ m₁
absorb-⊔-⊓¹ k v k,v∈m₁m₁₂
with Expr-Provenance k ((` m₁) ∪ ((` m₁) ∩ (` m₂))) (∈-cong proj₁ k,v∈m₁m₁₂)
... | (_ , (bothᵘ (single {v₁} k,v₁∈m₁)
(bothⁱ (single {v₁'} k,v₁'∈m₁)
(single {v₂} k,v₂∈m₂)) , v₁v₁'v₂∈m₁m₁₂))
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁
rewrite Map-functional {m = m₁ ⊔ (m₁ ⊓ m₂)} k,v∈m₁m₁₂ v₁v₁'v₂∈m₁m₁₂ =
with Expr-Provenance-≡ ((` m₁) ∪ ((` m₁) ∩ (` m₂))) k,v∈m₁m₁₂
... | bothᵘ (single {v₁} k,v₁∈m₁)
(bothⁱ (single {v₁'} k,v₁'∈m₁)
(single {v₂} k,v₂∈m₂))
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁ =
(v₁' , (absorb-⊔₂-⊓₂ v₁' v₂ , k,v₁'∈m₁))
... | (_ , (in₁ (single {v₁} k,v₁∈m₁) k∉km₁₂ , k,v₁∈m₁m₁₂))
rewrite Map-functional {m = m₁ ⊔ (m₁ ⊓ m₂)} k,v∈m₁m₁₂ k,v₁∈m₁m₁₂ =
... | in₁ (single {v₁} k,v₁∈m₁) k∉km₁₂ =
(v₁ , (≈₂-refl , k,v₁∈m₁))
... | (_ , (in₂ k∉km₁ (bothⁱ (single {v₁'} k,v₁'∈m₁)
(single {v₂} k,v₂∈m₂)) , _)) =
... | in₂ k∉km₁ (bothⁱ (single {v₁'} k,v₁'∈m₁)
(single {v₂} k,v₂∈m₂)) =
⊥-elim (k∉km₁ (∈-cong proj₁ k,v₁'∈m₁))
absorb-⊔-⊓² : m₁ ⊆ (m₁ ⊔ (m₁ ⊓ m₂))
@ -1044,7 +1014,7 @@ module _ {l} {L : Set l}
f'l₁f'l₂⊆f'l₂ : ((f' l₁) ⊔ (f' l₂)) ⊆ f' l₂
f'l₁f'l₂⊆f'l₂ k v k,v∈f'l₁f'l₂
with Expr-Provenance-≡ k v ((` (f' l₁)) ∪ (` (f' l₂))) k,v∈f'l₁f'l₂
with Expr-Provenance-≡ ((` (f' l₁)) ∪ (` (f' l₂))) k,v∈f'l₁f'l₂
... | in₁ (single k,v∈f'l₁) k∉kf'l₂ =
let
k∈kfl₁ = updating-via-∈k-backward (f l₁) ks (updater l₁) (forget {m = f' l₁} k,v∈f'l₁)
@ -1077,7 +1047,7 @@ module _ {l} {L : Set l}
with k∈kfl₂ ← updating-via-∈k-backward (f l₂) ks (updater l₂) (forget {m = f' l₂} k,v∈f'l₂)
with (v' , k,v'∈fl₂) ← locate {m = f l₂} k∈kfl₂
with (v'' , (v'≈v'' , k,v''∈fl₁fl₂)) ← fl₂⊆fl₁fl₂ k v' k,v'∈fl₂
with Expr-Provenance-≡ k v'' ((` (f l₁)) ∪ (` (f l₂))) k,v''∈fl₁fl₂
with Expr-Provenance-≡ ((` (f l₁)) ∪ (` (f l₂))) k,v''∈fl₁fl₂
... | in₁ (single k,v''∈fl₁) k∉kfl₂ = ⊥-elim (k∉kfl₂ k∈kfl₂)
... | in₂ k∉kfl₁ (single k,v''∈fl₂) =
let