Coq定理证明疑问：为何此处无法使用destruct或discriminate？

定理定义与当前证明进度 #

Definition excluded_middle := forall P : Prop,
  P \/ ~ P.

Theorem not_exists_dist :
  excluded_middle ->
  forall (X:Type) (P : X -> Prop),
    ~ (exists x, ~ P x) -> (forall x, P x).
Proof.
  intros.
  unfold excluded_middle in H.
  unfold not in H0.
  unfold not in H.
  assert (P x \/ ~ P x).
  apply H.
  destruct H1.
  - apply H1.
  - unfold not in H1. 

当前证明目标 #

1 goal
H : forall P : Prop, P \/ (P -> False)
X : Type
P : X -> Prop
H0 : (exists x : X, P x -> False) -> False
x : X
H1 : P x -> False
______________________________________(1/1)
P x

问题 #

• 当目标形如H -> False且假设中存在False时，我通常会使用discriminate或destruct。但现在假设中有H1: P x -> False，目标是P x，为何无法再使用这两个策略？
• 我知道可以用exfalso，但我认为exfalso本质是引入False后再destruct，想问是否有不用assert仅用destruct类策略的解决办法？

解答 #

为什么discriminate/destruct无效？ #

• discriminate仅用于处理归纳类型构造子的矛盾（比如0 = S n这类等式冲突），当前场景只有命题逻辑层面的蕴含、否定，没有构造子层面的冲突，因此discriminate完全不适用。
• destruct的核心是拆分归纳类型结构：
  • 若对H1: P x -> False使用destruct，需要先提供P x的证明，但这正是当前目标，直接陷入循环；
  • 若对目标P x使用destruct，P x不是归纳类型，没有可拆分的结构，因此destruct也无法生效。

不用assert的替代方案 #

不需要额外assert，直接利用现有假设的结构就能完成证明：

- apply H0.
  exists x.
  apply H1.

如果一定要贴合destruct类策略的思路，可以直接拆分排中律实例，省去单独的assert步骤：
在intros之后，替换原有的assert步骤，直接执行：

intros.
destruct (H (P x)) as [H1|H1].
- apply H1.
- apply H0.
  exists x.
  apply H1.

这里的destruct (H (P x))直接拆分了P x对应的排中律实例，和原证明思路一致但省去了显式assert。

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