## Stream: Coq users

### Topic: targeting specific part of a goal to simplify

#### Nicolas Rinaudo (Aug 22 2023 at 07:16):

(extreme beginner question)
In the middle of proofs, I sometimes find myself wanting to `simpl` or `rewrite` specific part of a goal - I might, for example, wish to use addition associativity on only one of the additions present.

My current solution is to use `assert <desired_outcome> as <hypothesis_label>`, prove that, and then rewrite my goal using this new knowledge.

This is kind of long winded though, and I was wondering if there was some better way?

As an example, to make this more concrete:

``````Theorem add_shuffle3 : forall n m p : nat,
n + (m + p) = m + (n + p).
Proof.
intros n m p.
rewrite add_assoc. (* n + (m + p) = (n + m) + p *)
assert (n + m = m + n) as H.
{ rewrite add_comm. reflexivity. } (* n + m = m + n *)
rewrite H.
rewrite <- add_assoc. (* n + (m + p) = (n + m) + p *)
reflexivity.
Qed.
``````

#### Olivier Laurent (Aug 22 2023 at 07:26):

Regarding your example, your introduced assertion is a specific instance of commutativity of `add` which you can define as `add_comm n m` and use directly for rewriting.
A possible more compact proof is then:

``````From Coq Require Import PeanoNat.
Import Nat.

Theorem add_shuffle3 : forall n m p : nat,
n + (m + p) = m + (n + p).
Proof.
intros n m p.
reflexivity.
Qed.
``````

or even more compact:

``````From Coq Require Import PeanoNat.
Import Nat.

Theorem add_shuffle3 n m p : n + (m + p) = m + (n + p).
``````

#### Nicolas Rinaudo (Aug 22 2023 at 07:28):

oh wow this is exactly what I was hoping to learn, thank you. Now I just need to work out what the ! does :)

#### Olivier Laurent (Aug 22 2023 at 07:29):

`!` is "as many times as possible and at least once"
https://coq.inria.fr/refman/proofs/writing-proofs/equality.html#coq:tacn.rewrite

#### Nicolas Rinaudo (Aug 22 2023 at 07:31):

I see. You're using it here to fail early if no rewrite happens, right? But then why are you not using it in `rewrite (add_comm n m).` ?

#### Nicolas Rinaudo (Aug 22 2023 at 07:31):

the absence of `!` is as many times as possible, possibly none, right?

#### Olivier Laurent (Aug 22 2023 at 07:34):

Nicolas Rinaudo said:

the absence of `!` is as many times as possible, possibly none, right?

No, this is `?`.
You could use both `?` or `!` here while none of them is doing just the first rewriting occurrence. Comparing to your original proof it allows to call `rewrite` on `add_assoc` only once.

#### Nicolas Rinaudo (Aug 22 2023 at 07:36):

ah! nice. Thank you very much.

#### Rodolphe Lepigre (Aug 22 2023 at 07:38):

You can also use ssreflect rewrite like:

``````rewrite [X in X + _ = _]add_comm.
``````

to specify the context under which to rewrite. The syntax basically says that the rewrite is gonna happen on the term identified by `X`, after matching the full goal with the pattern `X + _ = _`.

There are variations of the selector like `[in X in X + _ = _]` which would rewrite anywhere inside of the term identified by `X`.

#### Pierre Rousselin (Aug 22 2023 at 08:14):

Nicolas Rinaudo said:

I see. You're using it here to fail early if no rewrite happens, right? But then why are you not using it in `rewrite (add_comm n m).` ?

Just to clarify, the number of terms rewritten by `rewrite` (without any flag) actually depends on the number of identical terms to the first match left to right.

``````Theorem add_shuffle3 (n m p : nat) :
n + (m + p) = m + (n + p).
Proof.
(* search first term (left to right) matching (_ + (_ + _))
then rewrite _all_ occurences of this term into ((_ + _) + _).
here, it matches first (n + (m + p)) so it behaves like
[rewrite (add_assoc n m p)] and there is only on occurence. *)
(* We could also have specified [rewrite (add_assoc n m p)] and get the same
result. *)
(* Same thing, now matches only (m + (n + p)) which has only one occurence. *)
(* Now we could have done it in one step that way: *)
Restart.
(* Or, as many times as is possible. *)
Restart.
rewrite !add_assoc. (* Use with care: may cause infinite loops... *)
(* What if we try to [rewrite add_comm] without specifying any argument? *)
(* first match of (_ + _) left to right is actually
[add_comm (n + m) p] because without the notations, it is
[add (add n m) p]. There is only one occurrence, hence one rewrite. *)
(* not what we want: *)
Undo 1.
(* Now we try to match (n + _). It matches only (n + m).
One occurence of (n + m) hence one rewrite. *)
reflexivity.
Qed.
``````

Just to illustrate that one rewrite may change multiple terms.

``````Theorem more_occurences (n m p : nat) : p + (n + m) = (n + m) + p.
Proof.
(* Search first term matching (n + _) and rewrites all identical terms using
First match is (n + m) in the LHS.
Other occurence is (n + m) in the RHS, so 2 terms rewritten with
only one rewrite. *)
Undo 1.
(* If one wants to rewrite only some occurrences, use [at] followed by one
ore more numbers. Order of occurrences is left to right (without notations)
and start at 1. *)
Undo 1.
Undo 1.
(* You may specify multiple occurences. *)
rewrite (add_comm n) at 1 2.
Undo 1.
(* Of course, here, we just want to move [p] around... *)
You probably don't want to play with the `!` flag with `add_comm`, it might loop infinitely (although not in that case).