在 Coq 中证明延续传递风格 Monad答案

【问题标题】：Proving the Continuation Passing Style Monad in Coq在 Coq 中证明延续传递风格 Monad
【发布时间】：2016-03-11 10:38:26
【问题描述】：

我正在尝试证明 Continuation Passing Style (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 中的 Compile-time parsing

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_unit 和 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)
  |}.

【问题讨论】：

也许你可以尝试直接去reflexivity？从 Coq 8.5 开始，记录有了 eta 转换，所以所有的规律都应该通过规范化和 eta 转换立即显现出来。
谢谢！你是绝对正确的。它也适用于 8.4。
@larsr 想要回答您自己的问题并接受它，这样它就不会被标记为“未回答”？

标签： monads coq continuation-passing

【解决方案1】：

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

也许您可以尝试直接进行自反性？从 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
  |}.

【讨论】：