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

Eschew proof-by-symmetry

Browse Source
This commit is contained in:
Danila Fedorin 2023-07-30 14:16:35 -07:00
parent af0066eaa7
commit d786e6bf48
1 changed files with 12 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
Map.agda
View File

@ -318,23 +318,15 @@ module _ (f : B → B → B) where
merge-comm m₁ m₂ = (merge-comm-subset m₁ m₂ , merge-comm-subset m₂ m₁)
where
merge-comm-subset : ∀ (m₁ m₂ : Map) → subset (_≡_) (merge f m₁ m₂) (merge f m₂ m₁)
merge-comm-subset m₁ m₂ k v k,v∈m₁m₂ with ∈k-dec k (proj₁ (merge f m₂ m₁) )
... | no k∉km₂m₁ = {!!}
... | yes k∈km₂m₁ with merge-provenance f m₁ m₂ k (∈-cong proj₁ k,v∈m₁m₂) | merge-provenance f m₂ m₁ k k∈km₂m₁
... | (both v₁ v₂ v₁∈m₁ v₂∈m₂ , v₁v₂∈m₁m₂) | (both v₂' v₁' v₂'∈m₂ v₁'∈m₁ , v₂'v₁'∈m₂m₁)
rewrite Map-functional {m = merge f m₁ m₂} k,v∈m₁m₂ v₁v₂∈m₁m₂
rewrite Map-functional {m = m₁} v₁∈m₁ v₁'∈m₁
rewrite Map-functional {m = m₂} v₂∈m₂ v₂'∈m₂ = (f v₂' v₁' , (f-comm v₁' v₂' , v₂'v₁'∈m₂m₁))
... | (in₁ v₁ v₁∈m₁ _ , v₁∈m₁m₂) | (in₂ v₁' _ v₁'∈m₁ , v₁'∈m₂m₁)
merge-comm-subset m₁@(l₁ , u₁) m₂@(l₂ , u₂) k v k,v∈m₁m₂
with merge-provenance f m₁ m₂ k (∈-cong proj₁ k,v∈m₁m₂)
... | (both v₁ v₂ v₁∈m₁ v₂∈m₂ , v₁v₂∈m₁m₂)
rewrite Map-functional {m = merge f m₁ m₂} k,v∈m₁m₂ v₁v₂∈m₁m₂ =
(f v₂ v₁ , (f-comm v₁ v₂ , ImplInsert.merge-combines f u₂ u₁ v₂∈m₂ v₁∈m₁))
... | (in₁ v₁ v₁∈m₁ k∉km₂ , v₁∈m₁m₂)
rewrite Map-functional {m = merge f m₁ m₂} k,v∈m₁m₂ v₁∈m₁m₂ =
(v₁' , (Map-functional {m = m₁} v₁∈m₁ v₁'∈m₁ , v₁'∈m₂m₁))
... | (in₂ v₂ _ v₂∈m₂ , v₂∈m₁m₂) | (in₁ v₂' v₂'∈m₂ _ , v₂'∈m₂m₁)
(v₁ , (refl , ImplInsert.merge-preserves-∈₁ f k∉km₂ v₁∈m₁))
... | (in₂ v₂ k∉km₁ v₂∈m₂ , v₂∈m₁m₂)
rewrite Map-functional {m = merge f m₁ m₂} k,v∈m₁m₂ v₂∈m₁m₂ =
(v₂' , (Map-functional {m = m₂} v₂∈m₂ v₂'∈m₂ , v₂'∈m₂m₁))
-- The rest of the cases are to be dismissed.
... | (both v₁ v₂ v₁∈m₁ v₂∈m₂ , _) | (in₁ v₂' v₂'∈m₂ k∉km₁ , _) = absurd (k∉km₁ (∈-cong proj₁ v₁∈m₁))
... | (both v₁ v₂ v₁∈m₁ v₂∈m₂ , _) | (in₂ v₁' k∉km₂ v₁'∈m₁ , _) = absurd (k∉km₂ (∈-cong proj₁ v₂∈m₂))
... | (in₁ v₁ v₁∈m₁ k∉km₂ , _) | (both v₂' v₁' v₂'∈m₂ v₁'∈m₁ , _) = absurd (k∉km₂ (∈-cong proj₁ v₂'∈m₂))
... | (in₁ v₁ v₁∈m₁ k∉km₂ , _) | (in₁ v₂' v₂'∈m₂ k∉km₁ , _) = absurd (k∉km₂ (∈-cong proj₁ v₂'∈m₂))
... | (in₂ v₂ k∉km₁ v₂∈m₂ , v₂∈m₁m₂) | (both v₂' v₁' v₂'∈m₂ v₁'∈m₁ , _) = absurd (k∉km₁ (∈-cong proj₁ v₁'∈m₁))
... | (in₂ v₂ k∉km₁ v₂∈m₂ , v₂∈m₁m₂) | (in₂ v₁' _ v₁'∈m₁ , v₁'∈m₂m₁) = absurd (k∉km₁ (∈-cong proj₁ v₁'∈m₁))
(v₂ , (refl , ImplInsert.merge-preserves-∈₂ f u₂ v₂∈m₂ k∉km₁))