coq - 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 以便我可以推断： px ？

Answer 1

您可以用( )实例化普遍量化x的 in 。 Hspecializespecialize (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.