From 34203840c84f34a128bdbb6a8fad57b04abf0625 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 7 Mar 2024 19:59:14 -0800 Subject: [PATCH] Use the new provenance function to clean up some proofs Signed-off-by: Danila Fedorin --- Lattice/FiniteValueMap.agda | 10 +-- Lattice/Map.agda | 154 +++++++++++++++--------------------- 2 files changed, 67 insertions(+), 97 deletions(-) diff --git a/Lattice/FiniteValueMap.agda b/Lattice/FiniteValueMap.agda index 9d9b9ca..db6b45f 100644 --- a/Lattice/FiniteValueMap.agda +++ b/Lattice/FiniteValueMap.agda @@ -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)) → diff --git a/Lattice/Map.agda b/Lattice/Map.agda index 2fdfde7..42d91e7 100644 --- a/Lattice/Map.agda +++ b/Lattice/Map.agda @@ -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