From 8743eb663a0e4f7957887f9eb5180841d77f0516 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 4 Jan 2021 23:30:26 +0100
Subject: [PATCH 01/13] Add lemmas `lookup_fmap_Some`, `lookup_omap_Some`, and
 `lookup_omap_id_Some`.

---
 theories/fin_maps.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index a7d8d9aa..fd9ecddc 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -652,6 +652,16 @@ Lemma delete_singleton_ne {A} i j (x : A) :
 Proof. intro. apply delete_notin. by apply lookup_singleton_ne. Qed.
 
 (** ** Properties of the map operations *)
+Lemma lookup_fmap_Some {A B} (f : A → B) (m : M A) i y :
+  (f <$> m) !! i = Some y ↔ ∃ x, f x = y ∧ m !! i = Some x.
+Proof. rewrite lookup_fmap, fmap_Some. naive_solver. Qed.
+Lemma lookup_omap_Some {A B} (f : A → option B) (m : M A) i y :
+  omap f m !! i = Some y ↔ ∃ x, f x = Some y ∧ m !! i = Some x.
+Proof. rewrite lookup_omap, bind_Some. naive_solver. Qed.
+Lemma lookup_omap_id_Some {A} (m : M (option A)) i x :
+  omap id m !! i = Some x ↔ m !! i = Some (Some x).
+Proof. rewrite lookup_omap_Some. naive_solver. Qed.
+
 Lemma fmap_empty {A B} (f : A → B) : f <$> ∅ = ∅.
 Proof. apply map_empty; intros i. by rewrite lookup_fmap, lookup_empty. Qed.
 Lemma omap_empty {A B} (f : A → option B) : omap f ∅ = ∅.
-- 
GitLab


From 920b62871005908dfbf1963f6b45803b8c4fb3d4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 4 Jan 2021 23:39:57 +0100
Subject: [PATCH 02/13] Generalize `omap_insert` and `omap_singleton` to cover
 both the `Some` and `None` case.

Add `_Some` and `_None` versions of the lemmas for the specific cases.
---
 theories/fin_maps.v | 51 ++++++++++++++++++++++++++++-----------------
 1 file changed, 32 insertions(+), 19 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index fd9ecddc..694b53d0 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -679,37 +679,50 @@ Proof.
   - by rewrite lookup_fmap, !lookup_insert.
   - by rewrite lookup_fmap, !lookup_insert_ne, lookup_fmap by done.
 Qed.
-Lemma fmap_delete {A B} (f: A → B) m i: f <$> delete i m = delete i (f <$> m).
-Proof.
-  apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
-  - by rewrite lookup_fmap, !lookup_delete.
-  - by rewrite lookup_fmap, !lookup_delete_ne, lookup_fmap by done.
-Qed.
-Lemma omap_insert {A B} (f : A → option B) m i x y :
-  f x = Some y → omap f (<[i:=x]>m) = <[i:=y]>(omap f m).
+Lemma omap_insert {A B} (f : A → option B) m i x :
+  omap f (<[i:=x]>m) = from_option (insert i) (delete i) (f x) (omap f m).
 Proof.
   intros; apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
-  - by rewrite lookup_omap, !lookup_insert.
-  - by rewrite lookup_omap, !lookup_insert_ne, lookup_omap by done.
-Qed.
+  - rewrite lookup_omap, !lookup_insert. destruct (f x) as [y|] eqn:Hx; simpl.
+    + by rewrite lookup_insert.
+    + by rewrite lookup_delete, Hx.
+  - rewrite lookup_omap, !lookup_insert_ne by done.
+    destruct (f x) as [y|] eqn:Hx; simpl.
+    + by rewrite lookup_insert_ne, lookup_omap by done.
+    + by rewrite lookup_delete_ne, lookup_omap by done.
+Qed.
+Lemma omap_insert_Some {A B} (f : A → option B) m i x y :
+  f x = Some y → omap f (<[i:=x]>m) = <[i:=y]>(omap f m).
+Proof. intros Hx. by rewrite omap_insert, Hx. Qed.
 Lemma omap_insert_None {A B} (f : A → option B) m i x :
   f x = None → omap f (<[i:=x]>m) = delete i (omap f m).
