option_monad.v

Definition bind_option (A: Type) (B: Type) (opt: option A) (f: A -> option B): option B :=
  match opt with
  | Some v => f v
  | None => None
  end.

Definition return_option (A: Type) (a: A) := Some a.

(* return a >>= f = f a *)
Theorem left_identity_option A B a f:
  bind_option A B (return_option A a) f = f a.
Proof.
  simpl.
  reflexivity.
Qed.

(* m >>= return = m *)
Theorem right_identity_option A m:
  bind_option A A m (return_option A) = m.
Proof.
  induction m.
  simpl.
  reflexivity.
  simpl.
  reflexivity.
Qed.

(*
 (m >>= f) >>= g = m >>= (\x -> (f x) >>= g)
 *)
Theorem associativity_option A B C opt f g:
  bind_option B C (bind_option A B opt f) g = 
    bind_option A C opt (fun x => bind_option B C (f x) g).
Proof.
  induction opt.
  simpl.
  reflexivity.
  simpl.
  reflexivity.
Qed.