From d786e6bf48e10b1a9c1c0791209e6e697023a0c4 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 30 Jul 2023 14:16:35 -0700 Subject: [PATCH] Eschew proof-by-symmetry --- Map.agda | 32 ++++++++++++-------------------- 1 file changed, 12 insertions(+), 20 deletions(-) diff --git a/Map.agda b/Map.agda index ba47d91..952ce67 100644 --- a/Map.agda +++ b/Map.agda @@ -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₁) - 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₁) - 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₁)) + 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₁ , (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₂ , (refl , ImplInsert.merge-preserves-∈₂ f u₂ v₂∈m₂ k∉km₁))