假设“或消除”证明的半个析取前提

Question

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

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

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

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

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

1. P / Q [前提]

2. ~Q [前提]

   1. P [假设]

   2. P [复制上一行]

      ---

   3. Q [假设]

   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".                         |
+-----------------+---------------------------------------------------------------------+

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

Answer 1

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

您要做的基本上是考虑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. 将失败，因为如果<term> : <type>，策略exact <term>. 应该解决目标<type>。你的目标不是Prop，对吧？ :)

3. apply premise1. 将失败，因为它仅适用于目标 P \/ Q。

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

---

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