From 33a02fc64e51fe08787e82d780231c582397bf4b Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Thu, 15 Apr 2021 10:29:07 +0200
Subject: [PATCH] Add some more lemmas for difference
---
theories/fin_maps.v | 17 +++++++++++++++++
1 file changed, 17 insertions(+)
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 0197e848..48aae385 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2422,6 +2422,8 @@ 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_difference_union {A} (m1 m2 : M A) :
m1 ⊆ m2 → m1 ∪ m2 ∖ m1 = m2.
Proof.
@@ -2441,6 +2443,21 @@ 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).
+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.
+Proof.
+ apply map_subseteq_spec. intros i' x'.
+ rewrite !lookup_difference_Some, lookup_insert_Some, lookup_insert_None.
+ naive_solver.
+Qed.
+
Lemma delete_difference {A} (m1 m2 : M A) i x :
delete i (m1 ∖ m2) = m1 ∖ <[i:=x]> m2.
Proof.
--
GitLab