3

我正在尝试证明连续传递风格（CPS）Monad 的 Monad 定律（左右单位 + 关联性）。

我正在使用来自https://coq.inria.fr/cocorico/AUGER_Monad的基于类型类的 Monad 定义：

Class Monad (m: Type -> Type): Type :=
  {
    return_ {A}:     A -> m A;
    bind    {A B}:   m A -> (A -> m B) -> m B;

    right_unit {A}:  forall (a: m A), bind a return_ = a;
    left_unit  {A}:  forall (a: A) B (f: A -> m B),
                       bind (return_ a) f = f a;
    associativity {A B C}:
                     forall a (f: A -> m B) (g: B -> m C),
                       bind a (fun x => bind (f x) g) = bind (bind a f) g
}.

Notation "a >>= f" := (bind a f) (at level 50, left associativity).

CPS 类型构造函数来自 Ralf Hinze 的Functional Pearl关于编译时解析Haskell 中

Definition CPS (S:Type) := forall A, (S->A) -> A.

我定义bind并return_喜欢这个

Instance CPSMonad : Monad CPS  :=
  {|
    return_ := fun {A} a {B} => fun (f:A->B) => f a ;
    bind A B := fun (m:CPS A) (k: A -> CPS B)
      =>(fun C => (m _ (fun a => k a _))) : CPS B

  |}.

但我坚持对right_unitand的证明义务associativity。

- unfold CPS; intros.

规定义务right_unit：

  A : Type
  a : forall A0 : Type, (A -> A0) -> A0
  ============================
   (fun C : Type => a ((A -> C) -> C) (fun (a0 : A) (f : A -> C) => f a0)) = a

非常感谢您的帮助！

编辑：András Kovács 指出类型检查器中的 eta 转换就足够了，所以intros; apply eq_refl., 或reflexivity.就足够了。

首先，我必须更正我对bind. （无形的论点c是在错误的一面)......

Instance CPSMonad : Monad CPS  :=
  {|
    return_ S s A f     := f s ;
    bind    A B m k C c := m _ (fun a => k a _ c)
  |}.
4

1 回答 1

3

正如András Kovács在 3 月 11 日 12:26的评论中提到的那样，解决方案是

也许您可以尝试直接进行反身性？从 Coq 8.5 开始，记录有了 eta 转换，所以所有的规律都应该通过规范化和 eta 转换立即显现出来。

这给了我们以下实例：

Instance CPSMonad : Monad CPS  :=
  {|
    return_       S s A f :=     f s ;
    bind          A B m k C c := m _ (fun a => k a _ c) ;
    right_unit    A a :=         eq_refl ;
    left_unit     A a B f :=     eq_refl ;
    associativity A B C a f g := eq_refl
  |}.
于 2016-11-14T10:26:28.690 回答