scope - 在当前环境中未找到该引用

Question

免责声明:这是一项家庭作业

我是一个coq菜鸟，所以我希望这不是一个重复的问题。我/已经/看过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. 将变量 Q : Prop. 替换为变量 P Q : Prop.。问题在于 P 将被假定为前提，但事实并非如此
2. 在目标声明之前添加Variables P.。这会导致语法错误。

我错过了什么吗？我似乎无法弄清楚这一点。

Answer 1

正确的解决方案是1，您期望的问题是错误的。

当你写下:

Variable P: Prop.

您并不是假设 P 存在(或者“P 成立”)，而只是假设存在一个名为 P 的命题，这是一个“陈述”，此处不考虑其有效性。

这与写作有很大不同:

Variable p: P.

假设存在类型“P”存在的证明“p”(如果 P 具有 Prop 类型，则 p 是命题 P 的证明)，因此假设 P 为真。

---

另外，原因是:

Variables P.

导致语法错误的是你需要为每个引入的变量提供一个类型(当没有信息引导类型推断引擎时，Coq 无法神奇地计算出它)。

---

因此，以以下方式开始脚本是完全可以的:

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