Commit 982d20ee by Robbert Krebbers

### Setoid stuff for monadic operations.

parent 75c2b38e
 ... @@ -399,20 +399,20 @@ and fmap. We use these type classes merely for convenient overloading of ... @@ -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 notations and do not formalize any theory on monads (we do not even define a class with the monad laws). *) class with the monad laws). *) Class MRet (M : Type → Type) := mret: ∀ {A}, A → M A. Class MRet (M : Type → Type) := mret: ∀ {A}, A → M A. Instance: Params (@mret) 3. Arguments mret {_ _ _} _. Arguments mret {_ _ _} _. Instance: Params (@mret) 3. Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B. Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B. Arguments mbind {_ _ _ _} _ !_ /. Arguments mbind {_ _ _ _} _ !_ /. Instance: Params (@mbind) 5. Instance: Params (@mbind) 4. Class MJoin (M : Type → Type) := mjoin: ∀ {A}, M (M A) → M A. Class MJoin (M : Type → Type) := mjoin: ∀ {A}, M (M A) → M A. Instance: Params (@mjoin) 3. Arguments mjoin {_ _ _} !_ /. Arguments mjoin {_ _ _} !_ /. Instance: Params (@mjoin) 3. Class FMap (M : Type → Type) := fmap : ∀ {A B}, (A → B) → M A → M B. Class FMap (M : Type → Type) := fmap : ∀ {A B}, (A → B) → M A → M B. Instance: Params (@fmap) 6. Arguments fmap {_ _ _ _} _ !_ /. Arguments fmap {_ _ _ _} _ !_ /. Instance: Params (@fmap) 4. Class OMap (M : Type → Type) := omap: ∀ {A B}, (A → option B) → M A → M B. Class OMap (M : Type → Type) := omap: ∀ {A B}, (A → option B) → M A → M B. Instance: Params (@omap) 6. Arguments omap {_ _ _ _} _ !_ /. 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) (at level 60, right associativity) : C_scope. Notation "( m ≫=)" := (λ f, mbind f m) (only parsing) : C_scope. Notation "( m ≫=)" := (λ f, mbind f m) (only parsing) : C_scope. ... ...
 ... @@ -525,12 +525,12 @@ End fresh. ... @@ -525,12 +525,12 @@ End fresh. Section collection_monad. Section collection_monad. Context `{CollectionMonad M}. Context `{CollectionMonad M}. Global Instance collection_fmap_proper {A B} (f : A → B) : Global Instance collection_fmap_proper {A B} : Proper ((≡) ==> (≡)) (fmap f). Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) (@fmap M _ A B). Proof. intros X Y [??]; split; esolve_elem_of. Qed. Proof. intros f g ? X Y [??]; split; esolve_elem_of. Qed. Global Instance collection_bind_proper {A B} (f : A → M B) : Global Instance collection_bind_proper {A B} : Proper ((≡) ==> (≡)) (mbind f). Proper (((=) ==> (≡)) ==> (≡) ==> (≡)) (@mbind M _ A B). Proof. intros X Y [??]; split; esolve_elem_of. Qed. Proof. unfold respectful; intros f g Hfg X Y [??]; split; esolve_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; esolve_elem_of. Qed. Proof. intros X Y [??]; split; esolve_elem_of. Qed. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!