From 9cbafb674abd6efb154559eb603b9599ae94c5ec Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 12 Dec 2018 21:20:41 +0100
Subject: [PATCH] Inline equality premise in `map_insert_zip_with`.

Two reasons:

- The equality makes it very hard to use the lemma with `rewrite`.
- The version for lists `insert_zip_with` does not have the equality either.
---
 theories/fin_maps.v | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 5983b55a..88a5628c 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1259,13 +1259,9 @@ Lemma map_zip_with_empty {A B C} (f : A → B → C) :
   map_zip_with f (∅ : M A) (∅ : M B) = ∅.
 Proof. unfold map_zip_with. by rewrite merge_empty by done. Qed.
 
-Lemma map_insert_zip_with {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i x y z :
-  f y z = x →
-  <[i:=x]>(map_zip_with f m1 m2) = map_zip_with f (<[i:=y]>m1) (<[i:=z]>m2).
-Proof.
-  intros Hf. unfold map_zip_with.
-  erewrite insert_merge; [ auto | by compute | by rewrite Hf ].
-Qed.
+Lemma map_insert_zip_with {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i y z :
+  <[i:=f y z]>(map_zip_with f m1 m2) = map_zip_with f (<[i:=y]>m1) (<[i:=z]>m2).
+Proof. unfold map_zip_with. by erewrite insert_merge by done. Qed.
 
 Lemma map_zip_with_fmap {A' A B' B C} (f : A → B → C)
     (g1 : A' → A) (g2 : B' → B) (m1 : M A') (m2 : M B') :
-- 
GitLab