在 Coq 中使用假设的对立面

Question

我目前的假设和目标是：

1 subgoal
x : Entity
H : ~ P x x -> exists z : Entity, P z x /\ ~ O z x
______________________________________(1/1)
P x x

我想应用H的对立面，我认为是

(~ exists z : Entity, P z x /\ ~ O z x) -> P x x

。我将获得目标

~ exists z : Entity, P z x /\ ~ O z x

，相当于

forall z : Entity, ~ P z x \/ O z x

.

我有几个问题：1）如何提出一个与H相反的新假设； 2）一旦我应用了逆势，如何将

~ exists z : Entity, P z x /\ ~ O z x

重写为

forall z : Entity, ~ P z x \/ O z x

？

Answer 1

我猜你在 Coq 中使用经典逻辑。

Require Import Classical.

Check imply_to_or.
Check not_ex_all_not.