monads - 在 Coq 中证明延续传递式 Monad

Question

我正在尝试证明 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关于Compile-time parsing在 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_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;应用 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)
  |}.

Answer 1

解决方案，如comment中所述通过 András Kovács 3 月 11 日 12:26，是

Maybe you could try going straight for reflexivity? From Coq 8.5 there's eta conversion for records, so all the laws should be apparent immediately by normalization and eta conversion.

这为我们提供了以下实例:

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
  |}.