Merge branch 'ci/msammler/lookup_union_l' into 'master'

Add lookup_union_l'

See merge request iris/stdpp!395

CHANGELOG.md

@@ -29,13 +29,17 @@ Coq 8.11 is no longer supported.
 - Flip direction of `map_disjoint_fmap`.
 - Add `map_agree` as a weaker version of `##ₘ` which requires the maps to agree
   on keys contained in both maps. (by Michael Sammler)
+- Rename `lookup_union_l` → `lookup_union_l'` and add `lookup_union_l`
+  as the dual to `lookup_union_r`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
 ```
 sed -i -E -f- $(find theories -name "*.v") <<EOF
 s/\bmap_disjoint_subseteq\b/kmap_subseteq/g
 s/\bmap_disjoint_subset\b/kmap_subset/g
+s/\blookup_union_l\b/lookup_union_l'/g
 EOF
 ```
 

theories/fin_maps.v

@@ -2261,6 +2261,9 @@ Lemma lookup_union_r {A} (m1 m2 : M A) i :
   m1 !! i = None → (m1 ∪ m2) !! i = m2 !! i.
 Proof. intros Hi. by rewrite lookup_union, Hi, (left_id_L _ _).  Qed.
 Lemma lookup_union_l {A} (m1 m2 : M A) i :
+  m2 !! i = None → (m1 ∪ m2) !! i = m1 !! i.
+Proof. intros Hi. rewrite lookup_union, Hi. by destruct (m1 !! i). Qed.
+Lemma lookup_union_l' {A} (m1 m2 : M A) i :
   is_Some (m1 !! i) → (m1 ∪ m2) !! i = m1 !! i.
 Proof. intros [x Hi]. rewrite lookup_union, Hi. by destruct (m2 !! i). Qed.
 Lemma lookup_union_Some_raw {A} (m1 m2 : M A) i x :