Généraliser les variables existentielles dans Coq

Question

J'essaie de prouver P ?x, où P : A -> Prop et ?x : A est une variable existentielle. Je peux prouver forall a:A, P a, donc j'ai besoin de généraliser P ?x à forall a:A, P a. Si x était une variable instanciée, x, je pourrais simplement utiliser generalize x pour produire forall x:A, P x. Lorsque j'essaie generalize ?x, Coq renvoie une erreur de syntaxe.

Est-ce possible? J'ai vérifié et Coq ne semble pas fournir un moyen intuitif de généraliser les déclarations sur les variables existentielles.

Toute aide serait grandement appréciée.

Answer 1

P ?x n'est pas équivalent à forall x, P x, ni même implicite par lui. Pour prouver P ?x, vous devez trouver quelques a tels que P a détient. Avec votre hypothèse, il suffit de trouver quelques a : A. En d'autres termes, vous devez prouver que le domaine n'est pas vide (ou plus précisément, vous devez prouver l'existence d'un élément dans le domaine). Ici, si vous avez a : A, vous pouvez utiliser instantiate (1 := A). Exemple stupide:

Parameter A : Set. 
Parameter P : A -> Prop. 
Goal (forall a, P a) -> A -> exists x, P x. 
Proof. 
    intros H a. eexists. instantiate (1 := a). apply H. 
Qed.