rewrite single occurence in ltac

Question

How can I invoke rewrite in ltac to only rewrite one occurrence? I think coq's documentation mentions something about rewrite at but I haven't been able to actually use it in practice and there are no examples.

This is an example of what I am trying to do:

Definition f (a b: nat): nat.
Admitted.

Theorem theorem1: forall a b: nat, f a b = 4.
Admitted.

Theorem theorem2: forall (a b: nat), (f a b) + (f a b) = 8.
Proof.
intros a b.
(*
my goal here is f a b + f a b = 8
I want to only rewrite the first f a b
The following tactic call doesn't work
*)
rewrite -> theorem1 at 1.

Answer 1

When I try rewrite -> theorem1 at 1. as you suggest, I get the following error message:

Error: Tactic failure: Setoid library not loaded.

So, as a reaction, I restarted your script, including the following command at the very beginning.

Require Import Setoid.

And now, it works (I am testing with coq 8.6).

Answer 2

You are using the rewrite at variant of the tactic, which as the manual specifies is always performed via setoid rewriting (see https://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic121).

Another possibility to have finer control over your rewriting rules is to assert the general shape of your desired rewrite (which here one would prove via theorem1), then perform a focused rewrite with the new hypothesis.

This works without resort to any libraries:

intros a b.
assert (H: f a b + f a b = 4 + f a b) by (rewrite theorem1; reflexivity).
rewrite H.