Removed the extras from Monad. They were annoying and had no benefit.

I also proved that State is a monad.

coq/monads/maybe.v

@@ -11,11 +11,7 @@ Instance Maybe_Monad : Monad Maybe := {
                | None => None b
               end;
 
-  ret a := Just a;
-
-  bind_ign a b i j := j;
-
-  fail_m a s := None a
+  ret a := Just a
 }.
 
 (* Proofs of the monad laws. *)

coq/monads/monad.v

@@ -17,17 +17,8 @@ Class Monad (m : Type -> Type) := {
     where "m '>>=' f" := (bind m f);
 
   (* return - The injector of our monad. *)
-  ret : forall {a}, a -> m a;
-
-  (* Extras. *)
+  ret : forall {a}, a -> m a;  
 
-  (* bind_ign - Like bind, but ignores the argument. *)
-  bind_ign : forall {a} {b}, m a -> m b -> m b
-    where "m '>>' f" := (bind m f);
-
-  (* fail_m - Used to break a chain. *)
-  fail_m : forall {a}, string -> m a;
-
   (* Monads Laws. *)
 
   (* Left identity. *)
@@ -75,5 +66,3 @@ Proof.
   rewrite -> left_id.
   reflexivity.
 Defined.
-
-

coq/monads/state.v

@@ -0,0 +1,47 @@
+Require Import monad.
+
+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 a => a
+  end.
+
+(* State is a monad. *)
+Parameter S : Type.
+
+Instance State_Monad : Monad (State S) := {
+  bind a b i f := 
+    state S b (fun s => 
+      let x := run i s in 
+        match x with
+          | (x', s') => run (f x') s' 
+        end);
+
+  ret A a := state S A (fun s => (a, s))
+}.
+
+Require Import FunctionalExtensionality.
+Proof.
+  intros a b c f.
+  simpl; destruct (f c); simpl; reflexivity.
+
+  intros a m'.
+  destruct m'.
+  simpl. 
+  rewrite -> (functional_extensionality (fun s : S => let (x', s') := p s in (x', s')) p).
+  reflexivity.
+  intros x.
+  destruct (p x).
+  reflexivity.
+
+  intros a b c i f g.
+  simpl.
+  f_equal.
+  destruct i.
+  extensionality s.
+  simpl.
+  destruct (p s).
+  reflexivity.
+Defined.