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

回答

相關問題