Coq证明选择monad是应用程序和monad

我对coq很新颖，迄今为止我设法证明了我也可以通过手工证明的东西。所以当我遇到Selection monad并决定在haskell中实现它时，我认为这将是一个很好的练习，但我被卡住了。有人能提供一个coq证明的例子，说明选择monad是应用程序和monad吗？这是一个函数的haskell实现。Coq证明选择monad是应用程序和monad

newtype Sel r a = Sel { runSel :: (a -> r) -> a } 

instance Functor (Sel r) where 
    fmap ab (Sel ara) = Sel (ab . ara . (. ab))

额外的感谢，如果你也能也证明了单子法律。

编辑：这是我的证明函子存在：

Definition sel (R A : Type) := (A -> R) -> A. 

Theorem functor_exists : forall (R A B : Type), 
    (A -> B) -> sel R A -> sel R B. 
    intros R A B. unfold sel. intros AB ARA BR. 
    apply AB. apply ARA. intro. apply BR. apply AB. exact X. 
    Qed.

来源

2017-02-09 fakedrake

当我第一次开始使用勒柯克，我重新实现的定义和引理从这个[“教程”（https://pdp7.org/blog/2011/01/the-maybe-monad-in- coq /），然后切换到其他（更有趣）monad。 – ichistmeinname

我已经完成了这些，但我似乎无法做到超出这一点。我认为这对一个经验丰富的coq-ist来说很简单，这就是我发布的原因，但我可能是错的。 – fakedrake

但是我猜你可以提供Coq代码，这样你就可以看到你陷入困境的具体情况了吗？ – ichistmeinname

您不必使用的战术，因为它是勒柯克：你可以使用它作为一种方式，是相当类似的编程语言哈斯克尔。

首先，因为R将是一个变量出现所有的时间在本节中，我们可以使符号通过一次提到它有点轻，为所有：

Section SelMon. 
Variable (R : Type).

然后我们就可以复制你的定义sel（没有R变量，因为它已经在上下文中）。并写fmap作为一个很好的定义，而不是使用的战术证明：

Definition sel (A : Type) := (A -> R) -> A. 

Definition fmap {A B : Type} (f : A -> B) (s : sel A) : sel B := 
    fun br => f (s (fun a => br (f a))).

下一步要证明你有一个应用性是提供pure方法。那很简单：我们可以使用一个常量函数。

Definition pure {A : Type} (a : A) : sel A := 
    fun _ => a.

然后它变得有点毛茸茸的。我建议你先从join，然后利用得出的规范结构bind（并从中app）：

Definition join {A : Type} (ssa : sel (sel A)) : sel A. 
Admitted. 

Definition bind {A B : Type} (sa : sel A) (asb : A -> sel B) : sel B. 
Admitted. 

Definition app {A B : Type} (sab : sel (A -> B)) (sa : sel A) : sel B. 
Admitted.

一旦你与这些完成后，你可以关闭部分和R将作为一个参数给你所有的定义。

End SelMon.

来源

2017-02-09 20:01:56 gallais

有趣。 coq的许多功能我不知道如此谢谢。你认为这也会证明相关法律有多难？ – fakedrake

相关法律（严格意义上的解释）很可能不可证明，因为'sel A'是一个函数空间。如果你愿意承担功能的扩展性，并且你已经知道一个笔和纸的证明，它不应该太糟糕。 – gallais

你说得对，谢谢。为了将来的参考，[HoTT书籍]（https://hott.github.io/book/nightly/hott-online-1075-g3c53219.pdf）第1章末尾的注释清楚了整个问题。 – fakedrake

Coq证明选择monad是应用程序和monad

回答

相关问题