The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

For this concrete example, it appears that the ssreflect rewrite tactic 
is doing what you want (i.e. it does _not_ instantiate the evar with 
[]). I have no idea if this is coincidental, or an explicit feature of 
the ssreflect rewrite tactic.

Maybe some of the ssr developers around here could tell more.

On 12/3/18 10:38 AM, Jeremy Dawson wrote:
> Hi Dominique,
>
> Thanks for your answer, I just want it to rewrite ?Φ1 ++ [] ++ ?Φ2 to
> ?Φ1 ++ ?Φ2.
>
> There would be only one possible spot to rewrite if it did not
> instantiate ?Φ1 to [].
>
> So how do I stop it instantiating variables in the goal?  (Obviously I
> want it to instantiate variables in the rule being used for rewriting,
> ie the variable l in the app_nil_l rule).  Experimenting with numbering
> locations where it might rewrite would be very inconvenient, since I
> will have dozens of goals I would be using my tactic on.
>
> Cheers,
>
> Jeremy
>
>
>
> On 12/03/2018 07:04 PM, Dominique Larchey-Wendling wrote:
> > ----- 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