From 60f310e6683b8d40d801784f3b1353a474f294ac Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 28 Jul 2021 15:04:19 +0200
Subject: [PATCH] add some lookup_{union,difference} lemmas

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index a6211d3e..8fce3468 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2043,13 +2043,6 @@ Proof. rewrite lookup_union. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
 Lemma lookup_union_None {A} (m1 m2 : M A) i :
   (m1 ∪ m2) !! i = None ↔ m1 !! i = None ∧ m2 !! i = None.
 Proof. rewrite lookup_union.  destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
-Lemma map_positive_l {A} (m1 m2 : M A) : m1 ∪ m2 = ∅ → m1 = ∅.
-Proof.
-  intros Hm. apply map_empty. intros i. apply (f_equal (.!! i)) in Hm.
-  rewrite lookup_empty, lookup_union_None in Hm; tauto.
-Qed.
-Lemma map_positive_l_alt {A} (m1 m2 : M A) : m1 ≠ ∅ → m1 ∪ m2 ≠ ∅.
-Proof. eauto using map_positive_l. Qed.
 Lemma lookup_union_Some {A} (m1 m2 : M A) i x :
   m1 ##ₘ m2 → (m1 ∪ m2) !! i = Some x ↔ m1 !! i = Some x ∨ m2 !! i = Some x.
 Proof.
@@ -2062,6 +2055,20 @@ Proof. intro. rewrite lookup_union_Some_raw; intuition. Qed.
 Lemma lookup_union_Some_r {A} (m1 m2 : M A) i x :
   m1 ##ₘ m2 → m2 !! i = Some x → (m1 ∪ m2) !! i = Some x.
 Proof. intro. rewrite lookup_union_Some; intuition. Qed.
+Lemma lookup_union_Some_l_inv {A} (m1 m2 : M A) i x :
+  (m1 ∪ m2) !! i = Some x → m2 !! i = None → m1 !! i = Some x.
+Proof. rewrite lookup_union_Some_raw. naive_solver. Qed.
+Lemma lookup_union_Some_r_inv {A} (m1 m2 : M A) i x :
+  (m1 ∪ m2) !! i = Some x → m1 !! i = None → m2 !! i = Some x.
+Proof. rewrite lookup_union_Some_raw. naive_solver. Qed.
+Lemma lookup_union_is_Some {A} (m1 m2 : M A) i :
+  is_Some ((m1 ∪ m2) !! i) ↔ is_Some (m1 !! i) ∨ is_Some (m2 !! i).
+Proof.
+  unfold is_Some. setoid_rewrite lookup_union_Some_raw. split; [naive_solver|].
+  intros [[a Ha]|[a Ha]]; [naive_solver|].
+  destruct (m1 !! i); naive_solver.
+Qed.
+
 Lemma map_union_comm {A} (m1 m2 : M A) : m1 ##ₘ m2 → m1 ∪ m2 = m2 ∪ m1.
 Proof.
   intros Hdisjoint. apply (merge_comm (union_with (λ x _, Some x))).
@@ -2069,6 +2076,14 @@ Proof.
   destruct (m1 !! i), (m2 !! i); compute; naive_solver.
 Qed.
 
+Lemma map_positive_l {A} (m1 m2 : M A) : m1 ∪ m2 = ∅ → m1 = ∅.
+Proof.
+  intros Hm. apply map_empty. intros i. apply (f_equal (.!! i)) in Hm.
+  rewrite lookup_empty, lookup_union_None in Hm; tauto.
+Qed.
+Lemma map_positive_l_alt {A} (m1 m2 : M A) : m1 ≠ ∅ → m1 ∪ m2 ≠ ∅.
+Proof. eauto using map_positive_l. Qed.
+
 Lemma map_subseteq_union {A} (m1 m2 : M A) : m1 ⊆ m2 → m1 ∪ m2 = m2.
 Proof.
   rewrite map_subseteq_spec.
@@ -2525,6 +2540,9 @@ Proof.
   unfold difference, map_difference; rewrite lookup_difference_with.
   destruct (m1 !! i), (m2 !! i); compute; intuition congruence.
 Qed.
+Lemma lookup_difference_is_Some {A} (m1 m2 : M A) i :
+  is_Some ((m1 ∖ m2) !! i) ↔ is_Some (m1 !! i) ∧ m2 !! i = None.
+Proof. unfold is_Some. setoid_rewrite lookup_difference_Some. naive_solver. Qed.
 Lemma lookup_difference_None {A} (m1 m2 : M A) i :
   (m1 ∖ m2) !! i = None ↔ m1 !! i = None ∨ is_Some (m2 !! i).
 Proof.
-- 
GitLab