I have a simple lemma for lists which says n::l = [n]++l whose proof appears below.
Lemma cons_to_app : (forall (n: nat) (l: list nat), n :: l = [n] ++ l).
Proof.
simpl. reflexivity.
Qed.
Now I want to use this proof rewrite cons terms :: wherever they appear in the proof goal. For example, consider following.
Lemma easy_lemma : forall (n : nat) (xs ys : list nat), (n::xs) ++ (n::ys) = (n::xs) ++ ([n] ++ ys).
I would like to rewrite the (n::ys) to [n] ++ ys and the proof is done. Since n::ys is the second time that :: appears in the proof goal, I thought that rewrite const_to_app at 2 would work, but actually it acts on the 3rd :: and changes the proof goal to (n :: xs) ++ n :: ys = ([n] ++ xs) ++ [n] ++ ys.
What location can I specify to make the rewrite work on the (n::ys) term?
I still can't find the original source that talks about the exact behavior of rewrite at (other than the one eponier mentioned). The post at the link was written in 2011 but seems to be still valid as of 2019 with Coq version 8.9.1, and likely won't be "fixed" because the issue was closed as "invalid" saying "changing the behavior will break backwards compatibility".
rewrite lemma at n instantiates the equality using the first occurrence, and then rewrites its nth occurrence.
Given the lemma to prove
Lemma easy_lemma :
forall (n : nat) (xs ys : list nat), (n::xs) ++ (n::ys) = (n::xs) ++ ([n] ++ ys).
and the lemma used to rewrite
Lemma cons_to_app : (forall (n: nat) (l: list nat), n :: l = [n] ++ l).
rewrite cons_to_app at n. always chooses the subterm n :: xs, then rewrites the nth occurrence of n :: xs to [n] ++ xs. The second n :: xs just happens to be the third _ :: _.
Simple solution is to give enough arguments to tell Coq the exact thing to rewrite. rewrite (cons_to_app _ ys) is enough in this case.
One alternative is to use the setoid_rewrite tactic, which looks at all applicable subterms. However, it sometimes looks too deep into the definitions, and indeed it's the case for this example; setoid_rewrite cons_to_app at 1. gives
1 subgoal
n : nat
xs, ys : list nat
______________________________________(1/1)
[n] ++
(fix app (l m : list nat) {struct l} : list nat := match l with
| [] => m
| a :: l1 => a :: app l1 m
end) xs (n :: ys) = (n :: xs) ++ [n] ++ ys
Folding the app gives [n] ++ (xs ++ n :: ys), which is different from what we want i.e. ([n] ++ xs) ++ n :: ys. We can observe that setoid_rewrite unfolded app once, changing the LHS to n :: (xs ++ n :: ys), then instantiated the lemma to rewrite the outermost _ :: _.
To avoid unfolding app, we can declare Opaque app. before rewriting. Then setoid_rewrite ... at 1 gives what we want (and so does at 2). To revert the effect of Opaque, use Transparent.