Can't figure out why re-write does not work

Question

I'm learning coq and can't figure out why a rewrite doesn't work.

My code looks like this:

Inductive nat : Type :=
| zero
| succ (n : nat)
.

Fixpoint add (a b : nat) : nat :=
  match b with
  | zero => a
  | succ b' => add (succ a) b'
  end.

Theorem add_succ : forall a b : nat,
    add a (succ b) = succ (add a b).

Proof.
  induction b as [ |  b' IHb ].
  - simpl.
    reflexivity.
  -

My current proof state is this:

- a, b' : nat
- IHb : add a (succ b') = succ (add a b')
============================
add a (succ (succ b')) = succ (add a (succ b'))

My expectation is that if I run

rewrite -> IHb.

then, coq will rewrite the left-hand side of my goal to

succ (add a (succ b')

My reason for thinking this is that (succ b') is of type nat and b' is of type nat with no other restriction. So I expect coq to notice that the pattern in IHb is matched by the left-hand side of the goal. But that does not happen.

What am I doing wrong?

Answer 1

Your hypothesis IHb only allows to rewrite the exact term add a (succ b'), because a and b' are variables in your context. You could do the rewrite step you indicate if your hypothesis IHb was quantifying universally over b', e.g. IHb : forall x, add a (succ x) = succ (add a x). Maybe you can modify your proof to obtain a stronger induction hypothesis at that point (relevant tactics to do that might be revert and generalize).