1

我读到影响是函数。但是我很难理解上述页面中给出的示例：

蕴涵 P → Q 的证明项是将 P 的证据作为输入并产生 Q 的证据作为其输出的函数。

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

我们可以看到，上述引理的证明项确实是一个函数：

打印 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 打印显示函数 image 是eq_refl : 1 + 1 = 2 -> 0 * 3 = 0，而不是eq_refl: 0 * 3 = 0。我不明白为什么假设1 + 1 = 2应该出现在输出中。谁能帮忙解释这里发生了什么？

谢谢。

4

1 回答 1

2

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

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

我想你误解了这个Print命令。Print显示与定义关联的术语以及定义的类型。它不显示函数的图像/输出。

例如，以下打印 value 的定义和类型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
于 2015-09-26T18:10:28.210 回答