From 982d20eeec75e6684ff19cae3f2af32c87de4b1e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 16 Nov 2015 23:01:41 +0100
Subject: [PATCH] Setoid stuff for monadic operations.

---
 prelude/base.v        | 10 +++++-----
 prelude/collections.v | 12 ++++++------
 2 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/prelude/base.v b/prelude/base.v
index adc16d87b..a94511d4e 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -399,20 +399,20 @@ and fmap. We use these type classes merely for convenient overloading of
 notations and do not formalize any theory on monads (we do not even define a
 class with the monad laws). *)
 Class MRet (M : Type → Type) := mret: ∀ {A}, A → M A.
-Instance: Params (@mret) 3.
 Arguments mret {_ _ _} _.
+Instance: Params (@mret) 3.
 Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B.
 Arguments mbind {_ _ _ _} _ !_ /.
-Instance: Params (@mbind) 5.
+Instance: Params (@mbind) 4.
 Class MJoin (M : Type → Type) := mjoin: ∀ {A}, M (M A) → M A.
-Instance: Params (@mjoin) 3.
 Arguments mjoin {_ _ _} !_ /.
+Instance: Params (@mjoin) 3.
 Class FMap (M : Type → Type) := fmap : ∀ {A B}, (A → B) → M A → M B.
-Instance: Params (@fmap) 6.
 Arguments fmap {_ _ _ _} _ !_ /.
+Instance: Params (@fmap) 4.
 Class OMap (M : Type → Type) := omap: ∀ {A B}, (A → option B) → M A → M B.
-Instance: Params (@omap) 6.
 Arguments omap {_ _ _ _} _ !_ /.
+Instance: Params (@omap) 4.
 
 Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : C_scope.
 Notation "( m ≫=)" := (λ f, mbind f m) (only parsing) : C_scope.
diff --git a/prelude/collections.v b/prelude/collections.v
index 7caafe69d..dd1d2f9e9 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -525,12 +525,12 @@ End fresh.
 Section collection_monad.
   Context `{CollectionMonad M}.
 
-  Global Instance collection_fmap_proper {A B} (f : A → B) :
-    Proper ((≡) ==> (≡)) (fmap f).
-  Proof. intros X Y [??]; split; esolve_elem_of. Qed.
-  Global Instance collection_bind_proper {A B} (f : A → M B) :
-    Proper ((≡) ==> (≡)) (mbind f).
-  Proof. intros X Y [??]; split; esolve_elem_of. Qed.
+  Global Instance collection_fmap_proper {A B} :
+    Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) (@fmap M _ A B).
+  Proof. intros f g ? X Y [??]; split; esolve_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; esolve_elem_of. Qed.
   Global Instance collection_join_proper {A} :
     Proper ((≡) ==> (≡)) (@mjoin M _ A).
   Proof. intros X Y [??]; split; esolve_elem_of. Qed.
-- 
GitLab