+Proof. intros Hx. by rewrite omap_insert, Hx. Qed.
+
+Lemma fmap_delete {A B} (f: A → B) m i: f <$> delete i m = delete i (f <$> m).
 Proof.
-  intros; apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
-  - by rewrite lookup_omap, lookup_insert, lookup_delete.
-  - by rewrite lookup_omap, lookup_insert_ne,
-     lookup_delete_ne, lookup_omap by done.
+  apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
+  - by rewrite lookup_fmap, !lookup_delete.
+  - by rewrite lookup_fmap, !lookup_delete_ne, lookup_fmap by done.
 Qed.
+
 Lemma map_fmap_singleton {A B} (f : A → B) i x : f <$> {[i := x]} = {[i := f x]}.
 Proof.
   by unfold singletonM, map_singleton; rewrite fmap_insert, fmap_empty.
 Qed.
-Lemma omap_singleton {A B} (f : A → option B) i x y :
-  f x = Some y → omap f {[ i := x ]} = {[ i := y ]}.
+Lemma omap_singleton {A B} (f : A → option B) i x :
+  omap f {[ i := x ]} = from_option (singletonM i) ∅ (f x).
 Proof.
-  intros. unfold singletonM, map_singleton.
-  by erewrite omap_insert, omap_empty by eauto.
+  rewrite <-insert_empty, omap_insert, omap_empty. destruct (f x) as [y|]; simpl.
+  - by rewrite insert_empty.
+  - by rewrite delete_empty.
 Qed.
+Lemma omap_singleton_Some {A B} (f : A → option B) i x y :
+  f x = Some y → omap f {[ i := x ]} = {[ i := y ]}.
+Proof. intros Hx. by rewrite omap_singleton, Hx. Qed.
+Lemma omap_singleton_None {A B} (f : A → option B) i x :
+  f x = None → omap f {[ i := x ]} = ∅.
+Proof. intros Hx. by rewrite omap_singleton, Hx. Qed.
+
 Lemma map_fmap_id {A} (m : M A) : id <$> m = m.
 Proof. apply map_eq; intros i; by rewrite lookup_fmap, option_fmap_id. Qed.
 Lemma map_fmap_compose {A B C} (f : A → B) (g : B → C) (m : M A) :
-- 
GitLab


From 49744e82c08315e53d21e0ac6fd6b2d72c0b535a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 4 Jan 2021 23:40:27 +0100
Subject: [PATCH 03/13] Add lemma `omap_delete`.

---
 theories/fin_maps.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 694b53d0..3b58bac7 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -704,6 +704,13 @@ Proof.
   - by rewrite lookup_fmap, !lookup_delete.
   - by rewrite lookup_fmap, !lookup_delete_ne, lookup_fmap by done.
 Qed.
+Lemma omap_delete {A B} (f: A → option B) m i :
+  omap f (delete i m) = delete i (omap f m).
+Proof.
+  apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
+  - by rewrite lookup_omap, !lookup_delete.
+  - by rewrite lookup_omap, !lookup_delete_ne, lookup_omap by done.
+Qed.
 
 Lemma map_fmap_singleton {A B} (f : A → B) i x : f <$> {[i := x]} = {[i := f x]}.
 Proof.
-- 
GitLab


From 0fc1b49813051930ebe0dccf684d804e7eddbe6f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 4 Jan 2021 23:32:41 +0100
Subject: [PATCH 04/13] Add lemmas `fmap_merge` and `omap_merge`.

---
 theories/fin_maps.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 3b58bac7..87b673d1 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1529,6 +1529,21 @@ Section more_merge.
     f (m1 !! i) (Some z) = Some x →
     <[i:=x]>(merge f m1 m2) = merge f m1 (<[i:=z]>m2).
   Proof. by intros; apply partial_alter_merge_r. Qed.
