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: Laurent Thery <Laurent.Thery AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] more naive questions about rewriting
  • Date: Tue, 16 Aug 2016 23:53:48 +0200


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