1

这是书中的代码：

Example In_example_2 :
  forall n, In n [2; 4] ->
  exists n', n = 2 * n'.
Proof.
  (* WORKED IN CLASS *)
  simpl.
  intros n [H | [H | []]].
  - exists 1. rewrite <- H. reflexivity.
  - exists 2. rewrite <- H. reflexivity.
Qed.

Aftersimpl. In转换为 3 个元素的析取：

============================
forall n : nat, 2 = n \/ 4 = n \/ False -> exists n' : nat, n = n' + (n' + 0)

但我完全不明白如何阅读：

intros n [H | [H | []]].

它产生了这个：

n : nat
H : 2 = n
============================
exists n' : nat, n = n' + (n' + 0)

subgoal 2 (ID 229) is:
 exists n' : nat, n = n' + (n' + 0)

我的理解：

  1. 它将 n fromforall放入上下文中。
  2. 它将 3 个元素的析取分解为 2 个子目标，忽略 False：
  3. 根据拆分的数量创建了 2 个子目标。

底部还有一个提示：

(** (Notice the use of the empty pattern to discharge the last case
    _en passant_.) *)

En passant（法语：[ɑ̃ paˈsɑ̃]，点燃。顺便说一句）是国际象棋中的一步。这是一种特殊的棋子捕获，只能在棋子从其起始格移动两个格子后立即发生，并且如果它只前进一个格子就可能被敌方棋子捕获。

看着这个：

intros n [H | [H | []]].

有人可以解释一下吗：

  1. 这种形式的命令应该用于破坏forall吗？这个任务还有别的吗？
  2. 如何用英文阅读这个命令？
  3. 为什么要[H | []]放在另一对括号中？
  4. 如何[]告诉 coq 忽略 False 语句？
  5. 一般什么时候应该使用这个命令？
4

1 回答 1

3

intros n [H | [H | []]]表格是一个简写形式

intros n H. destruct H as [H | [H | []]].

您可以进一步将证明重写为

intros n H. destruct H as [H2 | H4F].
- (* H2 : 2 = n *)
  exists 1. rewrite <- H2. reflexivity.
- (* H4F : 4 = n \/ False *)
  destruct H4F as [H4 | HF].
  + (* H4 : 4 = n *)
    exists 2. rewrite <- H4. reflexivity.
  + (* HF : False *)
    destruct HF. (* No more subgoals here *)

这两个证明在逻辑上是等价的，但第一个更短（并且更容易阅读，一旦你习惯了语法）。

一般来说，该策略destruct x as [...]采用表达式x并为每个可用于生成的构造函数生成一个子目标x。构造函数的参数根据模式命名，[...]不同构造函数对应的部分用竖线分隔。

形式的命题A \/ B \/ C应读作A \/ (B \/ C)。因此，当您destruct在上面的扩展形式中第一次调用时，您会得到两种情况：when 为 whenA保持，另一种为 whenB \/ C保持。您需要再次调用destruct以分析内部或，这就是为什么您在原始表达式中嵌套括号的原因。至于最后一个分支，False被定义为一个没有构造函数的命题，所以一旦你破坏了一个假设HF : False，证明就完成了。

（这里，“ en passant ”相当于英文的“inpassant”，大致意思是“顺便”。它指的是我们将最后一个案例作为对或假设进行案例分析的副产品来排放。 )

于 2019-04-26T01:17:45.363 回答