在 Coq 中定义 Maybe monad答案

【问题标题】：Defining Maybe monad in Coq在 Coq 中定义 Maybe monad
【发布时间】：2014-03-09 10:38:48
【问题描述】：

我想在 Coq 中使用类型类来定义 Maybe monad。 Monad 继承 Functor。

我想证明Some (f x') = fmap f (Some x')，这是单子定律之一。我使用了compute、reflexivity 和destruct option_functor，但我无法证明。我不能适当地简化fmap。

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.

【问题讨论】：

标签： monads typeclass functor coq theorem-proving

【解决方案1】：

您的问题源于您使用 Qed 而不是 Defined 结束了 option_function 的定义。

使用Qed，您以某种方式“隐藏”了fmap 的内部结构。然后你不能再展开它的定义（例如使用unfold 和simpl 策略）。使用 Defined 而不是 Qed 可以告诉 Coq 你打算使用 fmap 后者的定义，所以它应该是可展开的。

【讨论】：