Commit e22e4a76 authored by Simon Friis Vindum's avatar Simon Friis Vindum
Browse files

Add changelog entry and make small tweaks

parent 28f8140d
Pipeline #49247 passed with stage
in 5 minutes and 13 seconds
......@@ -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`):
......@@ -1387,8 +1387,7 @@ Section map_filter_misc.
apply option_guard_True, Hi, Hlook.
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) :
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment