From d11b32df33073c79907e028f0eae1b2645314167 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Fri, 1 Jul 2016 13:11:09 +0200
Subject: [PATCH] New lemma aboud maps : fmap_delete

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 5f5e702b..ac1ae49f 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -527,6 +527,12 @@ Proof.
   - by rewrite lookup_fmap, !lookup_insert.
   - by rewrite lookup_fmap, !lookup_insert_ne, lookup_fmap by done.
 Qed.
+Lemma fmap_delete {A B} (f: A → B) m i: f <$> delete i m = delete i (f <$> m).
+Proof.
+  apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
+  - by rewrite lookup_fmap, !lookup_delete.
+  - by rewrite lookup_fmap, !lookup_delete_ne, lookup_fmap by done.
+Qed.
 Lemma omap_insert {A B} (f : A → option B) m i x y :
   f x = Some y → omap f (<[i:=x]>m) = <[i:=y]>(omap f m).
 Proof.
-- 
GitLab