From 5e384379e2bd60821763bfd8089537a05b6ca2bf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 31 May 2016 00:04:12 +0200
Subject: [PATCH] Generalize insert_delete lemma.

---
 algebra/cmra_big_op.v  |  5 +++--
 algebra/upred_big_op.v |  5 ++++-
 prelude/fin_maps.v     | 13 ++++---------
 3 files changed, 11 insertions(+), 12 deletions(-)

diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index 030ddb25f..9d7b6eeec 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -53,7 +53,8 @@ Proof. intros ?; by rewrite /big_opM map_to_list_insert. Qed.
 Lemma big_opM_delete m i x :
   m !! i = Some x → x ⋅ big_opM (delete i m) ≡ big_opM m.
 Proof.
-  intros. by rewrite -{2}(insert_delete m i x) // big_opM_insert ?lookup_delete.
+  intros. rewrite -{2}(insert_id m i x) // -insert_delete.
+  by rewrite big_opM_insert ?lookup_delete.
 Qed.
 Lemma big_opM_singleton i x : big_opM ({[i := x]} : gmap K A) ≡ x.
 Proof.
@@ -69,7 +70,7 @@ Proof.
   destruct (map_equiv_lookup_l (<[i:=x]> m1) m2 i x)
     as (y&?&Hxy); auto using lookup_insert.
   rewrite Hxy -big_opM_insert; last auto using lookup_delete.
-  by rewrite insert_delete.
+  by rewrite insert_delete insert_id.
 Qed.
 Lemma big_opM_lookup_valid n m i x : ✓{n} big_opM m → m !! i = Some x → ✓{n} x.
 Proof.
diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index 013de3e6b..176de68ea 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -171,7 +171,10 @@ Section gmap.
   Lemma big_sepM_delete Φ (m : gmap K A) i x :
     m !! i = Some x →
     ([★ map] k↦y ∈ m, Φ k y) ⊣⊢ (Φ i x ★ [★ map] k↦y ∈ delete i m, Φ k y).
-  Proof. intros. by rewrite -big_sepM_insert ?lookup_delete // insert_delete. Qed.
+  Proof.
+    intros. rewrite -big_sepM_insert ?lookup_delete //.
+    by rewrite insert_delete insert_id.
+  Qed.
 
   Lemma big_sepM_singleton Φ i x : ([★ map] k↦y ∈ {[i:=x]}, Φ k y) ⊣⊢ Φ i x.
   Proof.
diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v
index e39403a83..2e2f7e39b 100644
--- a/prelude/fin_maps.v
+++ b/prelude/fin_maps.v
@@ -366,13 +366,8 @@ Qed.
 Lemma delete_insert {A} (m : M A) i x :
   m !! i = None → delete i (<[i:=x]>m) = m.
 Proof. apply delete_partial_alter. Qed.
-Lemma insert_delete {A} (m : M A) i x :
-  m !! i = Some x → <[i:=x]>(delete i m) = m.
-Proof.
-  intros Hmi. unfold delete, map_delete, insert, map_insert.
-  rewrite <-partial_alter_compose. unfold compose. rewrite <-Hmi.
-  by apply partial_alter_self_alt.
-Qed.
+Lemma insert_delete {A} (m : M A) i x : <[i:=x]>(delete i m) = <[i:=x]> m.
+Proof. symmetry; apply (partial_alter_compose (λ _, Some x)). Qed.
 Lemma delete_subseteq {A} (m : M A) i : delete i m ⊆ m.
 Proof.
   rewrite !map_subseteq_spec. intros j x. rewrite lookup_delete_Some. tauto.
@@ -473,8 +468,8 @@ Lemma insert_subset_inv {A} (m1 m2 : M A) i x :
   ∃ m2', m2 = <[i:=x]>m2' ∧ m1 ⊂ m2' ∧ m2' !! i = None.
 Proof.
   intros Hi Hm1m2. exists (delete i m2). split_and?.
-  - rewrite insert_delete. done. eapply lookup_weaken, strict_include; eauto.
-    by rewrite lookup_insert.
+  - rewrite insert_delete, insert_id. done.
+    eapply lookup_weaken, strict_include; eauto. by rewrite lookup_insert.
   - eauto using insert_delete_subset.
   - by rewrite lookup_delete.
 Qed.
-- 
GitLab