From 62ce48ffd7007e707526a9938d77482576d639ab Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Tue, 20 Apr 2021 10:18:59 +0200
Subject: [PATCH] Strengthen, rename, and move some lemmas

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 06ef84ef..e40137df 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -647,8 +647,8 @@ Proof.
 Qed.
 Lemma singleton_non_empty {A} i (x : A) : {[i:=x]} ≠ (∅ : M A).
 Proof. apply insert_non_empty. Qed.
-Lemma map_singleton_lookup_subseteq {A} i (x : A) (m : M A) :
-  m !! i = Some x ↔ {[i := x]} ⊆ m.
+Lemma map_singleton_subseteq {A} i (x : A) (m : M A) :
+  {[i := x]} ⊆ m ↔ m !! i = Some x.
 Proof.
   rewrite map_subseteq_spec. setoid_rewrite lookup_singleton_Some. naive_solver.
 Qed.
@@ -2010,12 +2010,6 @@ 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 map_union_least {A} (m1 m2 m3 : M A) :
-  m1 ⊆ m3 → m2 ⊆ m3 → m1 ∪ m2 ⊆ m3.
-Proof.
-  intros ??. apply map_subseteq_spec.
-  intros ?? [?|[_ ?]]%lookup_union_Some_raw; by eapply lookup_weaken.
-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))).
@@ -2038,6 +2032,12 @@ Lemma map_union_subseteq_r {A} (m1 m2 : M A) : m1 ##ₘ m2 → m2 ⊆ m1 ∪ m2.
 Proof.
   intros. rewrite map_union_comm by done. by apply map_union_subseteq_l.
 Qed.
+Lemma map_union_least {A} (m1 m2 m3 : M A) :
+  m1 ⊆ m3 → m2 ⊆ m3 → m1 ∪ m2 ⊆ m3.
+Proof.
+  intros ??. apply map_subseteq_spec.
+  intros ?? [?|[_ ?]]%lookup_union_Some_raw; by eapply lookup_weaken.
+Qed.
 Lemma map_union_subseteq_l_alt {A} (m1 m2 m3 : M A) : m1 ⊆ m2 → m1 ⊆ m2 ∪ m3.
 Proof. intros. trans m2; auto using map_union_subseteq_l. Qed.
 Lemma map_union_subseteq_r_alt {A} (m1 m2 m3 : M A) :
@@ -2422,8 +2422,10 @@ Proof.
 Qed.
 Lemma map_disjoint_difference_r {A} (m1 m2 : M A) : m1 ⊆ m2 → m1 ##ₘ m2 ∖ m1.
 Proof. intros. symmetry. by apply map_disjoint_difference_l. Qed.
-Lemma map_difference_subseteq {A} (m1 m2 : M A) : m1 ∖ m2 ⊆ m1.
-Proof. apply map_subseteq_spec. by intros ?? []%lookup_difference_Some. Qed.
+Lemma map_subseteq_difference_l {A} (m1 m2 m : M A) : m1 ⊆ m → m1 ∖ m2 ⊆ m.
+Proof.
+  rewrite !map_subseteq_spec. setoid_rewrite lookup_difference_Some. naive_solver.
+Qed.
 Lemma map_difference_union {A} (m1 m2 : M A) :
   m1 ⊆ m2 → m1 ∪ m2 ∖ m1 = m2.
 Proof.
@@ -2443,15 +2445,31 @@ Global Instance map_difference_right_id {A} : RightId (=) (∅:M A) (∖) := _.
 Lemma map_difference_empty {A} (m : M A) : m ∖ ∅ = m.
 Proof. by rewrite (right_id _ _). Qed.
 
-Lemma map_difference_insert_l {A} (m1 m2 : M A) i x :
-  m2 !! i = None → <[i := x]> m1 ∖ m2 = <[i := x]> (m1 ∖ m2).
+Lemma insert_difference {A} (m1 m2 : M A) i x :
+  m2 !! i = None → <[i := x]> (m1 ∖ m2) = <[i := x]> m1 ∖ m2.
 Proof.
   intros. apply map_eq. intros j. apply option_eq. intros y.
   rewrite lookup_insert_Some, !lookup_difference_Some, lookup_insert_Some.
   naive_solver.
 Qed.
-Lemma map_difference_insert_subseteq {A} (m1 m2 : M A) i x :
-  <[i := x]> m1 ∖ <[i := x]> m2 ⊆ m1 ∖ m2.
+Lemma difference_insert {A} (m1 m2 : M A) i x1 x2 x3 :
+  <[i := x1]> m1 ∖ <[i := x2]> m2 = m1 ∖ <[i := x3]> m2.
+Proof.
+  apply map_eq. intros i'. symmetry.
+  destruct ((<[i:=x1]> m1 ∖ <[i:=x2]> m2) !! i') as [x'|] eqn:Eqx'.
+  - apply lookup_difference_Some.
+    apply lookup_difference_Some in Eqx' as [Eqx' [EqN ?]%lookup_insert_None].
+    rewrite lookup_insert_ne; [|done].
+    by rewrite lookup_insert_ne in Eqx'.
+  - apply lookup_difference_None.
+    apply lookup_difference_None in Eqx' as [[]%lookup_insert_None|[x' Eqx']].
+    + by left.
+    + right. revert Eqx'. destruct (decide (i' = i)) as [->|].
+      * rewrite !lookup_insert; by eauto.
+      * rewrite !lookup_insert_ne; by eauto.
+Qed.
+Lemma difference_insert_subseteq {A} (m1 m2 : M A) i x1 x2 :
+  <[i := x1]> m1 ∖ <[i := x2]> m2 ⊆ m1 ∖ m2.
 Proof.
   apply map_subseteq_spec. intros i' x'.
   rewrite !lookup_difference_Some, lookup_insert_Some, lookup_insert_None.
-- 
GitLab