Maybe monad is monad

gistfile1.ml

Definition bind {A B : Type} (m : option A) (f : A -> option B) : option B :=
    match m with
      None => None
    | Some v => f v
    end.
Infix ">>=" := bind (at level 50).

Definition ret {A : Type} (v : A) : option A :=
  Some v.

Theorem a: forall A B (f : A -> option B) x,
  (ret x) >>= f = f x.
Proof.
intros.
simpl.
reflexivity.
Qed.

Theorem b: forall A (m : option A),
  m >>= ret = m.
Proof.
intros.
destruct m.
 simpl.
 reflexivity.

 simpl.
 reflexivity.
Qed.

Theorem c: forall A B C (f : A -> option B) (g : B -> option C) m,
  (m >>= f) >>= g = m >>= (fun x => f x >>= g).
Proof.
intros.
destruct m.
 simpl.
 destruct (f a0).
  simpl.
  reflexivity.

  simpl.
  reflexivity.

 simpl.
 reflexivity.
Qed.