假设对矛盾的证明否定

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.

我认为这应该有效.