假设对矛盾证明的否定

【问题标题】：Assume Negation for Proof by Contradiction假设对矛盾证明的否定
【发布时间】：2012-09-26 20:06:42
【问题描述】：

我有一堆规则，它们本质上意味着某些命题 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 *)

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

【问题讨论】：

标签： coq

【解决方案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.

我认为这应该可行。

【讨论】：