作为 Coq 中的函数的含义？

Question

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

蕴涵 P → Q 的证明项是一个函数 P 的证据作为输入，Q 的证据作为其输出。

引理 silly_implication : (1 + 1) = 2 → 0 × 3 = 0。证明。介绍 H。 反身性。 Qed。

我们可以看到，上述引理的证明项确实是 功能：

打印 silly_implication。 (* ===> silly_implication = 有趣 _ : 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

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

但上面的 Coq 打印显示函数图像是...

我认为您误解了Print 命令。 Print 显示与定义关联的术语以及定义的类型。它确实不显示函数的图像/输出。

例如，下面打印值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

如果你想查看函数的 codomain，你必须将函数应用到一个值上，像这样：

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

如果您想查看函数的图像/输出，Print 对您没有帮助。你需要的是Compute。 Compute 取一个术语（例如一个函数应用程序）并尽可能减少它：

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