在Coq中使用假设的逆否命题：相关操作方法咨询

当前证明状态：

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

1. 创建H的逆否命题假设 #

要得到~(exists z : Entity, P z x /\ ~ O z x) -> P x x这个逆否命题假设，有几种实现方式：

• 借助contrapositive策略（需先导入经典逻辑库）：

Require Import Coq.Logic.Classical_Prop.

assert (H_contra : ~ (exists z : Entity, P z x /\ ~ O z x) -> P x x).
{ apply contrapositive. exact H. }

• 手动构造证明逻辑：

assert (H_contra : ~ (exists z : Entity, P z x /\ ~ O z x) -> P x x).
{ intro H_no_exists.
  apply (not_not_intro (P x x)).
  intro H_not_Pxx.
  apply H_no_exists.
  apply H. exact H_not_Pxx. }

• 用自动策略快速推导：

assert (H_contra : ~ (exists z : Entity, P z x /\ ~ O z x) -> P x x).
{ tauto. }

添加假设后执行apply H_contra.，即可将目标转换为~ exists z : Entity, P z x /\ ~ O z x。

2. 将存在命题的否定转换为全称析取命题 #

要把~ exists z : Entity, P z x /\ ~ O z x改写为forall z : Entity, ~ P z x \/ O z x，可分两步利用逻辑等价规则：

1. 将存在的否定转换为全称的否定：

apply not_exists_all_not.

此时目标变为forall z : Entity, ~ (P z x /\ ~ O z x)。

2. 应用德摩根定律将合取的否定转换为析取：

intros z. apply de_morgan_not_and.

最终目标就变为forall z : Entity, ~ P z x \/ O z x。

如果不需要分步操作，也可以用自动策略一步完成转换：

firstorder.

内容的提问来源于stack exchange，提问作者Lepticed