From e22e4a76ec94e96a88b2ec79e004ce3d10351cdc Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Fri, 25 Jun 2021 07:55:05 +0200
Subject: [PATCH] Add changelog entry and make small tweaks

---
 CHANGELOG.md        | 5 ++++-
 theories/fin_maps.v | 7 +++----
 2 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a28b5914..38aa64dd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -97,7 +97,10 @@ API-breaking change is listed.
     representations as lists.
 - Remove explicit equality from cross split lemmas so that they become easier
   to use in forward-style proofs.
-
+- Add lemmas for finite maps: `dom_map_zip_with`, `dom_map_zip_with_L`,
+  `map_filter_id`, `map_filter_subseteq`, and `map_lookup_zip_Some`.
+- Add lemmas for sets: `elem_of_weaken` and `not_elem_of_weaken`.
+ 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
 ```
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 629c7498..2e6d663e 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1387,8 +1387,7 @@ Section map_filter_misc.
     apply option_guard_True, Hi, Hlook.
   Qed.
 
-  Lemma map_filter_subseteq f `{∀ (x : (K *A)), Decision (f x)} m :
-    filter f m ⊆ m.
+  Lemma map_filter_subseteq m : filter P m ⊆ m.
   Proof. apply map_subseteq_spec, map_filter_lookup_Some_1_1. Qed.
 End map_filter_misc.
 
@@ -1630,8 +1629,8 @@ Lemma map_lookup_zip_with_None {A B C} (f : A → B → C) (m1 : M A) (m2 : M B)
   map_zip_with f m1 m2 !! i = None ↔ m1 !! i = None ∨ m2 !! i = None.
 Proof. rewrite map_lookup_zip_with. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
 
-Lemma map_lookup_zip_Some {A B} (m1 : M A) (m2 : M B) l p :
-  (map_zip m1 m2) !! l = Some p ↔ m1 !! l = Some p.1 ∧ m2 !! l = Some p.2.
+Lemma map_lookup_zip_Some {A B} (m1 : M A) (m2 : M B) i p :
+  map_zip m1 m2 !! i = Some p ↔ m1 !! i = Some p.1 ∧ m2 !! i = Some p.2.
 Proof. rewrite map_lookup_zip_with_Some. destruct p. naive_solver. Qed.
 
 Lemma map_zip_with_empty {A B C} (f : A → B → C) :
-- 
GitLab