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.
