Доказательство продолжения перехода Монада в Coq

Question

Я пытаюсь доказать законы Монады (левая и правая единица + ассоциативность) для продолжения стиля перехода (CPS) Monad.

Я использую тип класса на основе Монада Defintion от https://coq.inria.fr/cocorico/AUGER_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). 

Конструктор типа КПС от 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 

Был бы очень благодарен за помощь!

EDIT: András Kovács указал, что эта конверсия в контроле типа достаточна, поэтому достаточно 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) 
    |}. 

Answer 1

Решение, как упомянуто в comment по András Kovács мар 11 12:26, ​​является

Может быть, вы может попытаться пойти прямо на рефлексивность? Из Coq 8.5 есть эта конверсия для записей, поэтому все законы должны быть очевидны немедленно путем нормализации и преобразования эта.

Это дает нам следующий пример:

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