在 Coq 中如何使 `simpl` 命令只执行一步缩减？

Question

我对add的定义如下：

Fixpoint add n m :=
  match n with
  | 0 => m
  | S p => add p (S m)
end.

在文件的后面，我试图证明以下目标： add (S n) 0 = S n

我调用simpl 命令期望它减少

add (S n) 0 到 add n (S 0)。

反而减少了

add (S n) 0 到 add n 1

我怀疑simpl 命令只要能执行就执行多个步骤。

我的问题：是否有一个命令可以减少一步，减少

add (S n) 0 = S n

到

add n (S 0) = S n

?

Answer 1

S 0 和 1 是相同的表达式。

“相同”不仅意味着S 0 = 1 成立，而且coq 的系统无法区分它们。相比之下，1 + 0 和 1 在 1 + 0 = 1 成立时并不相同。

0 是 O 的符号，1 是 S O 的符号。 所以S 0和1都代表同一个表达式S O。

如果您开始证明S 0 = 1，您将立即看到目标是1 = 1，如果您禁用Unset Printing Notations 的Notations，您将立即看到目标是eq (S O) (S O)。