Defining Maybe monad in Coq

Question

I want to define Maybe monad using type class in Coq. Monad inherits Functor.

I want to prove Some (f x') = fmap f (Some x'), which is one of the monad laws. I used compute, reflexivity and destruct option_functor, but I couldn't prove it. I can't simplify fmap appropriately.

Class Functor (F: Type -> Type) := {
   fmap : forall {A B}, (A -> B) -> (F A -> F B)
 ; homo_id : forall {A} (x : F A), x = fmap (fun x' => x') x
 ; homo_comp : forall {A B C} (f : A -> B) (g : B -> C) (x : F A),
     fmap (fun x' => g (f x')) x = fmap g (fmap f x)
}.

Class Monad (M: Type -> Type) := {
   functor :> Functor M
 ; unit : forall {A}, A -> M A
 ; join : forall {A}, M (M A) -> M A
 ; unit_nat : forall {A B} (f : A -> B) (x : A), unit (f x) = fmap f (unit x)
 ; join_nat : forall {A B} (f : A -> B) (x : M (M A)), join (fmap (fmap f) x) = fmap f (join x)
 ; identity : forall {A} (x : M A), join (unit x) = x /\ x = join (fmap unit x)
 ; associativity : forall {A} (x : M (M (M A))), join (join x) = join (fmap join x)
}.

Instance option_functor : Functor option := {
   fmap A B f x :=
     match x with
     | None => None
     | Some x' => Some (f x')
     end
}.
Proof.
  intros. destruct x; reflexivity.
  intros. destruct x; reflexivity.
Qed.

Instance option_monad : Monad option := {
   unit A x := Some x
 ; join A x :=
     match x with
     | Some (Some x') => Some x'
     | _ => None
     end
}.
Proof.
  Admitted.

Answer 1

Your problem arises from the fact that you ended the definition of the option_function with Qed instead of Defined.

Using Qed, you somehow 'hide' the internals of fmap. Then you can no longer unfold its definition (e.g. using the unfold and simpl tactics). Using Defined instead of Qed let you tell Coq that you intend to use the definition of fmap latter, so it should be unfoldable.