如何从 Coq 中的见证人引入新的存在条件？

Question

我的问题是关于如何在 conditions/hypotheses 的集合中构造一个 exist 项。

我有以下中间证明状态：

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

在我心里，我知道因为H0，x是(exists x : X, P x -> False)的见证，我想介绍一个名字：

w: (exists x : X, P x -> False)

根据上面的推理再和apply H in w一起使用，在假设中生成一个False，最后inversion得到False.

但是我不知道用什么tactic/syntax来介绍上面的见证人w。到目前为止我能达到的最好结果是 Check (ex_intro _ (fun x => P x -> False) x H0)). 给出 False.

谁能解释一下如何引入存在条件，或者另一种方法来完成证明？

谢谢。

P.S。我要证明的整个定理是：

Theorem not_exists_dist :
  excluded_middle ->
  forall (X:Type) (P : X -> Prop),
    ~ (exists x, ~ P x) -> (forall x, P x).
Proof.
  unfold excluded_middle. unfold not. 
  intros exm X P H x.

  destruct (exm (P x)).
    apply H0.
    Check (H (ex_intro _ (fun x => P x -> False)  x H0)).

Answer 1

您可以使用 assert 策略：

assert(w: exists x, P x -> False).

它会要求你在一个新的子目标中证明这个陈述，并将w添加到你现有的目标中。对于这种平凡的证明，可以直接内联证明：

assert(w: exists x, P x -> False) by (exists x; exact H0).

Answer 2

在这里，由于您已经知道如何构造 False 类型的术语，因此您可以使用 pose proof 将其添加到上下文中。这给出：

pose proof (H (ex_intro (fun x => P x -> False)  x H0))

你甚至可以直接破坏这个词，这就解决了目标。

destruct (H (ex_intro (fun x => P x -> False)  x H0))

完成证明的另一种方法是证明 False。您可以使用 exfalso 或 contradiction 等策略将目标更改为 False。通过这种方法，您可以使用 _ -> False 形式的假设，否则难以操纵。为了你的证明，你可以写：

exfalso. apply H. (* or directly, contradiction H *)
exists x. assumption.

如何从 Coq 中的见证人引入新的存在条件？

How to introduce a new existential condition from a witness in Coq?

coq

coq-tactic