如何在Coq中证明~(exists x:D, ~ R x)->(forall y:D, R y)定理

你要证明的是经典谓词逻辑中的量词德摩根律，Coq 默认使用直觉主义逻辑，无法直接证明该命题，需要引入经典逻辑的排中律支持。

你原有代码中声明的全局x、y参数是多余的，可以直接删除，避免和引理内部的约束变量产生重名冲突。

完整的证明代码如下：

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

Parameter D: Set.
Parameter R: D->Prop.

Lemma b:  ~(exists x:D, ~ (R x))->(forall y:D, (R y)).
Proof.
  intros H y.              (* 引入蕴含左前提H，以及全称量词的任意个体y *)
  destruct (classic (R y)) as [HR | HnR].
                           (* 调用排中律，分R y成立、不成立两种情况讨论 *)
  - exact HR.              (* 情况1：R y已经成立，直接返回该事实即可 *)
  - exfalso.               (* 情况2：R y不成立，我们需要从前提导出矛盾 *)
    apply H.               (* 前提H是~(exists x:D, ~R x)，只要构造出符合条件的exists命题就能得到矛盾 *)
    exists y.              (* 取x为当前的y，我们正好有~R y的假设 *)
    exact HnR.             (* 匹配假设完成证明 *)
Qed.

如果你不想导入整个经典逻辑库，也可以手动声明排中律公理，效果完全一致：
Axiom classic : forall P:Prop, P \/ ~P.

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