The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

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
>