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

您可以实例化通用量化 x在 H与 specialize ( specialize (H x) )。