Setoid instances for fmap on fin_map and option.

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 *)

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. *)