如何在Coq中不使用自动化tactic证明这条德摩根定律？

核心前提说明 #

你当前卡在反向证明（从~ (forall x, p x)推导exists x, ~ p x）的步骤，这个方向在Coq默认的构造主义逻辑中无法直接证明，必须引入排中律公理才能完成。如果你不允许使用经典逻辑公理，该命题是不可证明的。

完整可运行证明代码 #

(* 导入经典逻辑库，获取排中律支持 *)
Require Import Classical.

Goal forall (X : Type) (p : X -> Prop), (exists x, ~ p x) <-> ~ (forall x, p x).
Proof. 
  intros. split.
  - (* 正向证明你已经完成，无需修改 *)
    intros. destruct H as [x H]. intros nh. apply H. apply (nh x).
  - (* 反向证明补全步骤 *)
    intros H.
    destruct (classic (exists x, ~ p x)) as [H_ex | H_not_ex].
    + (* 情况1：目标命题已经成立，直接取用 *)
      exact H_ex.
    + (* 情况2：目标命题不成立，走反证法推导矛盾 *)
      exfalso. apply H.
      intros x.
      destruct (classic (p x)) as [Hpx | Hnpx].
      * (* p x成立的情况直接返回结果 *)
        exact Hpx.
      * (* p x不成立的情况，和H_not_ex矛盾直接结束分支 *)
        contradiction H_not_ex. exists x. exact Hnpx.
Qed.

反向分支步骤逻辑说明 #

1. 用destruct (classic (exists x, ~ p x))对要证明的目标做排中判断，拆分出两种情况
2. 第一种情况目标已经成立，直接用exact取假设即可
3. 第二种情况拿到~ (exists x, ~ p x)的假设后，走反证路线：
   • exfalso把目标替换为证明矛盾
   • apply H将矛盾来源转为需要证明forall x, p x（因为H是~ (forall x, p x)，只要构造出forall x, p x就能导出矛盾）
   • 对任意x再做一次排中判断p x是否成立：成立就直接返回；不成立就得到了满足~ p x的x，和~ (exists x, ~ p x)的假设矛盾，直接结束证明

内容的提问来源于stack exchange，提问作者Tyler's ruler