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

coq, coq-tactic, successor-arithmetics

Solution

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

Problem

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?

Original source