+
+  Lemma fmap_merge {D} (g : C → D) m1 m2 :
+    g <$> merge f m1 m2 = merge (λ mx1 mx2, g <$> f mx1 mx2) m1 m2.
+  Proof.
+    assert (DiagNone (λ mx1 mx2, g <$> f mx1 mx2)).
+    { unfold DiagNone. by rewrite diag_none. }
+    apply map_eq; intros i. by rewrite lookup_fmap, !lookup_merge by done.
+  Qed.
+  Lemma omap_merge {D} (g : C → option D) m1 m2 :
+    omap g (merge f m1 m2) = merge (λ mx1 mx2, f mx1 mx2 ≫= g) m1 m2.
+  Proof.
+    assert (DiagNone (λ mx1 mx2, f mx1 mx2 ≫= g)).
+    { unfold DiagNone. by rewrite diag_none. }
+    apply map_eq; intros i. by rewrite lookup_omap, !lookup_merge by done.
+  Qed.
 End more_merge.
 
 Lemma merge_diag {A C} (f : option A → option A → option C) `{!DiagNone f} (m : M A) :
-- 
GitLab


From 9eb0ae2bd564bf8cea769a237238b0b6e11eeda4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 4 Jan 2021 23:33:01 +0100
Subject: [PATCH 05/13] Add lemmas `map_disjoint_fmap` and `map_disjoint_omap`.

---
 theories/fin_maps.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 87b673d1..2b4de4fa 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1782,6 +1782,17 @@ Proof.
   rewrite !map_filter_lookup_Some. naive_solver.
 Qed.
 
+Lemma map_disjoint_fmap {A B} (f1 f2 : A → B) (m1 m2 : M A) :
+  m1 ##ₘ m2 ↔ f1 <$> m1 ##ₘ f2 <$> m2.
+Proof.
+  rewrite !map_disjoint_spec. setoid_rewrite lookup_fmap_Some. naive_solver.
+Qed.
+Lemma map_disjoint_omap {A B} (f1 f2 : A → option B) (m1 m2 : M A) :
+  m1 ##ₘ m2 → omap f1 m1 ##ₘ omap f2 m2.
+Proof.
+  rewrite !map_disjoint_spec. setoid_rewrite lookup_omap_Some. naive_solver.
+Qed.
+
 (** ** Properties of the [union_with] operation *)
 Section union_with.
   Context {A} (f : A → A → option A).
-- 
GitLab


From 94dfc264eb5c59e52bcb24477bdd8f493b5b0b38 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 4 Jan 2021 23:33:15 +0100
Subject: [PATCH 06/13] Add lemma `map_omap_union`.

---
 theories/fin_maps.v | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 2b4de4fa..221a0a42 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2082,7 +2082,15 @@ Proof.
   rewrite lookup_fmap, !lookup_union, !lookup_fmap.
   destruct (m1 !! i), (m2 !! i); auto.
 Qed.
-
+Lemma map_omap_union {A B} (f : A → option B) (m1 m2 : M A) :
+  m1 ##ₘ m2 →
+  omap f (m1 ∪ m2) = omap f m1 ∪ omap f m2.
+Proof.
+  intros Hdisj. apply map_eq; intros i. specialize (Hdisj i).
+  apply option_eq; intros x.
+  rewrite lookup_omap, !lookup_union, !lookup_omap.
+  destruct (m1 !! i), (m2 !! i); simpl; repeat (destruct (f _)); naive_solver.
+Qed.
 
 (** ** Properties of the [union_list] operation *)
 Lemma map_disjoint_union_list_l {A} (ms : list (M A)) (m : M A) :
-- 
GitLab


From d154faa4b5ef5815ad9f556ad737dd60cd1c9316 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 17 Jan 2021 14:10:55 +0100
Subject: [PATCH 07/13] Also write `map_imap_insert` using `from_option`.

---
 theories/fin_maps.v | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 221a0a42..3c67d967 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1001,12 +1001,9 @@ Proof.
 Qed.
 
 Lemma map_imap_insert {A B} (f : K → A → option B) (i : K) (v : A) (m : M A) :
-  map_imap f (<[i:=v]> m) = match f i v with
-                            | None   => delete i (map_imap f m)
-                            | Some w => <[i:=w]> (map_imap f m)
-                            end.
+  map_imap f (<[i:=v]> m) = from_option (insert i) (delete i) (f i v) (map_imap f m).
 Proof.
-  destruct (f i v) as [w|] eqn:Hw.
+  destruct (f i v) as [w|] eqn:Hw; simpl.
   - apply map_eq. intros k. rewrite map_lookup_imap.
     destruct (decide (k = i)) as [->|Hk_not_i].
     + by rewrite lookup_insert, lookup_insert.
-- 
GitLab


From 24e01f11a5a5f68bf8f2a320bff31ea65811163e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 17 Jan 2021 14:11:19 +0100
Subject: [PATCH 08/13] Generalize `map_size_insert` and `map_size_delete` to
 cover both the `Some` and `None` case.

---
 theories/fin_maps.v | 36 ++++++++++++++++++++++++++----------
 1 file changed, 26 insertions(+), 10 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 3c67d967..0c648034 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1063,21 +1063,37 @@ Proof. by rewrite map_size_empty_iff. Qed.
 
 Lemma map_size_singleton {A} i (x : A) : size ({[ i := x ]} : M A) = 1.
 Proof. unfold size, map_size. by rewrite map_to_list_singleton. Qed.
+
 Lemma map_size_insert {A} i x (m : M A) :
-  m !! i = None → size (<[i:=x]> m) = S (size m).
-Proof. intros. unfold size, map_size. by rewrite map_to_list_insert. Qed.
-Lemma map_size_delete {A} i (m : M A) :
-  is_Some (m !! i) → size (delete i m) = pred (size m).
-Proof. intros [??]. unfold size, map_size. by rewrite <-(map_to_list_delete m). Qed.
+  size (<[i:=x]> m) = from_option (λ _, id) S (m !! i) (size m).
+Proof.
+  destruct (m !! i) as [y|] eqn:?; simpl.
+  - rewrite <-(insert_id m i y) at 2 by done. rewrite <-!(insert_delete m).
+    unfold size, map_size.
+    by rewrite !map_to_list_insert by (by rewrite lookup_delete).
+  - unfold size, map_size. by rewrite map_to_list_insert.
+Qed.
 Lemma map_size_insert_Some {A} i x (m : M A) :
   is_Some (m !! i) → size (<[i:=x]> m) = size m.
+Proof. intros [y Hi]. by rewrite map_size_insert, Hi. Qed.
+Lemma map_size_insert_None {A} i x (m : M A) :
+  m !! i = None → size (<[i:=x]> m) = S (size m).
+Proof. intros Hi. by rewrite map_size_insert, Hi. Qed.
+
+Lemma map_size_delete {A} i (m : M A) :
+  size (delete i m) = from_option (λ _, pred) id (m !! i) (size m).
 Proof.
-  intros [? Hmi]. rewrite <-insert_delete, map_size_insert, map_size_delete.
-  - assert (size m ≠ 0); [|by lia]. apply map_size_non_empty_iff.
-    intros ->. rewrite lookup_empty in Hmi. done.
-  - eauto.
-  - rewrite lookup_delete. done.
+  destruct (m !! i) as [y|] eqn:?; simpl.
+  - unfold size, map_size. by rewrite <-(map_to_list_delete m).
+  - by rewrite delete_notin.
 Qed.
+Lemma map_size_delete_Some {A} i (m : M A) :
+  is_Some (m !! i) → size (delete i m) = pred (size m).
+Proof. intros [y Hi]. by rewrite map_size_delete, Hi. Qed.
+Lemma map_size_delete_None {A} i (m : M A) :
+  m !! i = None → size (delete i m) = size m.
+Proof. intros Hi. by rewrite map_size_delete, Hi. Qed.
+
 Lemma map_size_fmap {A B} (f : A -> B) (m : M A) : size (f <$> m) = size m.
 Proof. intros. unfold size, map_size. by rewrite map_to_list_fmap, fmap_length. Qed.
 
-- 
GitLab


From 056d738cd45e89c2aa315019212405b699850537 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 7 Jan 2021 09:32:46 +0100
Subject: [PATCH 09/13] CHANGELOG.

---
 CHANGELOG.md | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 63f94233..39e38bb4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -46,6 +46,9 @@ Coq 8.8 and 8.9 are no longer supported.
 - Add `rename select <pat> into <name>` tactic to find a hypothesis by pattern
   and give it a fixed name.
 - Remove unused `find_pat` tactic that was made mostly obsolete by `select`.
+- Generalize `omap_insert`, `omap_singleton`, `map_size_insert`, and
+  `map_size_delete` to cover the `Some` and `None` case. Add `_Some` and `_None`
+  versions of the lemmas for the specific cases.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
@@ -63,6 +66,10 @@ s/\bQp_mult_plus_distr_r\b/Qp_mul_add_distr_l/g
 s/\bmap_fmap_empty\b/fmap_empty/g
 s/\bmap_fmap_empty_inv\b/fmap_empty_inv/g
 s/\bseq_S_end_app\b/seq_S/g
+s/\bomap_insert\b/omap_insert_Some/g
+s/\bomap_singleton\b/omap_singleton_Some/g
+s/\bomap_size_insert\b/map_size_insert_None/g
+s/\bomap_size_delete\b/map_size_delete_Some/g
 ' $(find theories -name "*.v")
 ```
 
