2

我想到目前为止，我已经阅读了标记为的 81 个问题（如果不是全部的话）的大部分内容。作为 coq 的新手，我无法找到这个非常简单的问题的答案（我相当肯定没有在 SO 上问过这个问题，因为它非常基础）。

我正在做一个家庭作业，为此我需要使用 coq 来证明：

  • 给定：P/Q。～问
  • 证明：P

这是我在纸上做的一个足够简单的证明，但我似乎无法让 coq 为我做这件事。

我的策略是假设每个P和Q，显示P并因此得出结论P必须成立：

  1. P / Q [前提]

  2. ～Q【前提】

    1. P [假设]

    2. P [复制上一行]

    3. 问 [假设]

    4. ~Q [复制上一行]
    5. [矛盾]
    6. P【矛盾消除】
  3. P [消除\/]

鉴于这是我在纸上证明它的方式，我能够想出以下 coq 代码在 coq 中证明它。可悲的是，我努力假设P,Q或~P没有通过：

Section Q5.

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

Goal P.

这是我对下一行的尝试，以及它们产生的错误：

+-----------------+---------------------------------------------------------------------+
|      Code       |                                Error                                |
+-----------------+---------------------------------------------------------------------+
| assumption.     | Error: No such assumption.                                          |
| exact P.        | The term "P" has type "Prop" while it is expected to have type "P". |
| apply premise1. | Error: Impossible to unify "P \/ Q" with "P".                       |
| apply P.        | Error: Impossible to unify "Prop" with "P".                         |
+-----------------+---------------------------------------------------------------------+

我很感激这方面的任何帮助，因为我已经用尽了我能想到的一切。

4

1 回答 1

3

我不确定我是否理解你的策略，但它似乎是正确的。

您要做的基本上是考虑P \/ Q析取的两种情况。这可以通过策略来完成destruct premise1.，这将产生两个目标，一个在其中p: P，一个在其中q: Q。这两个应该很容易证明。

你的战术失败的原因：

P : Prop
Q : Prop
premise1 : P \/ Q
premise2 : ~ Q
______________________________________(1/1)
P

  1. assumption.不会起作用，因为它只是在您的假设中查找类型是您当前目标的术语。这里没有类型的术语P。

  2. exact P.将失败，因为该策略exact <term>.应该解决一个目标<type>，如果<term> : <type>. 你的目标不是Prop，对吧？:)

  3. apply premise1.会失败，因为它只适用于一个目标P \/ Q。

  4. apply P.与当时基本相同exact P.。

总体而言，您似乎在区分术语和类型时遇到了（常见）问题。请记住，您的目标是一种类型，您尝试通过构建一个术语来证明它。你的假设都是形式的<term> : <type>，所以每当你使用exact <term>.or时apply <term>.，这是因为冒号右边的东西<term>匹配你的目标，而不是冒号左边的名字。

于 2012-09-23T06:12:17.507 回答