为什么我的本地coq的行为与标准coq不同，例如JsCoq

Question

我正在讨论这个问题中的一个琐碎的例子我如何重写"+1〃；(加一(到"；S〃；(成功(在Coq？但是，尽管我的本地计算机在jscoq上运行，但这个证明在它上不起作用。这就是我的证据被卡住的地方：

Lemma s_is_plus_one: 
forall n:nat, 
S n = n + 1.
Proof.
intros.
induction n.
- by reflexivity.
- simpl. rewrite -> IHn. (* reflexivity. Qed. *)

在那之后，反身性应该会结束证明，但在我的情况下，它没有，而是进入了这种奇怪的状态：

n: nat
IHn: n.+1 = n + 1
1/1
(n + 1).+1 = n + 1 + 1

而不是

1 goal
n ℕ 
IHn S n = n + 1 
S (n + 1) = S (n + 1)

Jscoq的版本：

jsCoq (0.14.2), Coq 8.14.1/81400
OCaml 4.12.0, Js_of_ocaml 3.11.0

我的电脑有

(meta_learning) brandomiranda~/coq4brando ❯ coqc -v
The Coq Proof Assistant, version 8.14.1
compiled with OCaml 4.10.2

我没想到会有什么不同，但确实存在。

发生了什么事？为什么Coq在两者中的表现不一样？

此外，Print Nat.add_comm.由于某种原因而失败，我认为这也是同样的原因：

Nat.add_comm not a defined object.
Not in proof mode.

---

注意，我知道，也许只对lhs上的S n进行归纳假设的重写可能会奏效，然后进行简单的。。。但我不知道如何做到这一点(我很想学习(，但我问题的重点不是如何让它在我的Coq上工作；标准coq"；。

Answer 1

鉴于您的目标提到了.+1，我怀疑您使用的是自然数的SSReflect库。SSReflect对加法的定义没有被simpl策略简化，因此simpl在这里不会做任何事情。

您可以通过如下显式展开SSReflect定义来修复此行为：

From mathcomp Require Import all_ssreflect.
Goal forall n, n.+1 = n + 1.
Proof.
rewrite addnE. intros n.
induction n as [|n IH].
- reflexivity.
- simpl. rewrite IH. reflexivity.
Qed.