证明函数如何证明？

Question

如果有人好心向我解释在以下简单案例中如何使用证明函数，这将有助于我理解“程序/证明”的并行性：

Theorem ex1: forall n:nat, 7*5 < n -> 6*6 <= n. 
Proof.
  intros.
  assumption.
Qed.

证明函数：

ex1 = fun (n : nat) (H : 7 * 5 < n) => H
     : forall n : nat, 7 * 5 < n -> 6 * 6 <= n

在证明过程中是否执行了证明功能？它的返回值是如何使用的？ 说ex1的返回值是forall n : nat, 7 * 5 < n -> 6 * 6 <= n类型的实例对吗？

Answer 1

说ex1的返回值是forall n : nat, 7 * 5 < n -> 6 * 6 <= n类型的实例对吗？

不完全是。更正确的说法是ex1 的返回类型是6 * 6 <= n，其中n 是传递给ex1 的第一个参数，或者ex1 的类型为forall n, 7 * 5 < n -> 6 * 6 <= n。

证明过程中是否执行了证明功能？

不一定。这里的执行意味着“简化”或“规范化”。由证明建立的术语通常不会被简化。例如：

Theorem foo : True.
Proof.
assert (H : True -> True).
{ intros H'. exact H'. }
apply H.
exact I. (* I is a proof of True *)
Qed.

Print foo.

(* foo = let H : True -> True := fun H' : True => H' in 
         H I *)

简化这个证明意味着用fun H' : True => H' 替换H 并减少应用程序，这会产生I。你可以通过让 Coq 计算这个项来看到这一点：

Compute let H : True -> True := fun H' : True => H' in H I.
(* = I : True *)

然而：

它的返回值是如何使用的？

你在 Coq 中输入的每一个证明都会经过类型检查步骤以确保它是正确的。类型检查器所做的一件事是在比较它们的类型时简化术语。在 Coq 中，计算到相同范式的两个项被认为是相等的。结果中给出的术语H 的类型为7 * 5 < n。但是a < b被定义为S a <= b；因此我们也可以将H 视为具有S (7 * 5) <= n 类型。 Coq 现在需要确保 H 具有 6 * 6 <= n 类型，因为这两个下限计算为 36。因此，当您在 Coq 中输入证明时会发生计算，但计算是由类型执行的-checker，而不是证明项（即使证明项确实具有计算行为）。