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'。根据您的代码段，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 中类型和命题的含义有点困惑。你说：

This seems puzzling: one can apply f to x but still can't obtain a witness y: f x that he has done so.

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

Coq：证明应用程序

Coq: Proving an application

function

definition

coq

proof