[Coq-Club] rewriting without instantiating

[Jeremy Dawson]

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

[Dominique Larchey-Wendling]

----- Mail original -----

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

[Jeremy Dawson]

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

Post by Dominique Larchey-Wendling
----- Mail original -----

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

[Robbert Krebbers]

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.

Post by Jeremy Dawson
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

Post by Dominique Larchey-Wendling
----- Mail original -----

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

[Emilio Jesús Gallego Arias]

Post by Robbert Krebbers
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.

See p. 44, Sec 7.2 of https://hal.inria.fr/inria-00258384v17:

,----
| Existential metavariables and rewriting
|
| The rewrite tactic will not instantiate existing existential
| metavariables when matching a redex pattern
`----

Cheers,
E.

[Jason Gross]

The general solution I use is a tactic I call set_evars:

Ltac set_evars :=
repeat match goal with
| [ |- context[?ev] ] => is_evar ev; let e := fresh "e" in set (e
:= ev)
end.

The rewrite tactic will not unfold these context definitions to find the
evars underneath them.

Post by Emilio Jesús Gallego Arias

Post by Robbert Krebbers
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.

,----
| Existential metavariables and rewriting
|
| The rewrite tactic will not instantiate existing existential
| metavariables when matching a redex pattern
`----
Cheers,
E.

[Armaël Guéneau]

Hi Jeremy,

Post by Jeremy Dawson
I just want it to rewrite ?Φ1 ++ [] ++ ?Φ2 to
?Φ1 ++ ?Φ2.

In my experience, ssreflect's rewrite is more conservative with respect
to evars (while the standard rewrite tends to instantiate them with
random stuff making it unusable in presence of evars).

With Coq >= 8.7 you can simply do:

Require Import ssreflect.
Require Import List.
Import ListNotations.

Goal exists (l1 l2 : list nat),
l1 ++ [] ++ l2 = nil.
Proof.
do 2 eexists. rewrite app_nil_l.

(*
============================
?l1 ++ ?l2 = []
*)


(note that the syntax of ssreflect's rewrite is slightly different from
the syntax of the standard rewrite, so you might need to adapt your
existing proofs a bit -- but in the long run, ssreflect's rewrite being
vastly superior makes the effort worth it)

------

Gah, turns out Robbert was faster and gave the same answer while I was
writing this... :-)

— Armaël

[Soegtrop, Michael]

Dear Jermeny,
Dear Coq Experts,

I thought an easy solution would be to use rewrite giving the evar as argument like this:

Require Import List.
Include List.ListNotations.

Goal forall T:Type, True.
Proof.
intro T.
evar (Φ1:list T).
evar (Φ2:list T).
assert(?Φ1 ++ [] ++ ?Φ2 = ?Φ1 ++ ?Φ2).
rewrite -> (app_nil_l ?Φ2).

But this doesn't work - Coq seems to ignore the argument. I would consider this to be a bug.

It does work if I give Φ2 rather than ?Φ2:

rewrite -> (app_nil_l Φ2).
reflexivity.

Another thing I don't understand is why I can't use the evar name if I create the goal in the way suggested by Armael:

Goal forall T:Type, exists (Φ1 Φ2 : list T),
Φ1 ++ [] ++ Φ2 = Φ1 ++ Φ2.
Proof.
do 2 eexists.

Fail rewrite -> (@app_nil_l T ?Φ2).

Can someone explain why the name ?Φ2 cannot be used here?

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: [phone], www.intel.de
Managing Directors: Christin Eisenschmid
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928