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