Sorry, I'm not sure if the title is the adequate question.
I have been going through Logical Foundations. In the Lemma "double_plus" i solved it with this solution:
Lemma double_plus : forall n, double n = n + n .
Proof.
induction n.
- simpl. reflexivity.
- simpl. rewrite <- plus_n_Sm. rewrite IHn. reflexivity.
Qed.
In the induction step my goal is: double (S n) = S n + S n.
I would like to know if it is possible to assume that (S n) is k and with that do something like:
(* double k = k + k *)
rewrite IH. (*k + k = k + k*)
reflexivity.
You can use the set tactic.
For instance
set (k := S n) in *.
will change all occurrences of S n and replace it by k. Note that this will still keep the information that k := S n in the context.
You can forget this information by using clearbody k.
Similar tactics include remember and generalize.
With respect to your title, note that rename is also a tactic that you can use, but only for renaming, eg. n into k (ie. you can change names, not terms).