Coq中包含N个元素所有函数的类型

Question

我正在学习 Coq，作为练习，我想定义一个类型 FnArity (N:nat) 来编码 all 个参数 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).

应该不行。

这是出于教学目的，欢迎任何相关资源。

编辑：从目前的答案来看，我意识到我可能正在接近这个错误，所以这是我试图证明的命题：组合 N 个组合运算符等同于组合 f 和 g 的组合运算符，其中 g 需要 N 个参数。在 haskell-ish 术语中：

(.).(.) ... 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 : 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). 永远行不通。

Answer 2

你写下的类型并不完全代表你在问题中所说的：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，其目的是携带到目前为止生成的所有存在量化类型。对于每个 "iteration step"，它量化另一种类型 T，将该类型添加到参数列表，然后递归。当递归结束时，我们使用 FnArityAux1 将所有累积的类型组合成一个函数类型。然后，我们可以简单地通过以空列表开始该过程来定义 FnArity —— 也就是说，根本没有量化类型。

Coq中包含N个元素所有函数的类型

Type that contains all functions of N elements in Coq

coq

theorem-proving