From d466539890c2fad4b706fedb9d92064c1c4c5318 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 11 Aug 2021 18:13:46 +0200
Subject: [PATCH] add map_size_disj_union

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 8bbcffa1..e2d7f68c 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2294,6 +2294,20 @@ Proof.
   destruct (m1 !! i), (m2 !! i); simpl; repeat (destruct (f _)); naive_solver.
 Qed.
 
+Lemma map_size_disj_union {A} (m1 m2 : M A) :
+  m1 ##ₘ m2 → size (m1 ∪ m2) = size m1 + size m2.
+Proof.
+  intros Hdisj. induction m1 as [|k x m1 Hm1 IH] using map_ind.
+  { rewrite map_empty_union. (* FIXME: [rewrite left_id] leaves a goal *)
+    rewrite map_size_empty. done. }
+  rewrite <-insert_union_l.
+  rewrite map_size_insert.
+  rewrite lookup_union_r by done.
+  apply map_disjoint_insert_l in Hdisj as [-> Hdisj].
+  rewrite map_size_insert, Hm1.
+  rewrite IH by done. done.
+Qed.
+
 Lemma map_cross_split {A} (ma mb mc md : M A) :
   ma ##ₘ mb → mc ##ₘ md →
   ma ∪ mb = mc ∪ md →
-- 
GitLab