Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] more naive questions about rewriting

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] more naive questions about rewriting


Chronological Thread 
  • 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).







Archive powered by MHonArc 2.6.18.

Top of Page