coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Damien Pous <Damien.Pous AT ens-lyon.fr>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] rewrite ... at ...
Date: Wed, 9 Feb 2011 09:10:08 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:content-type; b=VqLcvsAUc9Xn6hXVVvFI3BLZFZGCONSOQRZQ2Yu6LZA2ZkDk5AE4neUM46wxSyij6x tuLoZ2Q140yohesR+kO9+cnyVi1nIPzqXzFUjUsdaFzcXPxJ9dawcN81f2+7DaJmlWhU TnTwwSJ+39HyWqZ1YMq6GqAy55AY2JEAzEJXk=

I recently filed a bug report about a similar behaviour with setoid relations:
http://coq.inria.fr/bugs/show_bug.cgi?id=2474
I didn't notice it was also problematic with plain Leibniz equality...

Another option here is to use "setoid_rewrite at" rather than "rewrite
at" (although "rewrite at" seems to be already implemented with
setoids!):

Require Import List.

Lemma foo (A: Type) (P: list A -> list A -> Prop) (x1 x2: A):
P (x1 :: nil) (x2 :: nil).
Proof.
rewrite <- List.app_nil_l.
Show Proof.                    (* eq_ind *)
Restart.
rewrite <- List.app_nil_l at 1.
Show Proof.                    (* setoid things *)
Restart.
Fail rewrite <- List.app_nil_l at 2.
setoid_rewrite <- List.app_nil_l at 2.
Show Proof.                    (* setoid things *)
Abort.

Damien

[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