我正在努力证明以下定理（假设非空域）：
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， wherec是一个常数。即forall量词将被淘汰。一旦完成，我将再次推断exists a，我的简单证明将被Qed编辑。
但是，我找不到forall在 Coq 中消除 on 的正确方法。
我是新手，我想知道如何forall在 Coq 中消除或证明上述定理的更好方法是什么？
PS 我看过这个答案，但它似乎与我的问题无关。
与其他逻辑形式（例如 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.
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句