coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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).
- [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.