Coq 证明 Selection monad 是一个 applicative 和 monad

Question

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

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.

Answer 1

你不必使用策略，因为它是 Coq：你可以将它用作一种编程语言，其方式与 Haskell.

非常相似

首先，由于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.

Coq 证明 Selection monad 是一个 applicative 和 monad

Coq proof that the Selection monad is an applicative and a monad

functor

theorem-proving

coq

applicative