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

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.
rewrite ! add_assoc.
rewrite (add_comm n m).
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).
Proof. rewrite ! add_assoc, (add_comm n). reflexivity. Qed.
```

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

`!`

is "as many times as possible and at least once"

https://coq.inria.fr/refman/proofs/writing-proofs/equality.html#coq:tacn.rewrite

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

?

the absence of `!`

is *as many times as possible, possibly none*, right?

Nicolas Rinaudo said:

the absence of

`!`

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

ah! nice. Thank you very much.

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`

.

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. *)
rewrite add_assoc.
(* 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. *)
rewrite add_assoc.
(* Now we could have done it in one step that way: *)
Restart.
rewrite 2add_assoc.
(* 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? *)
rewrite add_comm.
(* 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.
rewrite (add_comm n).
(* 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
[add_comm].
First match is (n + m) in the LHS.
Other occurence is (n + m) in the RHS, so 2 terms rewritten with
only one rewrite. *)
rewrite (add_comm n).
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. *)
rewrite (add_comm n) at 1.
Undo 1.
rewrite (add_comm n) at 2.
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... *)
rewrite (add_comm p); reflexivity.
Qed.
```

You probably don't want to play with the `!`

flag with `add_comm`

, it might loop infinitely (although not in that case).

Thanks! I'll need to take a little time to study this, wasn't expecting such an in-depth answer. Much appreciated.

Last updated: Jun 13 2024 at 19:02 UTC