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.
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”.
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
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.
I…. I …. don’t know what is happening.