coq：消除forall量词

Question

我要证明以下定理：

Theorem Frobenius (A: Set) (q: Prop) (p: A -> Prop) :
  (q \/ forall x : A, p x) -> (forall x : A, q \/ p x).

我已经得到以下证明：

Proof.
intro.
intro.
destruct H.
left.
assumption.

但现在我不知道该怎么办。以下内容可供我使用：

A : Set
q : Prop
p : A -> Prop
H : forall x : A, p x
x : A

我想证明以下子目标：

q \/ p x

如何消除给定前提中的 forall 量词

forall x : A, p x

也就是说：我怎样才能插入我的具体 x : A 以便我可以推断： p x ？

Answer 1

您可以使用specialize (specialize (H x)) 实例化H 中的通用量化x。

Answer 2

可能是最简单的？

Theorem Frobenius (A: Set) (q: Prop) (p: A -> Prop) :
  (q \/ forall x : A, p x) -> (forall x : A, q \/ p x).
intro H.

elim H.
intros Hl x.
left.
exact Hl.

intros Hr x.
right.
apply Hr.