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

Rename union-preserves to properly match what's being preserved

Browse Source
This commit is contained in:
Danila Fedorin 2023-07-30 17:57:06 -07:00
parent 70b85c99cc
commit 1e4e8000cf
1 changed files with 26 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
Map.agda
View File

@ -199,25 +199,25 @@ private module ImplInsert (f : B → B → B) where
let (v , k,v∈l) = locate k∈kl let (v , k,v∈l) = locate k∈kl
in ∈-cong proj₁ (insert-preserves-∈ k≢k' k,v∈l) in ∈-cong proj₁ (insert-preserves-∈ k≢k' k,v∈l)
union-preserves-∈₁ : ∀ {k : A} {v : B} {l₁ l₂ : List (A × B)} → union-preserves-∈₂ : ∀ {k : A} {v : B} {l₁ l₂ : List (A × B)} →
¬ k ∈k l₁ → (k , v) ∈ l₂ → (k , v) ∈ union l₁ l₂ ¬ k ∈k l₁ → (k , v) ∈ l₂ → (k , v) ∈ union l₁ l₂
union-preserves-∈₁ {l₁ = []} _ k,v∈l₂ = k,v∈l₂ union-preserves-∈₂ {l₁ = []} _ k,v∈l₂ = k,v∈l₂
union-preserves-∈₁ {l₁ = (k' , v') ∷ xs₁} k∉kl₁ k,v∈l₂ = union-preserves-∈₂ {l₁ = (k' , v') ∷ xs₁} k∉kl₁ k,v∈l₂ =
let recursion = union-preserves-∈₁ (λ k∈xs₁ → k∉kl₁ (there k∈xs₁)) k,v∈l₂ let recursion = union-preserves-∈₂ (λ k∈xs₁ → k∉kl₁ (there k∈xs₁)) k,v∈l₂
in insert-preserves-∈ (λ k≡k' → k∉kl₁ (here k≡k')) recursion in insert-preserves-∈ (λ k≡k' → k∉kl₁ (here k≡k')) recursion
union-preserves-∈₂ : ∀ {k : A} {v : B} {l₁ l₂ : List (A × B)} → union-preserves-∈₁ : ∀ {k : A} {v : B} {l₁ l₂ : List (A × B)} →
Unique (keys l₁) → (k , v) ∈ l₁ → ¬ k ∈k l₂ → (k , v) ∈ union l₁ l₂ Unique (keys l₁) → (k , v) ∈ l₁ → ¬ k ∈k l₂ → (k , v) ∈ union l₁ l₂
union-preserves-∈₂ {k} {v} {(k' , v') ∷ xs₁} (push k'≢xs₁ uxs₁) (there k,v∈xs₁) k∉kl₂ = union-preserves-∈₁ {k} {v} {(k' , v') ∷ xs₁} (push k'≢xs₁ uxs₁) (there k,v∈xs₁) k∉kl₂ =
insert-preserves-∈ k≢k' k,v∈mxs₁l insert-preserves-∈ k≢k' k,v∈mxs₁l
where where
k,v∈mxs₁l = union-preserves-∈₂ uxs₁ k,v∈xs₁ k∉kl₂ k,v∈mxs₁l = union-preserves-∈₁ uxs₁ k,v∈xs₁ k∉kl₂
k≢k' : ¬ k ≡ k' k≢k' : ¬ k ≡ k'
k≢k' with ≡-dec-A k k' k≢k' with ≡-dec-A k k'
... | yes k≡k' rewrite k≡k' = absurd (All¬-¬Any k'≢xs₁ (∈-cong proj₁ k,v∈xs₁)) ... | yes k≡k' rewrite k≡k' = absurd (All¬-¬Any k'≢xs₁ (∈-cong proj₁ k,v∈xs₁))
... | no k≢k' = k≢k' ... | no k≢k' = k≢k'
union-preserves-∈₂ {l₁ = (k' , v') ∷ xs₁} (push k'≢xs₁ uxs₁) (here k,v≡k',v') k∉kl₂ union-preserves-∈₁ {l₁ = (k' , v') ∷ xs₁} (push k'≢xs₁ uxs₁) (here k,v≡k',v') k∉kl₂
rewrite cong proj₁ k,v≡k',v' rewrite cong proj₂ k,v≡k',v' = rewrite cong proj₁ k,v≡k',v' rewrite cong proj₂ k,v≡k',v' =
insert-fresh (union-preserves-∉ (All¬-¬Any k'≢xs₁) k∉kl₂) insert-fresh (union-preserves-∉ (All¬-¬Any k'≢xs₁) k∉kl₂)
@ -238,7 +238,7 @@ private module ImplInsert (f : B → B → B) where
(k , v₁) ∈ l₁ → (k , v₂) ∈ l₂ → (k , f v₁ v₂) ∈ union l₁ l₂ (k , v₁) ∈ l₁ → (k , v₂) ∈ l₂ → (k , f v₁ v₂) ∈ union l₁ l₂
union-combines {l₁ = (k' , v) ∷ xs₁} {l₂} (push k'≢xs₁ uxs₁) ul₂ (here k,v₁≡k',v) k,v₂∈l₂ union-combines {l₁ = (k' , v) ∷ xs₁} {l₂} (push k'≢xs₁ uxs₁) ul₂ (here k,v₁≡k',v) k,v₂∈l₂
rewrite cong proj₁ (sym (k,v₁≡k',v)) rewrite cong proj₂ (sym (k,v₁≡k',v)) = rewrite cong proj₁ (sym (k,v₁≡k',v)) rewrite cong proj₂ (sym (k,v₁≡k',v)) =
insert-combines (union-preserves-Unique xs₁ l₂ ul₂) (union-preserves-∈₁ (All¬-¬Any k'≢xs₁) k,v₂∈l₂) insert-combines (union-preserves-Unique xs₁ l₂ ul₂) (union-preserves-∈₂ (All¬-¬Any k'≢xs₁) k,v₂∈l₂)
union-combines {k} {l₁ = (k' , v) ∷ xs₁} (push k'≢xs₁ uxs₁) ul₂ (there k,v₁∈xs₁) k,v₂∈l₂ = union-combines {k} {l₁ = (k' , v) ∷ xs₁} (push k'≢xs₁ uxs₁) ul₂ (there k,v₁∈xs₁) k,v₂∈l₂ =
insert-preserves-∈ k≢k' (union-combines uxs₁ ul₂ k,v₁∈xs₁ k,v₂∈l₂) insert-preserves-∈ k≢k' (union-combines uxs₁ ul₂ k,v₁∈xs₁ k,v₂∈l₂)
where where
@ -296,10 +296,10 @@ module _ (f : B → B → B) where
in (f v₁ v₂ , (bothᵘ g₁ g₂ , union-combines (proj₂ ⟦ e₁ ⟧) (proj₂ ⟦ e₂ ⟧) k,v₁∈e₁ k,v₂∈e₂)) in (f v₁ v₂ , (bothᵘ g₁ g₂ , union-combines (proj₂ ⟦ e₁ ⟧) (proj₂ ⟦ e₂ ⟧) k,v₁∈e₁ k,v₂∈e₂))
... | yes k∈ke₁ | no k∉ke₂ = ... | yes k∈ke₁ | no k∉ke₂ =
let (v₁ , (g₁ , k,v₁∈e₁)) = Expr-Provenance k e₁ k∈ke₁ let (v₁ , (g₁ , k,v₁∈e₁)) = Expr-Provenance k e₁ k∈ke₁
in (v₁ , (in₁ g₁ k∉ke₂ , union-preserves-∈₂ (proj₂ ⟦ e₁ ⟧) k,v₁∈e₁ k∉ke₂)) in (v₁ , (in₁ g₁ k∉ke₂ , union-preserves-∈₁ (proj₂ ⟦ e₁ ⟧) k,v₁∈e₁ k∉ke₂))
... | no k∉ke₁ | yes k∈ke₂ = ... | no k∉ke₁ | yes k∈ke₂ =
let (v₂ , (g₂ , k,v₂∈e₂)) = Expr-Provenance k e₂ k∈ke₂ let (v₂ , (g₂ , k,v₂∈e₂)) = Expr-Provenance k e₂ k∈ke₂
in (v₂ , (in₂ k∉ke₁ g₂ , union-preserves-∈₁ k∉ke₁ k,v₂∈e₂)) in (v₂ , (in₂ k∉ke₁ g₂ , union-preserves-∈₂ k∉ke₁ k,v₂∈e₂))
... | no k∉ke₁ | no k∉ke₂ = absurd (union-preserves-∉ k∉ke₁ k∉ke₂ k∈ke₁e₂) ... | no k∉ke₁ | no k∉ke₂ = absurd (union-preserves-∉ k∉ke₁ k∉ke₂ k∈ke₁e₂)
@ -313,7 +313,8 @@ module _ (_≈_ : B → B → Set b) where
lift m₁ m₂ = subset m₁ m₂ × subset m₂ m₁ lift m₁ m₂ = subset m₁ m₂ × subset m₂ m₁
module _ (f : B → B → B) where module _ (f : B → B → B) where
module _ (f-comm : ∀ (b₁ b₂ : B) → f b₁ b₂ ≡ f b₂ b₁) where module _ (f-comm : ∀ (b₁ b₂ : B) → f b₁ b₂ ≡ f b₂ b₁)
(f-assoc : ∀ (b₁ b₂ b₃ : B) → f (f b₁ b₂) b₃ ≡ f b₁ (f b₁ b₂)) where
union-comm : ∀ (m₁ m₂ : Map) → lift (_≡_) (union f m₁ m₂) (union f m₂ m₁) union-comm : ∀ (m₁ m₂ : Map) → lift (_≡_) (union f m₁ m₂) (union f m₂ m₁)
union-comm m₁ m₂ = (union-comm-subset m₁ m₂ , union-comm-subset m₂ m₁) union-comm m₁ m₂ = (union-comm-subset m₁ m₂ , union-comm-subset m₂ m₁)
where where
@ -325,7 +326,18 @@ module _ (f : B → B → B) where
(f v₂ v₁ , (f-comm v₁ v₂ , ImplInsert.union-combines f u₂ u₁ v₂∈m₂ v₁∈m₁)) (f v₂ v₁ , (f-comm v₁ v₂ , ImplInsert.union-combines f u₂ u₁ v₂∈m₂ v₁∈m₁))
... | (_ , (in₁ {v₁} (single v₁∈m₁) k∉km₂ , v₁∈m₁m₂)) ... | (_ , (in₁ {v₁} (single v₁∈m₁) k∉km₂ , v₁∈m₁m₂))
rewrite Map-functional {m = union f m₁ m₂} k,v∈m₁m₂ v₁∈m₁m₂ = rewrite Map-functional {m = union f m₁ m₂} k,v∈m₁m₂ v₁∈m₁m₂ =
(v₁ , (refl , ImplInsert.union-preserves-∈₁ f k∉km₂ v₁∈m₁)) (v₁ , (refl , ImplInsert.union-preserves-∈₂ f k∉km₂ v₁∈m₁))
... | (_ , (in₂ {v₂} k∉km₁ (single v₂∈m₂) , v₂∈m₁m₂)) ... | (_ , (in₂ {v₂} k∉km₁ (single v₂∈m₂) , v₂∈m₁m₂))
rewrite Map-functional {m = union f m₁ m₂} k,v∈m₁m₂ v₂∈m₁m₂ = rewrite Map-functional {m = union f m₁ m₂} k,v∈m₁m₂ v₂∈m₁m₂ =
(v₂ , (refl , ImplInsert.union-preserves-∈₂ f u₂ v₂∈m₂ k∉km₁)) (v₂ , (refl , ImplInsert.union-preserves-∈₁ f u₂ v₂∈m₂ k∉km₁))
union-assoc₁ : ∀ (m₁ m₂ m₃ : Map) → subset (_≡_) (union f (union f m₁ m₂) m₃) (union f m₁ (union f m₂ m₃))
union-assoc₁ m₁ m₂ m₃ k v k,v∈m₁₂m₃
with Expr-Provenance f k (((` m₁) ∪ (` m₂)) ∪ (` m₃)) (∈-cong proj₁ k,v∈m₁₂m₃)
... | (_ , (in₂ k∉ke₁₂ (single {v₃} v₃∈e₃) , v₃∈m₁₂m₃)) = {!!}
... | (_ , (in₁ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) k∉ke3 , v₂∈m₁₂m₃)) = {!!}
... | (_ , (bothᵘ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₂v₃∈m₁₂m₃)) = {!!}
... | (_ , (in₁ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) k∉ke₃ , v₁∈m₁₂m₃)) = {!!}
... | (_ , (bothᵘ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) (single {v₃} v₃∈e₃) , v₁v₃∈m₁₂m₃)) = {!!}
... | (_ , (in₁ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) k∉ke₃), v₁v₂∈m₁₂m₃) = {!!}
... | (_ , (bothᵘ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₁v₂v₃∈m₁₂m₃)) = {!!}