From a198e45b95dad74dfeeaa4ac95cc2a9ec26237b4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 14 Jan 2016 02:04:20 +0100
Subject: [PATCH] Some properties about fmap on fin_maps.

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

diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v
index b51728b50..4aecf8d16 100644
--- a/prelude/fin_maps.v
+++ b/prelude/fin_maps.v
@@ -234,6 +234,8 @@ Lemma map_subset_empty {A} (m : M A) : m ⊄ ∅.
 Proof.
   intros [_ []]. rewrite map_subseteq_spec. intros ??. by rewrite lookup_empty.
 Qed.
+Lemma map_fmap_empty {A B} (f : A → B) : f <$> (∅ : M A) = ∅.
+Proof. by apply map_eq; intros i; rewrite lookup_fmap, !lookup_empty. Qed.
 
 (** ** Properties of the [partial_alter] operation *)
 Lemma partial_alter_ext {A} (f g : option A → option A) (m : M A) i :
@@ -516,6 +518,10 @@ Proof.
   intros. apply map_eq; intros i'. by destruct (decide (i = i')) as [->|?];
     rewrite ?lookup_alter, ?lookup_singleton_ne, ?lookup_alter_ne by done.
 Qed.
+Lemma map_fmap_singleton {A B} (f : A → B) i x : f <$> {[i ↦ x]} = {[i ↦ f x]}.
+Proof.
+  by unfold singletonM, map_singleton; rewrite fmap_insert, map_fmap_empty.
+Qed.
 
 (** ** Properties of the map operations *)
 Lemma fmap_empty {A B} (f : A → B) : f <$> ∅ = ∅.
-- 
GitLab