在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

to

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。