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

Question

我正在经历这个问题中的简单示例 如何在 Coq 中将“+ 1”（加一）重写为“S”（succ）？ 但是该证明在我的本地计算机上不起作用，尽管它在 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 没有表现出与“标准 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.