coq：消除forall量词 [英] coq: elimination of forall quantifier

问题描述

我想证明以下定理：

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 （ specialize（H x））。

You can instantiate the universally quantified x in H with specialize (specialize (H x)).

这篇关于coq：消除forall量词的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！