CoqのN個の要素のすべての関数を含む型

Question

私はCoqを学習しており、練習としてタイプFnArity (N:nat)をすべての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). 

は動作しないようにしてください。

これは教育目的のためのもので、関連するリソースは大歓迎です。

EDITは： 作曲N組成演算子をgはNを期待fとgを構成する組成演算子に相当します。これまでの回答から、私はおそらくので、ここで間違ってこれを近づいています、私は証明しようとしている命題があると認識します議論

(.).(.) ... 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のための一般的な定理を定義することです。

Answer 1

あなたが書き留めた型は、あなたの問題で明示したとおりではありません。forall A B C, A -> B -> Cは、3つの引数のすべての関数の型ではなく、2つの引数の特定の多型関数の型です。おそらく、A、B、およびCがのようなものがと数値化された{ A & { B & { C & A -> B -> C }}}のようなものを書くことを意味します。また、Checkコマンドを使用する代わりに、Compute (FnArity 3)と言うこともあります。これは、後者が用語を評価するコマンドであるためです（指摘したように、あなたが最初に書いたタイプを持つ用語はありません）。

ここに、あなたが望むことをするコードがあります。私たちは、リストに指定された引数を持つ関数型を計算する関数FnArityAux1 : list Type -> Type -> Typeを書き込むことによって開始します。たとえば、FnArityAux1 [nat; bool] boolはnat -> bool -> boolと評価さ

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

。次のように私たちは、その後、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. 

この定義では、我々は目的これまでに生成されたすべての存在量化タイプを持ち歩くことです引数argsを持つ別の補助機能FnArityAux2を使用しています。それぞれの "反復ステップ"については、別のタイプのTを定量化し、そのタイプを引数のリストに追加して再帰します。再帰が終了すると、FnArityAux1を使用して、すべての累積型を単一の関数型に結合します。次に、空のリストでプロセスを開始するだけで、つまり量的な型がまったくないことによって、FnArityを定義することができます。

Answer 2

いいえ、(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).は決して動作しません。