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

Question

在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 的常见模式。官方手册似乎是为非常高级的用户设计的，因为他们在几个其他术语上定义了一个术语，这些术语由更多术语定义，而且他们的语言是模棱两可的。

非常感谢您的回答！

Answer 1

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

关于你的问题，我想你会受益于阅读一些更全面的 Coq 介绍，例如 "Coq'art"、"Software Foundations" 或 "Programs and Proofs" 等。

特别是，elim 策略试图将所谓的 "elimination principle" 应用于特定类型。它被称为消除，因为在某种意义上，该规则允许您 "get rid" 该特定对象，允许您继续证明 [我建议阅读 Dummett 以更全面地讨论逻辑连接词的起源]

特别是∨联结词的消元规则，逻辑学家通常写成如下：

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

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

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

特别地，∨的定义是：

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

也就是说，or A B 是包含 A 或 B 以及 "tag" 的数据片段，它允许我们"match" 知道我们真正拥有哪一个。

现在，"elimination principle for or" 的类型为：

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

Coq的厉害之处在于，这样的原理不是"built-in"，只是一个正则程序！想一想，你能写出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 来解决你的第二个例子。祝你好运！

How does elim work in Coq on /\ and \/?