-- 
GitLab


From 0ab214ebc82221b581526bbf82ea39dfb7230a0f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 17 Jan 2021 14:40:31 +0100
Subject: [PATCH 10/13] Use explicit match instead of `from_option`.

---
 theories/fin_maps.v | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 0c648034..37be26d2 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -680,7 +680,8 @@ Proof.
   - by rewrite lookup_fmap, !lookup_insert_ne, lookup_fmap by done.
 Qed.
 Lemma omap_insert {A B} (f : A → option B) m i x :
-  omap f (<[i:=x]>m) = from_option (insert i) (delete i) (f x) (omap f m).
+  omap f (<[i:=x]>m) =
+    match f x with Some y => <[i:=y]> | None => delete i end (omap f m).
 Proof.
   intros; apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
   - rewrite lookup_omap, !lookup_insert. destruct (f x) as [y|] eqn:Hx; simpl.
@@ -717,7 +718,7 @@ Proof.
   by unfold singletonM, map_singleton; rewrite fmap_insert, fmap_empty.
 Qed.
 Lemma omap_singleton {A B} (f : A → option B) i x :
-  omap f {[ i := x ]} = from_option (singletonM i) ∅ (f x).
+  omap f {[ i := x ]} = match f x with Some y => {[ i:=y ]} | None => ∅ end.
 Proof.
   rewrite <-insert_empty, omap_insert, omap_empty. destruct (f x) as [y|]; simpl.
   - by rewrite insert_empty.
