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.
a, b: nat
nat
Admitted.

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

Theorem theorem2: forall (a b: nat), (f a b) + (f a b) = 8.
forall a b : nat, f a b + f a b = 8
Proof.
forall a b : nat, f a b + f a b = 8
  intros a b.
a, b: nat
f a b + f a b = 8
  (*
    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.
Tactic failure: Setoid library not loaded.
a, b: nat
f a b + f a b = 8

Answer (Yves)

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

The command has indeed failed with message:
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.

Answer (Rob Blanco)

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.
a, b: nat
f a b + f a b = 8
  assert (H: f a b + f a b = 4 + f a b) by (rewrite theorem1; reflexivity).
a, b: nat
H: f a b + f a b = 4 + f a b
f a b + f a b = 8
  rewrite H.
a, b: nat
H: f a b + f a b = 4 + f a b
4 + f a b = 8

Answer (Anton Trunov)

There are several options, one of them was pointed out by @Yves.

Another option is to use the pattern tactic:

  pattern (f a b) at 1.
a, b: nat
(fun n : nat => n + f a b = 8) (f a b)
  rewrite theorem1.
a, b: nat
4 + f a b = 8

The trick here is in fact that pattern (f a b) at 1. turns the goal

1 subgoal

  a, b : nat
  ============================
  f a b + f a b = 8

into

1 subgoal

  a, b : nat
  ============================
  (fun n : nat => n + f a b = 8) (f a b)

Basically, it beta-expands your goal, abstracting on the first occurrence of f a b. Also, normally rewrite won't rewrite under binders (e.g. lambdas), because if it did, you'd be able to go from let's say fun x => x + 0 to fun x => x, which are not equal in vanilla Coq.

Then rewrite theorem1. rewrites the argument (f a b) to 4 and simplifies a bit (it does beta-reduction), hence you obtain 4 + f a b = 8.

Side note: you can also use the replace tactic like so:

  replace (f a b + f a b) with (4 + f a b) by now rewrite theorem1.
a, b: nat
4 + f a b = 8