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

Prove associativity of maps (in one direction)

Browse Source
This commit is contained in:
Danila Fedorin 2023-07-30 19:08:51 -07:00
parent 1e4e8000cf
commit 2c839db924
1 changed files with 60 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

75
Map.agda
View File

@ -182,6 +182,42 @@ private module ImplInsert (f : B → B → B) where
... | yes k≡k' = absurd (k∉kl₁ (here k≡k'))
... | no k≢k' = insert-preserves-∉k k≢k' (union-preserves-∉ (λ k∈kxs₁ → k∉kl₁ (there k∈kxs₁)) k∉kl₂)
insert-preserves-∈k : ∀ {k k' : A} {v' : B} {l : List (A × B)} →
k ∈k l → k ∈k insert k' v' l
insert-preserves-∈k {k} {k'} {v'} {(k'' , v'') ∷ xs} (here k≡k'')
with (≡-dec-A k' k'')
... | yes _ = here k≡k''
... | no _ = here k≡k''
insert-preserves-∈k {k} {k'} {v'} {(k'' , v'') ∷ xs} (there k∈kxs)
with (≡-dec-A k' k'')
... | yes _ = there k∈kxs
... | no _ = there (insert-preserves-∈k k∈kxs)
union-preserves-∈k₁ : ∀ {k : A} {l₁ l₂ : List (A × B)} →
k ∈k l₁ → k ∈k (union l₁ l₂)
union-preserves-∈k₁ {k} {(k' , v') ∷ xs} {l₂} (here k≡k')
with ∈k-dec k (union xs l₂)
... | yes k∈kxsl₂ = insert-preserves-∈k k∈kxsl₂
... | no k∉kxsl₂ rewrite k≡k' = ∈-cong proj₁ (insert-fresh k∉kxsl₂)
union-preserves-∈k₁ {k} {(k' , v') ∷ xs} {l₂} (there k∈kxs) =
insert-preserves-∈k (union-preserves-∈k₁ k∈kxs)
union-preserves-∈k₂ : ∀ {k : A} {l₁ l₂ : List (A × B)} →
k ∈k l₂ → k ∈k (union l₁ l₂)
union-preserves-∈k₂ {k} {[]} {l₂} k∈kl₂ = k∈kl₂
union-preserves-∈k₂ {k} {(k' , v') ∷ xs} {l₂} k∈kl₂ =
insert-preserves-∈k (union-preserves-∈k₂ {l₁ = xs} k∈kl₂)
∉-union-∉-either : ∀ {k : A} {l₁ l₂ : List (A × B)} →
¬ k ∈k union l₁ l₂ → ¬ k ∈k l₁ × ¬ k ∈k l₂
∉-union-∉-either {k} {l₁} {l₂} k∉l₁l₂
with ∈k-dec k l₁
... | yes k∈kl₁ = absurd (k∉l₁l₂ (union-preserves-∈k₁ k∈kl₁))
... | no k∉kl₁ with ∈k-dec k l₂
... | yes k∈kl₂ = absurd (k∉l₁l₂ (union-preserves-∈k₂ {l₁ = l₁} k∈kl₂))
... | no k∉kl₂ = (k∉kl₁ , k∉kl₂)
insert-preserves-∈ : ∀ {k k' : A} {v v' : B} {l : List (A × B)} →
¬ k ≡ k' → (k , v) ∈ l → (k , v) ∈ insert k' v' l
insert-preserves-∈ {k} {k'} {l = x ∷ xs} k≢k' (here k,v=x)
@ -193,12 +229,6 @@ private module ImplInsert (f : B → B → B) where
... | yes _ = there k,v∈xs
... | no _ = there (insert-preserves-∈ k≢k' k,v∈xs)
insert-preserves-∈k : ∀ {k k' : A} {v' : B} {l : List (A × B)} →
¬ k ≡ k' → k ∈k l → k ∈k insert k' v' l
insert-preserves-∈k k≢k' k∈kl =
let (v , k,v∈l) = locate k∈kl
in ∈-cong proj₁ (insert-preserves-∈ k≢k' k,v∈l)
union-preserves-∈₂ : ∀ {k : A} {v : B} {l₁ l₂ : List (A × B)} →
¬ k ∈k l₁ → (k , v) ∈ l₂ → (k , v) ∈ union l₁ l₂
union-preserves-∈₂ {l₁ = []} _ k,v∈l₂ = k,v∈l₂
@ -314,7 +344,7 @@ module _ (_≈_ : B → B → Set b) where
module _ (f : B → 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
(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₂ = (union-comm-subset m₁ m₂ , union-comm-subset m₂ m₁)
where
@ -332,12 +362,27 @@ module _ (f : B → B → B) where
(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₃
union-assoc₁ m₁@(l₁ , u₁) m₂@(l₂ , u₂) m₃@(l₃ , u₃) 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₃)) = {!!}
... | (_ , (in₂ k∉ke₁₂ (single {v₃} v₃∈e₃) , v₃∈m₁₂m₃))
rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₃∈m₁₂m₃ =
let (k∉ke₁ , k∉ke₂) = ImplInsert.∉-union-∉-either f {l₁ = l₁} {l₂ = l₂} k∉ke₁₂
in (v₃ , (refl , ImplInsert.union-preserves-∈₂ f k∉ke₁ (ImplInsert.union-preserves-∈₂ f k∉ke₂ v₃∈e₃)))
... | (_ , (in₁ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) k∉ke₃ , v₂∈m₁₂m₃))
rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₂∈m₁₂m₃ =
(v₂ , (refl , ImplInsert.union-preserves-∈₂ f k∉ke₁ (ImplInsert.union-preserves-∈₁ f 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 = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₂v₃∈m₁₂m₃ =
(f v₂ v₃ , (refl , ImplInsert.union-preserves-∈₂ f k∉ke₁ (ImplInsert.union-combines f u₂ u₃ v₂∈e₂ v₃∈e₃)))
... | (_ , (in₁ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) k∉ke₃ , v₁∈m₁₂m₃))
rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₁∈m₁₂m₃ =
(v₁ , (refl , ImplInsert.union-preserves-∈₁ f u₁ v₁∈e₁ (ImplInsert.union-preserves-∉ f k∉ke₂ k∉ke₃)))
... | (_ , (bothᵘ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) (single {v₃} v₃∈e₃) , v₁v₃∈m₁₂m₃))
rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₁v₃∈m₁₂m₃ =
(f v₁ v₃ , (refl , ImplInsert.union-combines f u₁ (ImplInsert.union-preserves-Unique f l₂ l₃ u₃) v₁∈e₁ (ImplInsert.union-preserves-∈₂ f k∉ke₂ v₃∈e₃)))
... | (_ , (in₁ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) k∉ke₃), v₁v₂∈m₁₂m₃)
rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₁v₂∈m₁₂m₃ =
(f v₁ v₂ , (refl , ImplInsert.union-combines f u₁ (ImplInsert.union-preserves-Unique f l₂ l₃ u₃) v₁∈e₁ (ImplInsert.union-preserves-∈₁ f 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 = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₁v₂v₃∈m₁₂m₃ =
(f v₁ (f v₂ v₃) , (f-assoc v₁ v₂ v₃ , ImplInsert.union-combines f u₁ (ImplInsert.union-preserves-Unique f l₂ l₃ u₃) v₁∈e₁ (ImplInsert.union-combines f u₂ u₃ v₂∈e₂ v₃∈e₃)))