在Coq中作为功能的含义？

Question

我读过那个含意是功能。但我很难理解上面提到的页面中给出的例子：

蕴涵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

如果要查看函数的协域，则必须将该函数应用于值，如下所示：

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

如果您想查看函数的图像/输出，Print将无助于您。你需要的是Compute。Compute使用一个术语(例如函数应用程序)并尽可能地减少它：

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