The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

> Le 9 juil. 2020 à 15:46, Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> a écrit :
> 
> 
> Hi,
> 
> I have a goal
> 
> swapped ((single a ++ qs) ++ vs) ((qs ++ vs) ++ single a)
> 
> where single is defined by
> 
> Definition single X (a : X) := [a].
> 
> When I try
> 
> rewrite - !app_comm_cons.
> 
> it unfolds one of the occurrences of single x
> 
> (which stops my carefully written Ltac function from working and took ages 
> to pinpoint what was happening).
> 
> How do I stop this from happening?

Hi,

I think you have to refine the syntactic pattern to `rewrite - [(_ :: _) ++ 
_]!app_comm_cons`, otherwise
the inferred syntactic pattern of the rule just considers the top-level 
symbol, e.g. `[_ ++ _]`
and then uses unification up-to-reduction for the subterms, which succeeds 
here.

Best,
— Matthieu