継続渡しスタイル (CPS) モナドのモナド法則 (左右のユニット + 結合性) を証明しようとしています。
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 about Compile-time parsing in 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
助けてくれてとても感謝しています！
intros; apply eq_refl.編集: András Kovács は、型チェッカーでの eta 変換で十分であると指摘しました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)
|}.