The Coq mailing list

[Armaël Guéneau <armael.gueneau AT ens-lyon.fr>]

Hi Jeremy,

> 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