The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

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).