为什么带分号的证明不适用于句点？

Question

下面的证明在Coq in a Hurry中给出：

Fixpoint add n m := match n with 0 => m | S p => add p (S m) end.
Lemma exercise6 : forall n m, add n (S m) = S (add n m).
Proof.
  induction n; intros m; simpl.
    reflexivity.
  rewrite IHn; reflexivity.
Qed.

我试着一步一步地写这篇文章来理解发生了什么，但是在解决了基本案例之后归纳假设是不一样的！因此，战术失败：

Lemma exercise6' : forall n m, add n (S m) = S (add n m).
Proof.
  induction n.
  intros m.
  simpl.
  reflexivity.
  rewrite IHn. reflexivity.
Qed.

它们在以 "rewrite" 开头的行失败，并出现以下错误：

Error: Found no subterm matching add n (S ?M1580) in the current goal.

为什么同样的代码，一步一步写，会失败？分号和句点有什么区别？

此外，有没有一种方法可以让我快速查看 Coq 中给出的证明的逐步进展？

Answer 1

Here is a related answer.

简而言之：

induction n 生成 2 个子目标。
A;B 将策略 B 应用于所有 A

所以在这里，intros m; simpl 应用于 induction 生成的 2 个目标。这意味着您可以通过在 rewrite:

之前插入一个额外的 intros m 和一个额外的 simpl 来修复您的第二个脚本

Lemma exercise6' : forall n m, add n (S m) = S (add n m).
Proof.
  induction n.
  intros m.
  simpl.
  reflexivity.
  intros m.
  simpl.
  rewrite IHn.
  reflexivity.
Qed.

顺便说一下，您可以通过使用项目符号分隔各个子目标来使证明脚本的结构更加清晰。这给出了以下两个脚本，您可以在其中看到在 exercise6 中执行在进入任一子目标之前 而在 exercise6' 中它们已被推送进入每个子目标：

Lemma exercise6 : forall n m, add n (S m) = S (add n m). Proof. induction n; intros m; simpl. - reflexivity. - rewrite IHn; reflexivity. Qed. Lemma exercise6' : forall n m, add n (S m) = S (add n m). Proof. induction n. - intros m. simpl. reflexivity. - intros m. simpl. rewrite IHn. reflexivity. Qed.

为什么带分号的证明不适用于句点？

Why does a proof with semicolons not work with periods?

syntax

coq