coq: élimination des forall quantificateurs

Question

Je veux prouver le théorème suivant:

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

je l'ai déjà obtenu la pièce suivante de la preuve:

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

Mais maintenant, je suis dans une situation que je don Je ne sais pas quoi faire. Les choses suivantes sont à ma disposition:

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

Et je voudrais prouver la subgoal suivante:

q \/ p x 

Comment puis-je éliminer les quantificateurs forall dans l'hypothèse donnée

forall x : A, p x 

c'est-à-dire: Comment puis-je brancher mon béton x: A pour que je puisse en déduire: px?

Answer 1

Vous pouvez instancier le x quantifié universellement dans H avec specialize (specialize (H x)).

Answer 2

Probablement le plus simple?

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.