Day two working through Software Foundations with Coq. Since I like to rant, and I love Darkest Dungeon, ENTER THE DARKEST PROOF. (Please don’t sue me!)

Naming

While trying to understand how rewrite works, I come across an obvious use-case:

Theorem adding_n_Sm : forall n m : nat, 
  n + S m = S n + m.
Proof.
  intros n. 
  induction n.
  simpl. reflexivity.
  simpl. rewrite <- IHn. 

At this point, in current scope I have:

1 subgoals, subgoal 1 (ID 90)
  n : nat
  IHn : forall m : nat, n + S m = S (n + m)
---------------
  forall m : nat, S (n + S m) = S (S (n + m))

Looks obvious enough. I should be able to substitute the n + S m with S (n + m) in my goal using rewrite <- IHn.

NOPE

Error: Found no subterm matching "n + S ?252" in the current goal.

Why is it: n + S ?252 the hypothesis clearly has n + S m! Where did m go? Am I losing my marbles?

After searching around, I come across an old thread with someone getting the same error. The reply post says

The strange-looking “?738” means any term to be instantiated… Besides, rewrite cannot rewrite under a “forall”.

Is m not defined? But it was up there in scope, right? Well my current scope did look like: IHn : forall m : nat, n + S m = S (n + m)

Oh, that does say forall m, how to make it just for that one m? Well n isn’t forall, perhaps intros?

Theorem adding_n_Sm : forall n m : nat, 
  n + S m = S n + m.
Proof.
  intros n m.
  induction n.
  simpl. reflexivity.
  simpl. rewrite <- IHn. 

SUCCESS

I…. I …. don’t know what is happening.