证明函数如何证明？

Question

如果有人能给我解释一下证明函数在下面这个简单的案例中是如何使用的，这将有助于我对'programsproofs'并行的理解。

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 *)

简化这个证明的意思是： H 由 fun H' : True => 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 中输入证明时，有计算发生，但计算是由类型检查器执行的，而不是由证明项执行的（尽管证明项确实有计算行为）。