The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 08/17/2016 12:11 AM, Vadim Zaliva wrote:
> 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'?

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.
  set (u :=  compose _  _) at 2.
  change u with (compose (compose f2 f3) f4).