The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

----- Mail original -----
> De: "Jeremy Dawson" 
> <Jeremy.Dawson AT anu.edu.au>
> À: "coq-club" 
> <coq-club AT inria.fr>
> Envoyé: Lundi 3 Décembre 2018 07:16:55
> Objet: [Coq-Club] rewriting without instantiating

> Hi coq-club,
> 
> when I have a subterm like ?Φ1 ++ [] ++ ?Φ2 in a goal,
> and I want to rewrite using app_nil_l (ie, [] ++ l = l)
> how to I tell coq to rewrite without instantiating?
> 
> When I just say rewrite app_nil_l it instantiates ?Φ1 to []
> and then removes "[] ++ ", which is not what I want at all.

Hi Jeremy,

It is not clear to me want you want to obtain here...
l++[]++m is the term l++([]++m) because contrary to + (nat),
++ (app) is right associative in Coq (to be compatible
with cons which can only be associated to the right).

It you want to be precise about which instance to rewrite,
you can write something like

rewrite app_nil_l at 1 3 ...

but if there are several ways to unify the rewrite rule
(ie several values of l in this case), the numbers above only 
match the instances that correspond to the first unification 
match Coq finds: unification comes before instance finding.

You can partially specify a rewrite rule with something like

rewrite app_nil_l with (l := _::_::nil) 

for instance which lets Coq find (hopefully) the instance you 
want but still avoids typing all the term, or the variables 
it contains (which is bad for stability if you do not control
the names introduced by "intros").

In the case of

l++[]++m

there is only one thing you can do with
rewrite app_nil_l here. Btw, []++m reduces to
m and thus "simpl" would also change the goal into l++m.

Best,

Dominique