@@ -1000,10 +1001,11 @@ Proof.
   apply map_eq. intros i. rewrite map_lookup_imap. by destruct (m !! i).
 Qed.
 
-Lemma map_imap_insert {A B} (f : K → A → option B) (i : K) (v : A) (m : M A) :
-  map_imap f (<[i:=v]> m) = from_option (insert i) (delete i) (f i v) (map_imap f m).
+Lemma map_imap_insert {A B} (f : K → A → option B) i x (m : M A) :
+  map_imap f (<[i:=x]> m) =
+    match f i x with Some y => <[i:=y]> | None => delete i end (map_imap f m).
 Proof.
-  destruct (f i v) as [w|] eqn:Hw; simpl.
+  destruct (f i x) as [y|] eqn:Hw; simpl.
   - apply map_eq. intros k. rewrite map_lookup_imap.
     destruct (decide (k = i)) as [->|Hk_not_i].
     + by rewrite lookup_insert, lookup_insert.
@@ -1065,7 +1067,7 @@ Lemma map_size_singleton {A} i (x : A) : size ({[ i := x ]} : M A) = 1.
 Proof. unfold size, map_size. by rewrite map_to_list_singleton. Qed.
 
 Lemma map_size_insert {A} i x (m : M A) :
-  size (<[i:=x]> m) = from_option (λ _, id) S (m !! i) (size m).
+  size (<[i:=x]> m) = match m !! i with Some _ => id | None => S end (size m).
 Proof.
   destruct (m !! i) as [y|] eqn:?; simpl.
   - rewrite <-(insert_id m i y) at 2 by done. rewrite <-!(insert_delete m).
@@ -1081,7 +1083,7 @@ Lemma map_size_insert_None {A} i x (m : M A) :
 Proof. intros Hi. by rewrite map_size_insert, Hi. Qed.
 
 Lemma map_size_delete {A} i (m : M A) :
-  size (delete i m) = from_option (λ _, pred) id (m !! i) (size m).
+  size (delete i m) = match m !! i with Some _ => pred | None => id end (size m).
 Proof.
   destruct (m !! i) as [y|] eqn:?; simpl.
   - unfold size, map_size. by rewrite <-(map_to_list_delete m).
-- 
GitLab


