The Coq mailing list

[Aaron Bohannon <bohannon AT cis.upenn.edu>]

On Tue, Feb 8, 2011 at 5:54 PM, Brandon Moore 
<brandon_m_moore AT yahoo.com>
 wrote:
> I just noticed arguments with underscores are allowed.
> "rewrite <- app_nil_l (x2::_)." will target the second instance.
> I think this would usually be almost as compact as using
> numbers, and much easier to read and write.

Ah, OK.  Thanks for the partial explanation and this tip.  I was
unfortunately in the situation where I have "P (e1 :: nil) (e2 ::
nil)" with e1 and e2 being very large expressions that are almost
identical except for deeply nested subterms.  It seems that, without
out a clearly specified semantics for pattern positions, the most
succinct, non-fragile way to do the rewrite is something like this...

assert (H := forall l1 l2, P (nil ++ l1) l2 -> P l1 l2)
  by (intros; replace l1 by (nil ++ l1) by app_nil_l; trivial).
apply H.

 - Aaron