# Coq and The Maybe Monad

Posted on December 17, 2007 by Tommy McGuire
Labels: coq, programming language
In the spirit of Coq and The Monad Laws, I here is a quick (and easy) proof that Maybe (known in Coq/OCaml as option) satisfies the three Monad Laws.

Section MaybeMonad.Definition retO (A:Set) (a:A) := Some a.Definition bindO (A B : Set) (m:option A) (f:A -&gt; option B) := match m with Some m' =&gt; f m' | None =&gt; None end.(* return a &gt;&gt;= f = f a *)Theorem first_law_opt :forall (A B : Set) (a:A) (f:A -&gt; option B), bindO A B (retO A a) f = f a.intros A B a f.unfold bindO.unfold retO.reflexivity.Qed.(* (m &gt;&gt;= return) = m *)Theorem second_law_opt : forall (A:Set) (m : option A), bindO A A m (retO A) = m.intros A m.unfold bindO.induction m.unfold retO.reflexivity.reflexivity.Qed.(* (m &gt;&gt;= f) &gt;&gt;= g = m &gt;&gt;= (\x -&gt; f x &gt;&gt;= g) *)Theorem third_law_opt: forall (A B C : Set) (m:option A) (a:A) (f : A -&gt; option B) (g : B -&gt; option C), bindO B C (bindO A B m f) g = bindO A C m (fun x =&gt; bindO B C (f x) g).intros A B C m a f g.induction m.unfold bindO.reflexivity.unfold bindO.reflexivity.Qed.End MaybeMonad.

I reiterate my statement that Coq is the best computer game I've ever played. 