2

免责声明：这是一个家庭作业

我是一个 coq 菜鸟，所以我希望这不是一个重复的问题。我/已经/看过这个问题，但我的问题似乎仍然没有答案。

我有以下前提：

P \/ Q
~Q

我需要证明：

P

到目前为止我的coq代码：

Section Q5.

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

当我尝试执行该行时出现以下错误Goal P.：

错误：在当前环境中找不到引用 P。

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

  1. 替换Variables Q : Prop.为Variables P Q : Prop.。问题在于，这P将被假定为前提，但事实并非如此
  2. Variables P.在目标声明之前添加。这会导致语法错误。

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

4

1 回答 1

4

正确的解决方案是 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.
于 2012-09-22T03:26:12.550 回答