From e18f9a7dec67568e374c83d673628bbb9f768ca4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 26 May 2021 15:09:31 +0200
Subject: [PATCH] Lemmas for `map_kmap` and disjointness and subsets.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index fae2bb19..9bcc4934 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2666,6 +2666,20 @@ Section map_kmap.
   Lemma map_kmap_fmap {A B} (g : A → B) (m : M1 A) :
     map_kmap f (g <$> m) = g <$> (map_kmap f m).
   Proof. by rewrite !map_fmap_alt, map_kmap_omap. Qed.
+
+  Lemma map_disjoint_kmap {A} (m1 m2 : M1 A) :
+    map_kmap f m1 ##ₘ map_kmap f m2 ↔ m1 ##ₘ m2.
+  Proof.
+    rewrite !map_disjoint_spec. setoid_rewrite lookup_map_kmap_Some. naive_solver.
+  Qed.
+  Lemma map_disjoint_subseteq {A} (m1 m2 : M1 A) :
+    map_kmap f m1 ⊆ map_kmap f m2 ↔ m1 ⊆ m2.
+  Proof.
+    rewrite !map_subseteq_spec. setoid_rewrite lookup_map_kmap_Some. naive_solver.
+  Qed.
+  Lemma map_disjoint_subset {A} (m1 m2 : M1 A) :
+    map_kmap f m1 ⊂ map_kmap f m2 ↔ m1 ⊂ m2.
+  Proof. unfold strict. by rewrite !map_disjoint_subseteq. Qed.
 End map_kmap.
 
 (** * Tactics *)
-- 
GitLab