在 Coq 中作为函数的含义？

Question

我读到 implications are functions。但是我很难理解上述页面中给出的示例：

The proof term for an implication P → Q is a function that takes evidence for P as input and produces evidence for Q as its output.

Lemma silly_implication : (1 + 1) = 2 → 0 × 3 = 0. Proof. intros H. reflexivity. Qed.

We can see that the proof term for the above lemma is indeed a function:

Print silly_implication. (* ===> silly_implication = fun _ : 1 + 1 = 2 => eq_refl : 1 + 1 = 2 -> 0 * 3 = 0 *)

的确，这是一个函数。但它的类型对我来说不合适。根据我的阅读，P -> Q 的证明项应该是一个函数，其输出为 Q 的证据。那么，(1+1) = 2 -> 0*3 = 0的输出应该单独作为0*3 = 0的证据吧？

但是上面的 Coq 打印显示函数图像是 eq_refl : 1 + 1 = 2 -> 0 * 3 = 0，而不是 eq_refl: 0 * 3 = 0。我不明白为什么假设 1 + 1 = 2 应该出现在输出中。谁能帮忙解释一下这是怎么回事？

谢谢。

Answer 1

您的理解是正确的，直到：

But the Coq print out above shows that the function image is ...

我认为您误解了 Print 命令。 Print 向您显示与定义关联的术语以及定义的类型。它 而不是 显示函数的 image/output。

例如，下面打印值 x 的定义和类型：

Definition x := 5.
Print x.
> x = 5 
>   : nat

同样，下面打印函数的定义和类型f：

Definition f := fun n => n + 2.
Print f.
> f = fun n : nat => n + 2
>   : nat -> nat

如果要查看函数的密码域，必须将函数应用于某个值，如下所示：

Definition fx := f x.
Print fx.
> fx = f x
>    : nat

如果您想查看函数的 image/output，Print 帮不了您。你需要的是Compute。 Compute 获取一个术语（例如函数应用程序）并尽可能减少它：

Compute (f x).
> = 7
> : nat

在 Coq 中作为函数的含义？

Implications as functions in Coq?

logic

coq

curry-howard