The Coq mailing list

[Bas Spitters <spitters AT cs.ru.nl>]

You probably need functional extensionality/setoids.

Bas

On Sat, Jul 2, 2011 at 9:24 AM, frank maltman
<frank.maltman AT googlemail.com>
 wrote:
> Hello list.
>
> I was working on some simple monad implementations a few weeks ago. The
> implementations for the identity, option, and error monads were very
> easy but I became stuck when it came to proving the monad laws for the
> State monad. I've gone back to them today but have gotten no further. Any
> advice on how to prove the laws would be appreciated!
>
> --8<--
>
> Module Type Base.
>  Parameter M : Type -> Type.
>
>  Parameter bind     : forall {A B : Type}, M A -> (A -> M B) -> M B.
>  Parameter return_m : forall {A : Type}, A -> M A.
>
>  (* return x >>= f = f x *)
>  Parameter left_identity : forall (A B : Type) (x : A) (f : A -> M B),
>    bind (return_m x) f = f x.
>
>  (* m >>= return = m *)
>  Parameter right_identity : forall (A : Type) (m : M A),
>    bind m return_m = m.
>
>  (* (m >>= f) >>= g = m >>= (\x -> f x >>= g) *)
>  Parameter associativity : forall (A B C : Type) (f : A -> M B) (g : B -> M 
> C) (m : M A),
>    bind (bind m f) g = bind m (fun z => bind (f z) g).
>
> End Base.
>
> Module Type Notations (MT : Base).
>  Notation "x >>= y" := (MT.bind x y)            (at level 42, left 
> associativity).
>  Notation "x >>  y" := (MT.bind x (fun _ => y)) (at level 42, left 
> associativity).
> End Notations.
>
> Inductive state (S A : Type) :=
>  | State : (S -> (A * S)) -> state S A.
>
> Definition run {S A : Type} (m : state S A) : (S -> (A * S)) :=
>  match m with
>    State c => c
>  end.
>
> Module Monad_State <: Base.
>  Parameter S : Type.
>  Definition M := state S.
>
>  Definition bind {A B : Type} (m : M A) (f : A -> M B) : M B :=
>    State S B (fun s =>
>      match run m s with
>        | (a, s') => run (f a) s'
>      end).
>
>  Definition return_m {A : Type} (x : A) : M A :=
>    State S A (fun s => (x, s)).
>
>  Lemma left_identity : forall (A B : Type) (x : A) (f : A -> M B),
>    bind (return_m x) f = f x.
>  Proof.
>    admit.
>  Defined.
>
>  Lemma right_identity : forall (A : Type) (m : M A),
>    bind m return_m = m.
>  Proof.
>    admit.
>  Defined.
>
>  Lemma associativity : forall {A B C : Type} (f : A -> M B) (g : B -> M C) 
> (m : M A),
>    bind (bind m f) g = bind m (fun z => bind (f z) g).
>  Proof.
>    admit.
>  Defined.
>
> End Monad_State.
>
> --8<--
>