From 7583028fe26130395ac402efc580d7536d71ee24 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 15 Feb 2016 19:45:02 +0100
Subject: [PATCH] show that monadic set operations respect the partial order

---
 theories/collections.v | 9 +++++++++
 theories/sets.v        | 2 +-
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/theories/collections.v b/theories/collections.v
index f3ed2dd9..c33193b1 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -531,12 +531,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.
diff --git a/theories/sets.v b/theories/sets.v
index f2543ebe..f2b215a8 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -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.
-- 
GitLab