Proving S (n + m) = n + (S m), how to rewrite n+1 = S(n)?

Question

Theorem add_0_r : forall n:nat, n + 0 = n.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *) reflexivity.
  - (* n = S n' *) simpl. rewrite -> IHn'. reflexivity. Qed.

Theorem plus_n_Sm : forall n m : nat,
  S (n + m) = n + (S m).
Proof.
  intros n m. induction m as [| m' IHn']. rewrite -> add_0_r. rewrite <- sum.

The last tactic rewirte <- sum does not work. This is the goal:

n: ℕ
-------------
S(n) = n + 1

I don't know how to rewrite n+1 as S(n). I think that n+1 is just a notation for S(n), right?

Answer 1

If you look at the definition of + as follows, you can see that it is defined by induction on its first argument:

Locate "+". (* to obtain the name Nat.add *)
Print Nat.add.
(*
Nat.add =
fix add (n m : nat) {struct n} : nat :=
  match n with
  | 0 => m
  | S p => S (add p m)
  end
     : nat -> nat -> nat
*)

As a result 1 + n is indeed convertible to S n (you can see that using Eval cbn in 1 + ?[n].) but not n + 1 (if you unfold Nat.add. you will obtain a pattern match stuck on the variable n).

For your proof, that specific definition of + means that you might reconsider your approach and try to do your proof by induction on n rather than m (paying attention to have the right induction hypothesis).

Answer 2

If you are using the nat type from the standard library, then n+1 is not a notation for S n, but a notation for the function Nat.add. In that case n+1 is not apparently equal to S n. You need to prove it by an induction on n.

By the way, if you are using Nat.nat, you need to use induction on n rather than m. Because Nat.add is defined by a match on the first argument. In this case, your first subgoal of the induction can be proved simply by reflexivity. (Coq is able to simplify S (0 + m) and 0 + S m, but not S (n + 0) and n + 1).

Answer 3

Was able to prove with the following:

Theorem plus_n_Sm : forall n m : nat,
  S (n + m) = n + (S m).
Proof.
  intros n m. induction n as [| n' IHn']. 
  - simpl. reflexivity.
  - simpl. rewrite -> IHn'. reflexivity.
Qed.