coq - elim 如何在 Coq on/\and\/中工作？

Question

在Coq Tutorial , section 1.3.1 and 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 策略试图对特定类型应用所谓的“消除原则”。它被称为消除，因为在某种意义上，该规则允许您“摆脱”那个特定的对象，允许您继续证明 [我建议阅读 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

也就是说，或A B是包含A或B的数据，连同“标签” ”，这使我们能够“匹配”以了解我们真正拥有的是哪一个。

现在，“or 的消除原则”有类型:

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 来解决你的第二个例子。祝你好运!