coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] rewrite ... at ...

From: Aaron Bohannon <bohannon AT cis.upenn.edu>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] rewrite ... at ...
Date: Tue, 8 Feb 2011 14:44:37 -0500
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:content-type; b=XCgseoAVvqZ/00d635cqZRtYOqz1H9TLt6ZIjtz6wG43PPu6WfOeeqtnMvG42/0sQ7 yOs04rbI3eLH1tUkmUZgGQmafLp+pP/rkTICWml3FT2RA167yEqRd+JCgUTvvOFQri5B KQN22uYGyFWnj1Rx3qudvjygObya2Si6BUbeE=

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?

- Aaron

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.

[Coq-Club] rewrite ... at ..., Aaron Bohannon
- Re: [Coq-Club] rewrite ... at ..., Brandon Moore
  - Re: [Coq-Club] rewrite ... at ..., Aaron Bohannon
    - Re: [Coq-Club] rewrite ... at ..., Alexandre Pilkiewicz
      - Re: [Coq-Club] rewrite ... at ..., Damien Pous
        
        Re: [Coq-Club] rewrite ... at ..., Matthieu Sozeau