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.在一个部分中，这样您就永远无法到达您不想到达的其他地方...

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

我认为这应该有效。