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.

这些是我能够提出的解决方案:

替换 Variables Q : Prop.与 Variables P Q : Prop. .问题在于 P将被假定为一个前提，它不是

添加 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.