From 41df24bf2c7f197ed30796557f12ee172f6709d6 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Thu, 15 Apr 2021 15:17:34 +0200
Subject: [PATCH] Add list_to_map_app

---
 theories/fin_maps.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 7397ef32..74ef0e8e 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2227,7 +2227,14 @@ Lemma foldr_delete_union {A} (m1 m2 : M A) is :
   foldr delete (m1 ∪ m2) is = foldr delete m1 is ∪ foldr delete m2 is.
 Proof. apply foldr_delete_union_with. Qed.
 
-(** ** Properties on disjointness of conversion to lists *)
+(** ** Properties on conversion to lists that depend on [∪] and [##ₘ] *)
+Lemma list_to_map_app {A} (l1 l2 : list (K * A)):
+  list_to_map (l1 ++ l2) =@{M A} list_to_map l1 ∪ list_to_map l2.
+Proof.
+  induction l1 as [|[??] ? IH]; simpl.
+  { by rewrite (left_id _ _). }
+  by rewrite IH, insert_union_l.
+Qed.
 Lemma map_disjoint_list_to_map_l {A} (m : M A) ixs :
   list_to_map ixs ##ₘ m ↔ Forall (λ ix, m !! ix.1 = None) ixs.
 Proof.
-- 
GitLab