The Coq mailing list

[Brandon Moore <brandon_m_moore AT yahoo.com>]

> From: Aaron Bohannon 
> <bohannon AT cis.upenn.edu>
> Sent: Tue, February 8, 2011 1:44:37 PM
>
> Can someone explain the behavior below.  There are clearly  two
> occurrences of lists eligible for rewriting.  Which one is  which?  And
> why does "at 2" fail?

It seems like the additional parameters of app_nil_l become fixed
before the search for matching locations, or perhaps they are filled
with existentials that are resolved at the first match.
before or during the search for matching locations.

This behavior seems consistent with the parameters of the rule
being filled in before the search for matching locations, or the
parameters being filled with existentials that become bound at
the first match.

That does not explain why "rewrite <- ..." and "rewrite <- ... at 1" pick 
different instances.

It's pretty clear this is not the best behavior, but giving instances by
number is pretty fragile and hard to read in the first place. For example,
there are actually four places where the rule could be applied.

I just noticed you can use arguments with underscores in a rewrite,
which should let you guide the matching without copying entire
subterms of the goal.

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.

Brandon

> Lemma  foo:
>   forall (A: Type) (P: list A -> list A -> Prop) (x1 x2:  A),
>   P (x1 :: nil) (x2 :: nil).
> Proof.
>   intros  *.
> 
> Goal is now:
>   P (x1 :: nil) (x2 :: nil).
> 
> If I  execute:
>   rewrite <- List.app_nil_l.
> Goal becomes:
>   P  (x1 :: nil) (nil ++ x2 :: nil).
> 
> If I execute:
>   rewrite <-  List.app_nil_l at 1.
> Goal becomes:
>   P (nil ++ x1 :: nil) (x2 ::  nil).
> 
> If I execute:
>   rewrite <- List.app_nil_l at  2.
> Result is:
>   Tactic failure:setoid rewrite failed: no progress  made.
>