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 -> 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.

active directory applied formal logic ashurbanipal authentication books c c++ comics conference continuations coq data structure digital humanities Dijkstra eclipse virgo electronics emacs goodreads haskell http java job Knuth ldap link linux lisp math naming nimrod notation OpenAM osgi parsing pony programming language protocols python quote quotes R random REST ruby rust SAML scala scheme shell software development system administration theory tip toy problems unix vmware yeti
Member of The Internet Defense League
Site proudly generated by Hakyll.