Commit ba30e046 authored by Ralf Jung's avatar Ralf Jung

show that monadic set operations respect the partial order

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