----- Mail original -----
Envoyé: Lundi 3 Décembre 2018 07:16:55
Objet: [Coq-Club] rewriting without instantiating
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.
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
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.