Why is my local coq no acting the same as standard coq e.g. as JsCoq?

Question

I was going through the trivial example in this question How can I rewrite "+ 1" (plus one) to "S" (succ) in Coq? but the proof does not work in my local computer despite it working on jscoq. This is where my proof gets stuck:

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

after that a reflexivity should conclude the proof but in my case it doesn't but gets into this weird state:

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

instead of

1 goal

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

Jscoq has version:

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

and my computer has

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

which I wouldn't have expected a difference but there is.

What is going on? Why is Coq not acting the same in both?

Also, Print Nat.add_comm. is failing for some reason that I assume is the same reason:

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

---

Note I am aware that perhaps doing a rewrite with the induction hypothesis only on the S n on the lhs might have worked followed by a simpl...but I don't know how to do that (which I am curious to learn) but the point of my question is not how to make it work on my Coq but why my coq is not acting the same as the "standard coq".

Answer 1

Given that your goal mentions the .+1, I suspect that you are using the SSReflect library of natural numbers. The SSReflect definition of addition is not simplified by the simpl tactic, hence simpl would not do anything here.

You can fix this behavior by explicity unfolding the SSReflect definition as follows:

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.