Nicolas Rinaudo (Aug 22 2023 at 07:16): 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.
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 :)
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. *)
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).
Nicolas Rinaudo (Aug 22 2023 at 08:17):Thanks! I'll need to take a little time to study this, wasn't expecting such an in-depth answer. Much appreciated.
Last updated: Oct 13 2024 at 01:02 UTC