From 6fb270ae9df311ebd90a91474e092dcd1ba091e7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 17 Jan 2021 14:40:44 +0100
Subject: [PATCH 11/13] Add lemmas `map_imap_insert_{Some,None}`.

---
 theories/fin_maps.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 37be26d2..3ae0f004 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1017,6 +1017,12 @@ Proof.
     + rewrite lookup_insert_ne, lookup_delete_ne by done.
       by rewrite map_lookup_imap.
 Qed.
+Lemma map_imap_insert_Some {A B} (f : K → A → option B) i x (m : M A) y :
+  f i x = Some y → map_imap f (<[i:=x]> m) = <[i:=y]> (map_imap f m).
+Proof. intros Hi. by rewrite map_imap_insert, Hi. Qed.
+Lemma map_imap_insert_None {A B} (f : K → A → option B) i x (m : M A) :
+  f i x = None → map_imap f (<[i:=x]> m) = delete i (map_imap f m).
+Proof. intros Hi. by rewrite map_imap_insert, Hi. Qed.
 
 Lemma map_imap_delete {A B} (f : K → A → option B) (m : M A) (i : K) :
   map_imap f (delete i m) = delete i (map_imap f m).
-- 
GitLab


From 1607a88174d9f1c41a4f984eaef3a212856eea02 Mon Sep 17 00:00:00 2001
From: Robbert <gitlab-sws@robbertkrebbers.nl>
Date: Tue, 19 Jan 2021 11:58:51 +0100
Subject: [PATCH 12/13] Apply 3 suggestion(s) to 1 file(s)

---
 theories/fin_maps.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 3ae0f004..fb14e077 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -681,7 +681,7 @@ Proof.
 Qed.
 Lemma omap_insert {A B} (f : A → option B) m i x :
   omap f (<[i:=x]>m) =
-    match f x with Some y => <[i:=y]> | None => delete i end (omap f m).
+    (match f x with Some y => <[i:=y]> | None => delete i end) (omap f m).
 Proof.
   intros; apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
   - rewrite lookup_omap, !lookup_insert. destruct (f x) as [y|] eqn:Hx; simpl.
@@ -1003,7 +1003,7 @@ Qed.
 
 Lemma map_imap_insert {A B} (f : K → A → option B) i x (m : M A) :
   map_imap f (<[i:=x]> m) =
-    match f i x with Some y => <[i:=y]> | None => delete i end (map_imap f m).
+    (match f i x with Some y => <[i:=y]> | None => delete i end) (map_imap f m).
 Proof.
   destruct (f i x) as [y|] eqn:Hw; simpl.
   - apply map_eq. intros k. rewrite map_lookup_imap.
@@ -1073,7 +1073,7 @@ Lemma map_size_singleton {A} i (x : A) : size ({[ i := x ]} : M A) = 1.
 Proof. unfold size, map_size. by rewrite map_to_list_singleton. Qed.
 
 Lemma map_size_insert {A} i x (m : M A) :
-  size (<[i:=x]> m) = match m !! i with Some _ => id | None => S end (size m).
+  size (<[i:=x]> m) = (match m !! i with Some _ => id | None => S end) (size m).
 Proof.
   destruct (m !! i) as [y|] eqn:?; simpl.
   - rewrite <-(insert_id m i y) at 2 by done. rewrite <-!(insert_delete m).
-- 
GitLab


From 2c0109b74b48a139889033dea6e0157df16d5db3 Mon Sep 17 00:00:00 2001
From: Robbert <gitlab-sws@robbertkrebbers.nl>
Date: Tue, 19 Jan 2021 12:48:25 +0100
Subject: [PATCH 13/13] Apply 1 suggestion(s) to 1 file(s)

---
 theories/fin_maps.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index fb14e077..5fd54b14 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1089,7 +1089,7 @@ Lemma map_size_insert_None {A} i x (m : M A) :
 Proof. intros Hi. by rewrite map_size_insert, Hi. Qed.
 
 Lemma map_size_delete {A} i (m : M A) :
-  size (delete i m) = match m !! i with Some _ => pred | None => id end (size m).
+  size (delete i m) = (match m !! i with Some _ => pred | None => id end) (size m).
 Proof.
   destruct (m !! i) as [y|] eqn:?; simpl.
   - unfold size, map_size. by rewrite <-(map_to_list_delete m).
-- 
GitLab