類型包含Coq中的N個元素的所有功能

我正在學習Coq並且作爲練習我想定義一個類型FnArity (N:nat)來編碼所有函數的N參數。那就是：類型包含Coq中的N個元素的所有功能

Check FnArity 3 : (forall A B C : Set, A -> B -> C).

應該工作，但

Check FnArity 2 : (forall A B C D : Set, A -> B -> C -> D).

不應該工作。

這是爲了教學目的，所以任何相關的資源是值得歡迎的。

編輯：從到目前爲止的答案我意識到我可能接近這個錯了，所以這裏是我想證明的命題：創作ň組成運營商就相當於對構成f和g組成算哪裏g預計ñ參數。在Haskell上下的術語：

(.).(.) ... N times ... (.).(.) f g = \a1, .. aN -> f (g (a1, .. , aN))

EDIT2：在COQ方面：

Definition compose { A B C : Type } (F : C -> B) (G : A -> C) : A -> B := 
    fun x => F (G (x)). 

Definition compose2 {A1 A2 B C : Type} (F : C -> B) (G : A1 -> A2 -> C) 
: A1 -> A2 -> B := fun x y => F (G x y). 

Definition compose3 {A1 A2 A3 B C : Type} (F : C -> B) (G : A1 -> A2 -> A3 -> C) 
: A1 -> A2 -> A3 -> B := fun x y z => F (G x y z). 

(* The simplest case *) 
Theorem dual_compose : forall {A B C D : Type} (f: D -> C) (g : A -> B -> D) , 
         (compose compose compose) f g = compose2 f g. 
Proof. reflexivity. Qed. 

Theorem triple_compose : forall {A1 A2 A3 B C : Type} (f: C -> B) (g : A1 -> A2 -> A3 -> C) , 
         (compose (compose (compose) compose) compose) f g = 
         compose3 f g.

我想是定義廣義定理composeN。

來源

2016-04-03 fakedrake

您記下的類型並不完全代表您在問題中陳述的內容：forall A B C, A -> B -> C不是三個參數的所有函數的類型，而是兩個參數的某些多態函數的類型。你可能打算寫下類似{ A & { B & { C & A -> B -> C }}}的東西，其中A，B和C都是存在量化。你可能也想說Compute (FnArity 3)而不是使用Check命令，因爲後者是評估一個術語的術語（並且，正如jbapple指出的那樣，沒有術語可以具有你最初編寫的類型）。

下面是一段代碼，它可以實現你想要的，我想。首先，我們寫一個函數FnArityAux1 : list Type -> Type -> Type，計算某個函數類型與列表上給出的參數：

Fixpoint FnArityAux1 (args : list Type) (res : Type) : Type := 
    match args with 
    | [] => res 
    | T :: args' => T -> FnArityAux1 args' res 
    end.

例如，FnArityAux1 [nat; bool] bool評估爲nat -> bool -> bool。然後，我們可以用這個功能來定義FnArity如下：

Fixpoint FnArityAux2 (args : list Type) (n : nat) : Type := 
    match n with 
    | 0 => { T : Type & FnArityAux1 args T } 
    | S n' => { T : Type & FnArityAux2 (args ++ [T]) n' } 
    end. 

Definition FnArity n := FnArityAux2 [] n.

在這個定義中，我們用另一種輔助功能FnArityAux2有一個參數args其目的是隨身攜帶的所有迄今生產的存在性量化類型。對於每個「迭代步驟」，它會量化另一種類型T，將該類型添加到參數列表中，並遞歸。當遞歸結束時，我們使用FnArityAux1將所有累積類型合併爲一個函數類型。然後，我們可以簡單地通過一個空列表來啓動進程來定義FnArity - 也就是說，根本沒有量化類型。

來源

2016-04-03 18:40:04

你確實似乎回答我的問題，但我不能讓派生類型爲我的問題工作。你能檢查我的編輯並修改你的回答評論嗎？ – fakedrake

@fakedrake在這種情況下，你可能只需要'FnArityAux1'類型。我會看看我能不能拿出一些東西。 –

另外''符號是什麼意思。我認爲它是某種中綴存在量詞，但我找不到有關它的文檔？ – fakedrake

不，這是不可能的，因爲(forall A B C : Set, A -> B -> C)是無人居住的。

Goal (forall A B C : Set, A -> B -> C) -> False. 
intros f. 
specialize (f True True False). 
apply f; trivial. 
Qed.

因此，Check FnArity 3 : (forall A B C : Set, A -> B -> C).永遠不能工作。

來源

2016-04-03 18:33:49 jbapple

類型包含Coq中的N個元素的所有功能

回答

相關問題