The Maybe monad is pretty useful whenever you're dealing with partial functions, especially in a language like Coq (or rather Gallina if you want to be exact) which requires all functions to be total.

The first idea is a to lift the codomain of a partial function \(f : A \rightharpoonup B\) by including a special value \(\bot\) such that \(f^\prime : A \rightarrow B \cup \{\bot\}\) is a total function. In Haskell you'll find that the type Maybe B plays the role of the lifted codomain \(B \cup \{\bot\}\). But enough mathematical foreplay, let's get to it:

In Haskell the Maybe monad is part of the standard library.

data Maybe t = Just t | Nothing

instance Monad Maybe where
  return = Just
  (Just x) >>= k = k x
  Nothing >>= k = Nothing

Coq's standard library also includes the datatype Maybe, but there it is called option.

Inductive option (A : Type) :=
| Some : A -> option A
| None : option A.

In order to make working with this type a little more enjoyable and the resulting code more readable, we declare the type argument of its constructors to be implicit which means that they should be inferred from the context:

Inductive option (A : Type) :=
Arguments Some [A] _.
Arguments None [A].

Now we can define the monad operations return (which we'll call ret to avoid confusion with the keyword of the same name) and >>= (which is also called bind).

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

Definition bind {A B : Type} (a : option A) (f : A -> option B) : option B :=
  match a with
    | Some x => f x
    | None => None
  end.

We can also define the usual notations for use in monadic code. First, the familiar infix operator for the bind operation.

Notation "A >>= F" := (bind A F) (at level 42, left associativity).

Followed by the beloved do-notation from Haskell.

Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200).

We could stop here, but because Coq is also a thereom prover and not only a fancy dependently typed functional programming language, we go right on and prove the three laws that each monad has to satisfy in order to be called a monad at all. Recall from any Haskell text that the monad laws are, in order:

• left identity: \(\mathrm{return}\;a \gg\!= f = f\;a\)
• right identity: \(a \gg\!= \mathrm{return} = a\)
• associativity: \((a \gg\!= f) \gg\!= g = a \gg\!= (\lambda x\,.\, f\;x \gg\!= g)\)

These laws correspond directly to the Coq lemmata mon_left_id, mon_right_id, and mon_assoc below. As you can see, the proofs in all three cases are rather trivial.

Lemma mon_left_id : forall (A B : Type) (a : A) (f : A -> option B),
  ret a >>= f = f a.
intros.
reflexivity.
Qed.

Lemma mon_right_id : forall (A : Type) (a : option A),
  a >>= ret = a.
intros.
induction a; repeat reflexivity.
Qed.

Lemma mon_assoc :
  forall (A B C : Type) (a : option A) (f : A -> option B) (g : B -> option C),
    (a >>= f) >>= g = a >>= (fun x => f x >>= g).
intros.
induction a; repeat reflexivity.
Qed.

That's is, have some fun with the Maybe monad in Coq!