在當前環境中找不到參考

Question

免責聲明：這是作業作業

我是coq noob，所以我希望這不是一個重複的問題。我/有/看着this question，但我的問題似乎仍然沒有答案。

我有以下前提：

P \/ Q 
~Q 

我需要證明：

P 

我COQ至今代碼：

Section Q5. 

Variables Q : Prop. 
Goal P. 
Hypothesis premise1 : P \/ Q. 
Hypothesis premise2 : ~Q. 

我收到以下錯誤，當我嘗試執行該行Goal P.：

Error: The reference P was not found in the current environment.

這些是我能想出的解決方案：

1. 更換Variables Q : Prop.與Variables P Q : Prop.。問題在於P將假定爲前提，它不是
2. 在目標聲明之前添加Variables P.。這會導致語法錯誤。

我錯過了什麼嗎？我似乎無法弄清楚這一點。

Answer 1

正確的解決方案是1，你所期望的問題是錯誤的。

當你寫：

Variable P: Prop. 

你是不是假設P爲居住（或爲「P秉着」），但只存在一個命題命名爲P，一個「聲明」，其有效性這裏沒有考慮。

這是從寫作非常不同：

Variable p: P. 

它假定有一個證明「P」的類型「P」被宅（如果P的類型爲支柱，p是命題的證明P），因此假設P是真實的。

---

另外，爲什麼的原因：

Variables P. 

導致語法錯誤是，你需要提供推出的每一個變量的類型（勒柯克不能弄明白神奇時，有沒有信息引導類型推理引擎）。

---

所以這是完全正常的，開始你的腳本：

Section Q5. 
Variables P Q : Prop. 
Hypothesis premise1 : P \/ Q. 
Hypothesis premise2 : ~Q. 
Goal P.