coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
To: Aaron Bohannon <bohannon AT cis.upenn.edu>
Cc: Brandon Moore <brandon_m_moore AT yahoo.com>, Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] rewrite ... at ...
Date: Wed, 9 Feb 2011 08:31:40 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type :content-transfer-encoding; b=fA/zVA3AfLTrxyTEFh3INa0oa+FfNyyYOe/5JPD0FMjk/ShzsZkh4pdo57Dq8a4LOQ eNxyaRwcuknlU2yHA7aPLir2rDNRByeaMwrMRNdVXY1TPf73mX1gGuJ8xhOA19gJtlcU V7thv+6conGuC/Y6p+UymHOYfXG9ya0pgaqV8=

Hi Aaron

2011/2/9 Aaron Bohannon
<bohannon AT cis.upenn.edu>:
> 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.

Maybe something like

match goal with
| |- context[P ?term _] =>
   let t := fresh in
   remember term as t;
   match goal with
     | Heqt : t = term |- _ =>
       rewrite EQ in Heqt;
       subst t; clear Heqt
   end
end.

would help ?

[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