# Coq and The Maybe Monad

Posted on December 17, 2007
by Tommy McGuire

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.

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

Section MaybeMonad.

Definition retO (A:Set) (a:A) := Some a.

Definition bindO (A B : Set) (m:option A) (f:A -> option B)

:= match m with Some m' => f m' | None => None end.

(* return a >>= f = f a *)

Theorem first_law_opt :

forall (A B : Set) (a:A) (f:A -> option B),

bindO A B (retO A a) f = f a.

intros A B a f.

unfold bindO.

unfold retO.

reflexivity.

Qed.

(* (m >>= 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 >>= f) >>= g = m >>= (\x -> f x >>= g) *)

Theorem third_law_opt:

forall (A B C : Set) (m:option A) (a:A)

(f : A -> option B) (g : B -> option C),

bindO B C (bindO A B m f) g

= bindO A C m (fun x => 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.

Powered by ScribeFire.