Coq：证明应用程序

Question

这是一个有点理论的问题。我们可以定义fx，但貌似不能定义fx'：

Function fx {A} (x:A) (f:A->Type) (g:Type->f x): f x := g (f x).
Definition fx' {A} (x:A) (f:A->Type): f x.

在某种程度上，这是有道理的，因为无法从f 和x 证明f 已经（或将）应用于x。但是我们可以将f 应用到x 以获得Type 类型的东西：

assert (h := f x).

这似乎令人费解：一个人可以将f 应用于x，但仍然无法让y: f x 证明他已经这样做了。

我能想到的唯一解释是：作为一个类型，f x 是一个应用程序，作为一个术语，它只是一个类型。我们不能从类型推断过去的应用程序；同样，我们不能从函数及其潜在参数推断未来的应用程序。至于应用本身（实例），它不是证明中的一个阶段，所以我们不能有它的见证。但我只是猜测。问题：

是否可以定义fx'？如果是，如何；如果不是，为什么（请给出理论上的解释）

Answer 1

首先，直接回答您的问题：否，无法定义fx'。根据你的 sn-p，fx' 应该有类型

forall (A : Type) (x : A) (f : A -> Type), f x.

不难看出fx' 的存在意味着矛盾，如下面的脚本所示。

Section Contra.

Variable fx' : forall (A : Type) (x : A) (f : A -> Type), f x.

Lemma contra : False.
Proof.
  exact (fx' unit tt (fun x => False)).
Qed.

End Contra.

这里发生了什么？ fx' 的类型表示对于由类型A 索引的任何类型f 家族，我们可以生成f x 的元素，其中x 是任意的。特别是，我们可以将f 视为(fun x => False) 类型的常量族，在这种情况下f x 与False 相同。 （注意False，除了是Prop的成员，也是Type的成员。）

现在，鉴于您的问题，我认为您对 Coq 中类型和命题的含义有些困惑。你说：

这似乎令人费解：可以将f 应用于x，但仍然无法获得 见证y: f x他已经这样做了。

我们可以将f 应用于x 的事实仅仅意味着表达式f x 具有有效类型，在本例中为Type。换句话说，Coq 显示f x : Type。但是拥有一个类型与被居住是不同的事情居住：当f 和x 是任意的时，不可能建立一个术语y 这样y : f x。特别是，我们有False : Type，但是我们无法用p : False 构建一个术语p，因为这意味着Coq 的逻辑是不一致的。