Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] rewriting without instantiating

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] rewriting without instantiating


Chronological Thread 
  • From: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] rewriting without instantiating
  • Date: Mon, 3 Dec 2018 09:04:38 +0100 (CET)



----- 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




Archive powered by MHonArc 2.6.18.

Top of Page