How can I rewrite "+ 1" (plus one) to "S" (succ) in Coq?

Question

I have the following Lemma with an incomplete proof:

Lemma s_is_plus_one : forall n:nat, S n = n + 1.
Proof.
  intros.
  reflexivity.
Qed.

This proof fails with

Unable to unify "n + 1" with "S n".

It seems like eq_S would be the way to prove this, but I can't apply it (it doesn't recognize n + 1 as S n: Error: Unable to find an instance for the variable y.). I've also tried ring, but it can't find a relation. When I use rewrite, it just reduces to the same final goal.

How can I finish this proof?

Answer 1

This is related to the way (+) is defined. You can access (+)'s underlying definition by turning notations off (in CoqIDE that's in View > Display notations), seeing that the notation (+) corresponds to the function Nat.add and then calling Print Nat.add which gives you:

Nat.add = 
fix add (n m : nat) {struct n} : nat :=
  match n with
  | O => m
  | S p => S (add p m)
  end

You can see that (+) is defined by matching on its first argument which in n + 1 is the variable n. Because n does not start with either O or S (it's not "constructor-headed"), the match cannot reduce. Which means you won't be able to prove the equality just by saying that the two things compute to the same normal form (which is what reflexivity claims).

Instead you need to explain to coq why it is the case that for any n the equality will hold true. A classic move in the case of a recursive function like Nat.add is to proceed with a proof by induction. And it does indeed do the job here:

Lemma s_is_plus_one : forall n:nat, S n = n + 1.
Proof.
intros. induction n.
 - reflexivity.
 - simpl. rewrite <- IHn. reflexivity.
Qed.

Another thing you can do is notice that 1 on the other hand is constructor-headed which means that the match would fire if only you had 1 + n rather than n + 1. Well, we're in luck because in the standard library someone already has proven that Nat.add is commutative so we can just use that:

Lemma s_is_plus_one : forall n:nat, S n = n + 1.
Proof.
intros.
rewrite (Nat.add_comm n 1).
reflexivity.
Qed.

A last alternative: using SearchAbout (?n + 1), we can find all the theorems talking about the pattern ?n + 1 for some variable ?n (the question mark is important here). The first result is the really relevant lemma:

Nat.add_1_r: forall n : nat, n + 1 = S n