Тип, содержащий все функции N элементов в Coq

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 операторов состава эквивалентно оператору состава, который сочиняет f и g где g ожидает N аргументы. В 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.

Answer 1

Типы, которые вы написали, не совсем представляют то, что вы указали в своей проблеме: 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, просто запустив процесс с пустым списком - то есть без каких-либо количественно типов.

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). не может работать.