coq - 假设对矛盾证明的否定

Question

我有一堆规则，它们本质上意味着某些命题 P 永远不会为真。我现在必须使用 Coq 证明 P 是错误的。为了在纸面上这样做，我会假设 P 成立，然后得出矛盾，从而证明 P 不能成立。

我不太确定如何假设 P 支持这个证明，这就是我寻求帮助的原因。我当前的代码：

Variables {…} : Prop.
Hypothesis rule1 : … .
Hypothesis rule2 : … .
.
.
.
Hypothesis rule6 : … .
Variable s : P. (* Assume that P holds for proof by contradiction *)
(* other Coq commands *)
(* proof is done *)

有人可以确认我是否以正确的方式进行此操作（否则，我应该怎么做？）？

Answer 1

你要做的是证明：

Theorem notP := ~ P.

归结为：

Theorem notP := P -> False.

因此，对于 P 类型的变量，您需要证明目标为 False。

我相信你这样做的方式是可以接受的，尽管你可能想把它放在Variable s : p.一个部分中，这样你就永远无法在你不想的其他地方达到那个 s...

Section ProvingNotP.
Variable p : P.
Theorem notP: False.
Proof. ... Qed.
End ProvingNotP.

我认为这应该有效。