coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Vadim Zaliva <vzaliva AT cmu.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] more naive questions about rewriting
- Date: Tue, 16 Aug 2016 15:11:03 -0700
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-wm0-f51.google.com
- Ironport-phdr: 9a23:zZDCEBADfzI6hR5f1XPqUyQJP3N1i/DPJgcQr6AfoPdwSP7/rsbcNUDSrc9gkEXOFd2CrakV0qyP4+u4ByRAuc/H6yFaNsQUFlcssoY/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbtr8FoOatcmrzef6o8SVOFQRwmPtKussZFXu9EOK55FQ2dMjYo8KiTLx6kNSfOpXwW46bXmypD3bovmKwZh47i5LsOgg/cMTGY/zfqA/UKAKRG9+azN9t4XXskzIShLK7X8BWE0XlABJCk7L9kLURJD05xXzuut4kBuTOczoRPhgRyar66Z1QTfjjTpBOjIkpjKEwvdshb5W9Ury7yd0xJTZNdmY
Laurent,
Thanks for the clarification. Now I understand why it did not work. However the solutions you propose are not perfect in my situation. Each of expressions f1,...,fn are automatically generated and potentially hundreds of lines long. Of course I can try to use 'remember' to give them shorter names, but that would require copy-pasting them into 'remember' statement.
I wonder if somebody tried to automate something like this? If there is a way in Ltac to find out nth-occurrence of the pattern, so it could be then used in 'replace'?
Vadim
--
CMU ECE PhD candidate
Mobile: +1(510)220-1060
On Tue, Aug 16, 2016 at 2:53 PM, Laurent Thery <Laurent.Thery AT inria.fr> wrote:
Hi
(* The following does not work. Error: Tactic failure: Nothing to
rewrite. *)
try rewrite <- compose_assoc at 2.
Unfortunately the rewrite _ at n, rewrite the nth occurrence of the first pattern that is found
Here is an example:
Goal forall (x y : nat), (x + 0) + (y + 0) + (x + 0) = 0.
intros.
rewrite <- plus_n_O at 2.
If you want to select a particular occurrence, one way is to instantiate the theorem enough to make it applicable only where you want.
In your example
Lemma Foo
{A:Type}
(f0 f1 f2 f3 f4: A->A)
:
compose f1 (compose f2 (compose f3 f4)) =
compose f1 (compose (compose f2 f3) f4).
Proof.
intros.
rewrite <- (compose_assoc _ _ _ _ _ _ f2).
or
Lemma Foo
{A:Type}
(f0 f1 f2 f3 f4: A->A)
:
compose f1 (compose f2 (compose f3 f4)) =
compose f1 (compose (compose f2 f3) f4).
Proof.
intros.
rewrite <- compose_assoc with (h := f2).
- [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/16/2016
- Re: [Coq-Club] more naive questions about rewriting, Laurent Thery, 08/16/2016
- Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/17/2016
- Re: [Coq-Club] more naive questions about rewriting, John Wiegley, 08/17/2016
- Re: [Coq-Club] more naive questions about rewriting, Laurent Thery, 08/17/2016
- Re: [Coq-Club] more naive questions about rewriting, Jonathan Leivent, 08/17/2016
- Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/17/2016
- Re: [Coq-Club] more naive questions about rewriting, Matthieu Sozeau, 08/17/2016
- Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/18/2016
- Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/18/2016
- Re: [Coq-Club] more naive questions about rewriting, Matthieu Sozeau, 08/18/2016
- Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/19/2016
- Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/18/2016
- Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/18/2016
- Re: [Coq-Club] more naive questions about rewriting, Matthieu Sozeau, 08/17/2016
- Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/17/2016
- Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/17/2016
- Re: [Coq-Club] more naive questions about rewriting, Laurent Thery, 08/16/2016
Archive powered by MHonArc 2.6.18.