How to use rewrite on a subexpression of the current goal

Question

In Coq, is it somehow possible to apply a lemma or hypothesis to a subexpression of the current goal? For example I would like to apply the fact that plus is commutative in order to swap 3 and 4 in this example.

Require Import Coq.Arith.Plus.

Inductive foobar : nat -> Prop :=
| foob : forall n : nat, foobar n.


foob (3 + 4) = foob (4 + 3)

foob (3 + 4) = foob (4 + 3)
Unable to unify "?M691 + ?M692 = ?M692 + ?M691" with "foob (3 + 4) = foob (4 + 3)".

foob (3 + 4) = foob (4 + 3)

gives:

The command has indeed failed with message: Unable to unify "?M691 + ?M692 = ?M692 + ?M691" with "foob (3 + 4) = foob (4 + 3)".

How can I tell Coq where exactly in this goal to apply plus_comm?

Answer

In this particular case, rewrite will work if you define the inductive type using a constructor parameter instead of an index:

Inductive foobar : Type :=
| foob (n : nat).

Since there is only one constructor for this type, my understanding (from this answer) is that using an index does not provide any benefit but makes it harder for Coq to pattern-match.

In general, either of the following techniques can achieve the effect of a targeted rewrite:

assert

  

3 + 4 = 4 + 3
H: 3 + 4 = 4 + 3
foob (3 + 4) = foob (4 + 3)

3 + 4 = 4 + 3

4 + 3 = 4 + 3
reflexivity.
H: 3 + 4 = 4 + 3

foob (3 + 4) = foob (4 + 3)

rewrite

  (* introduce a new sub-goal where you can prove that the replacement is OK *)
  

foob (4 + 3) = foob (4 + 3)

4 + 3 = 3 + 4
(* Coq orders the new goal last. I think it's clearer to tackle it first *)

4 + 3 = 3 + 4
(* do the rewrite *)

3 + 4 = 3 + 4
reflexivity.

foob (4 + 3) = foob (4 + 3)