From 8288632bf61de4d27ae57700a5e45e04d17c2a6a Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Tue, 26 Jul 2022 20:22:59 +0200
Subject: [PATCH] Rename lookup_union_l' to lookup_union_l and add
 lookup_union_l dual to lookup_union_r

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3a7511d5..9e7a16e7 100644
--- a/CHANGELOG.md
+++ b/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
 ```
 
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 20a8857d..6331dde7 100644
--- a/theories/fin_maps.v
+++ b/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 :
-- 
GitLab