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

Question

在Coq教程 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

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

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

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

尤其是针对？的排除规则。连接词通常由逻辑学家写成如下：

          A   B
          ?  ?
 A ? B    C   C
????????????????
       C

也就是说，如果我们可以C独立地从A和导出B，则可以从中导出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。祝好运！