推廣Coq中的存在變量

Question

我試圖證明P ?x，其中P : A -> Prop和?x : A是一個存在變量。我可以證明forall a:A, P a，所以我需要將P ?x概括爲forall a:A, P a。

如果？x是一個實例化變量x，我可以簡單地使用generalize x來生成forall x:A, P x。但是，當我嘗試generalize ?x時，Coq返回語法錯誤。

這可能嗎？我已經檢查過，Coq似乎沒有提供一種直觀的方式來概括關於存在變量的陳述。

任何幫助將不勝感激。

Answer 1

P ?x不等於forall x, P x，甚至不暗示它。爲了證明P ?x，你需要找到一些a，使得P a成立。用你的假設，找到一些a : A就足夠了。換句話說，你需要證明域不是空的（或者更確切地說，你需要證明域中元素的存在）。

在這裏，如果您有一些a : A，則可以使用instantiate (1 := A)。愚蠢的例子：

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.