目标状态 Coq 为真

Question

在

Software Foundations Volume 1, Logic.v 中尝试证明 

All 时，我遇到了一个简单的

True

的证明状态。 IE。我的证明状态如下：

T : Type 
P : T -> Prop
H : forall x : T, False -> P 
==================================
(1/1)
True 

我知道只需使用

reflexivity

就可以实现我的目标。但是，我不明白为什么，也不明白证明状态只是

True

意味着什么。这是什么意思？为什么反身性在这里起作用？

Answer 1

您可以要求 Coq 打印任何术语的定义：

Print True.

回复是：

Inductive True : Prop :=  I : True.

从这个响应中，我们看到

True

是一个命题，而

I

是（法定的）

True

的证明。

当您在上面的上下文中有类似

H : forall x : T, False -> P

的内容时，这意味着

H

是

forall x : T, False -> P

的证明，因此，如果您的目标是

forall x : T, False -> P

那么您可以使用命令

exact H.

证明这个目标

一般来说，只要你有

H : P

，那么

H

就是

P

的证明。

因此，在这种情况下，你有

I : True

，你的目标是

True

，所以你可以使用命令

exact I.

来证明这个目标