Commit 0da9298e authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 79421f72 7583028f
......@@ -533,12 +533,21 @@ End fresh.
Section collection_monad.
Context `{CollectionMonad M}.
Global Instance collection_fmap_mono {A B} :
Proper (pointwise_relation _ (=) ==> () ==> ()) (@fmap M _ A B).
Proof. intros f g ? X Y ?; solve_elem_of. Qed.
Global Instance collection_fmap_proper {A B} :
Proper (pointwise_relation _ (=) ==> () ==> ()) (@fmap M _ A B).
Proof. intros f g ? X Y [??]; split; solve_elem_of. Qed.
Global Instance collection_bind_mono {A B} :
Proper (((=) ==> ()) ==> () ==> ()) (@mbind M _ A B).
Proof. unfold respectful; intros f g Hfg X Y ?; solve_elem_of. Qed.
Global Instance collection_bind_proper {A B} :
Proper (((=) ==> ()) ==> () ==> ()) (@mbind M _ A B).
Proof. unfold respectful; intros f g Hfg X Y [??]; split; solve_elem_of. Qed.
Global Instance collection_join_mono {A} :
Proper (() ==> ()) (@mjoin M _ A).
Proof. intros X Y ?; solve_elem_of. Qed.
Global Instance collection_join_proper {A} :
Proper (() ==> ()) (@mjoin M _ A).
Proof. intros X Y [??]; split; solve_elem_of. Qed.
......
......@@ -28,4 +28,4 @@ Instance set_join : MJoin set := λ A (XX : set (set A)),
Instance set_collection_monad : CollectionMonad set.
Proof. by split; try apply _. Qed.
Global Opaque set_union set_intersection.
Global Opaque set_union set_intersection set_difference.
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