diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v index 3229099b5a642cd57ccbd94f8d9557ba9671b46f..e752c675b12089a3141a3f049bd7cdcccfe0665a 100644 --- a/prelude/fin_maps.v +++ b/prelude/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/prelude/option.v b/prelude/option.v index 6f1c36808cb1250e689a2e3e3f74446ae7212ddf..0f972ca16d9d20d29fb18feb0e59d4e0b56261b2 100644 --- a/prelude/option.v +++ b/prelude/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. *)