本文介绍了coq：消除forall量词的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！
问题描述
我想证明以下定理：
Theorem Frobenius (A: Set) (q: Prop) (p: A -> Prop) :
(q \/ forall x : A, p x) -> (forall x : A, q \/ p x).
我已经得到了以下证明：
I already got the following piece of the proof:
Proof.
intro.
intro.
destruct H.
left.
assumption.
但是现在我处在一个不知所措的境地。我可以处理以下事情：
But now I am in a situation I don't know what to do. The following things are at my disposal:
A : Set
q : Prop
p : A -> Prop
H : forall x : A, p x
x : A
想要证明以下子目标：
q \/ p x
如何消除给定前提下的全部量词
How can I eliminate the forall quantifier in the given premise
forall x : A, p x
即：如何插入我的具体x：A这样我可以推断出：px？
that is: How can I plug in my concrete x : A so that I can deduce: p x ?
推荐答案
您可以实例化通用量化的 x 在 H 中，并带有（ specialize（H x））。
You can instantiate the universally quantified x in H with specialize (specialize (H x)).
这篇关于coq：消除forall量词的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！