了解Show Proof上的COQ证明.

Question

我是COQ的新手,我试图证明反例定理.

Variable A B:Prop.

Hypothesis R1: ~A->B.
Hypothesis R2: ~B.

Theorem ej: A.

当我们研究逻辑时,我们学习了RAA技术,但在COQ中,这并没有增加新的假设,现在我们陷入困境.

那么我们尝试:

Proof.
tauto.
Show Proof.

有了以下输出,但我们不知道它是什么意思.

(NNPP A
   (fun H : ~ A => let H0 : B := R1 H in let H1 : False := R2 H0 in False_ind False H1))

有人可以帮我们理解COQ Show Proof输出吗？

Answer 1

Coq在Curry-Howard对应之后代表了作为函数式编程语言程序的证明.这些程序是通过将Coq逻辑的原语与用户证明的公理和定理相结合而编写的.你看到的输出是一个"程序",它调用NNPP两个参数,即命题A和匿名函数的公理fun H : ~ A => ....公理NNPP是通常在矛盾证据中使用的双重否定消除原则.如果您键入Check NNPP.,勒柯克告诉你,它的类型是forall P : Prop, ~ ~ P -> P,这意味着,给定任意命题P和任何证明H的~ ~ P,NNPP P H就是一个证明P.Coq在上面构建的功能术语fun H : ~ A => ...恰好是~ ~ A使用您声明的假设的Coq证明.

我不知道您对Coq和函数式编程有多少先前的经验,但是看看Software Foundations的书籍系列可能会有所帮助,该系列文章全面介绍了Coq.特别是," 证明对象"一章描述了如何表示Coq证明.