From 28045c1038f4855ecd81182d83f73ecf61202af8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 14 Jun 2016 15:03:52 +0200
Subject: [PATCH] Setoid instances for fmap on fin_map and option.

---
 theories/fin_maps.v | 5 +++++
 theories/option.v   | 4 ++++
 2 files changed, 9 insertions(+)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 05272e82..5f5e702b 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -174,6 +174,11 @@ Section setoid.
   Lemma map_equiv_lookup_l (m1 m2 : M A) i x :
     m1 ≡ m2 → m1 !! i = Some x → ∃ y, m2 !! i = Some y ∧ x ≡ y.
   Proof. generalize (equiv_Some_inv_l (m1 !! i) (m2 !! i) x); naive_solver. Qed.
+  Global Instance map_fmap_proper `{Equiv B} (f : A → B) :
+    Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap (M:=M) f).
+  Proof.
+    intros ? m m' ? k; rewrite !lookup_fmap. by apply option_fmap_proper.
+  Qed.
 End setoid.
 
 (** ** General properties *)
diff --git a/theories/option.v b/theories/option.v
index 24552ced..5af4b5a0 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -207,6 +207,10 @@ Proof. destruct mx; naive_solver. Qed.
 Lemma bind_with_Some {A} (mx : option A) : mx ≫= Some = mx.
 Proof. by destruct mx. Qed.
 
+Instance option_fmap_proper `{Equiv A, Equiv B} (f : A → B) :
+  Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap (M:=option) f).
+Proof. destruct 2; constructor; auto. Qed.
+
 (** ** Inverses of constructors *)
 (** We can do this in a fancy way using dependent types, but rewrite does
 not particularly like type level reductions. *)
-- 
GitLab