Coq:去掉`forall`？

Question

我正在努力证明以下定理(假设域为非空域)：

Theorem t (A: Set) (P: A -> Prop): (forall a: A, P a) -> (exists a: A, P a).
Proof.
  intros H.

通常，有了forall a: A, P a，我会推导出P c，其中c是一个常量。即forall量词将被消除。一旦完成，我将再次推导exists a，并且我的简单证明将是Qeded。

然而，我找不到正确的方法来消除forall在Coq中的影响。

我是新手，我想知道如何消除Coq中的forall，或者证明上述定理的更好方法是什么？

附言:我已经看过this的答案了，但它似乎与我的问题无关。

Answer 1

与其他逻辑形式不同(例如Isabelle/HOL)，在Coq中完全有可能有一个空域。如果你想证明你的陈述，你必须明确地假设A不是空的。这里有一种可能性。

Definition non_empty (A : Type) : Prop :=
  exists x : A, True.

Theorem t (A : Set) (P : A -> Prop) :
  non_empty A ->
  (forall a : A, P a) ->
  (exists a : A, P a).
Proof.
intros [c _] H. exists c. apply H.
Qed.