在 Coq 中，elim 如何在 /\ 和 \/ 上工作？答案

【问题标题】：How does elim work in Coq on /\ and \/?在 Coq 中，elim 如何在 /\ 和 \/ 上工作？
【发布时间】：2017-09-24 04:50:17
【问题描述】：

在Coq Tutorial 的1.3.1 和1.3.2 节中，有两个elim 应用程序：第一个：

1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A /\ B
  ============================
   B /\ A

申请elim H后，

Coq < elim H.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A /\ B
  ============================
   A -> B -> B /\ A

第二个：

1 subgoal

  H : A \/ B
  ============================
   B \/ A

申请elim H后，

Coq < elim H.
2 subgoals

  H : A \/ B
  ============================
   A -> B \/ A

subgoal 2 is:
 B -> B \/ A

共有三个问题。首先，在第二个示例中，我不明白将什么推理规则（或逻辑同一性）应用于生成两个子目标的目标。不过，第一个例子我很清楚。

第二个问题，根据 Coq 的手册，elim 与归纳类型有关。所以看来elim这里根本不能应用，因为我感觉这两个例子都没有归纳类型（原谅我不知道归纳类型的定义）。为什么elim可以用在这里？

第三，elim 一般是做什么的？这里的两个示例没有显示elim 的常见模式。官方手册似乎是为非常高级的用户设计的，因为他们定义一个术语是基于由更多术语定义的其他几个术语，并且他们的语言是模棱两可的。

非常感谢您的回答！

【问题讨论】：

【解决方案1】：

Jian，首先请注意，该手册是开源的，可在https://github.com/coq/coq 获得；如果您认为可以改进措辞/定义顺序，请在此处打开问题或随时提交拉取请求。

关于您的问题，我认为您会受益于阅读一些更全面的 Coq 介绍，例如“Coq'art”、“软件基础”或“程序和证明”等。

特别是，elim 策略试图对特定类型应用所谓的“消除原则”。之所以称为消除，是因为从某种意义上说，该规则允许您“摆脱”该特定对象，从而使您可以继续证明[我建议阅读 Dummett 以更全面地讨论逻辑连接词的起源]

特别是，∨连接词的消除规则通常由逻辑学家编写如下：

          A   B
          ⋮  ⋮
 A ∨ B    C   C
────────────────
       C

也就是说，如果我们可以从A和B独立推导出C，那么我们可以从A ∨ B推导出来。这看起来很明显，不是吗？

回到 Coq，事实证明，由于“Curry-Howard-Kolmogorov”等价性，这条规则具有计算解释。事实上，Coq 并没有将大多数标准逻辑连接词作为内置提供，但它允许我们通过“归纳”数据类型来定义它们，类似于 Haskell 或 OCaml 中的那些。

特别是∨的定义是：

Inductive or (A B : Prop) : Prop :=
  | or_introl : A -> A \/ B
  | or_intror : B -> A \/ B

也就是说，or A B 是包含A 或B 以及“标签”的数据片段，它允许我们“匹配”以了解我们真正的哪一个有。

现在，“或的消除原理”具有以下类型：

or_ind : forall A B P : Prop, (A -> P) -> (B -> P) -> A \/ B -> P

Coq 的伟大之处在于，这样的原理不是“内置”的，只是一个常规程序！想想，你能写出or_ind函数的代码吗？我给你一个提示：

Definition or_ind A B P (hA : A -> P) (hB : B -> P) (orW : A ‌\/ B) :=
  match orW with
  | or_introl aW => ?
  | or_intror bW => ?
  end.

一旦定义了这个函数，elim 所做的就是应用它，正确地实例化变量P。

练习：使用apply 和ord_ind 而不是elim 解决您的第二个示例。祝你好运！

【讨论】：