Commit 5d2a103d authored by Robbert Krebbers's avatar Robbert Krebbers

Setoid instances for fmap on fin_map and option.

parent efa43aa3
......@@ -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 *)
......
......@@ -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. *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment