The rewrite tactic achieves the replacement of equal (sub-)terms by other (sub-)terms. This replacement is a cornerstone of equational reasoning in that it epitomizes referential transparency, i.e., the ability to replace equals by equals.
The following proposition captures the fact that given two arguments that are equal, a function maps each of them to two equal results:
Proposition p1 :
forall i j : nat,
i = j ->
forall f : nat -> nat,
f i = f j.
Proof.
intros i j H_i_j f.
The *goals* window then reads:
i, j : nat
H_i_j : i = j
f : nat -> nat
============================
f i = f j
We use the rewrite tactic from left to right over the assumption named H_i_j, a Leibniz equality, to replace i by j in the goal:
rewrite -> H_i_j.
The *goals* window then reads:
i, j : nat
H_i_j : i = j
f : nat -> nat
============================
f j = f j
Since both sides of the = sign are textually identical, we complete the proof by using the reflexivity tactic:
reflexivity.
Qed.
Sometimes, the goal contains several occurrences of an expression we want to rewrite. The rewrite tactic processes all of them, which may or may not be what we want. Each occurrence can be indexed by its depth-first, left-to-right occurrence. Postfixing the call to the rewrite tactic with this index specifies which occurrence to rewrite. Here is a silly example that makes the point:
Proposition silly :
forall x y : nat,
x = y ->
x + x * y + (y + y) = y + y * x + (x + x).
Proof.
intros x y H_x_y.
The *goals* window then reads:
x, y : nat
H_x_y : x = y
============================
x + x * y + (y + y) = y + y * x + (x + x)
Using the rewrite tactic below replaces all occurrences of x in the goal by y:
rewrite -> H_x_y.
And indeed the *goals* window reads:
x, y : nat
H_x_y : x = y
============================
y + y * y + (y + y) = y + y * y + (y + y)
Since both sides of the = sign are textually identical, we complete the proof by using the reflexivity tactic:
reflexivity.
Alternatively, we can single out which occurrence to rewrite:
Restart.
intros x y H_x_y.
Restarting the proof and using the intros rules yields back the same *goals* window:
x, y : nat
H_x_y : x = y
============================
x + x * y + (y + y) = y + y * x + (x + x)
There are 5 occurrences of x in the goal, numbered 1, 2, 3, 4, and 5 depth-first from left to right. Let us replace the 4th occurrence:
rewrite -> H_x_y at 4.
The *goals* window then reads:
x, y : nat
H_x_y : x = y
============================
x + x * y + (y + y) = y + y * x + (y + x)
And indeed the 4th occurrence of x has been replaced by y. There are now 4 occurrences of x in the goal, numbered 1, 2, 3, and 4, i.e., the last occurrence of x, which was the 5th one, is now the 4th one. So 3 consecutive rewritings of the first occurrence of x will have the effect of replacing its 3 first occurrences by y:
rewrite -> H_x_y at 1.
rewrite -> H_x_y at 1.
rewrite -> H_x_y at 1.
And indeed the *goals* window reads:
x, y : nat
H_x_y : x = y
============================
y + y * y + (y + y) = y + y * y + (y + x)
In the (rare) occasions where we need to use the same rewrite several times in a row, tCPA lets us specify this number of times after the arrow. For example:
Restart.
intros x y H_x_y.
rewrite -> H_x_y at 4.
rewrite ->3 H_x_y at 1.
The rewritings are the same and they yield the same *goals* window.
The resource file contains another example in the proof of Proposition p2.
If one wants to use the rewrite tactic not in the goal, but in an assumption, one uses the keyword in followed by the name of the assumption:
rewrite -> ... in name_of_the_assumption.
The resource file illustrates this feature in the proof of Proposition p3, which establishes the transitivity of Leibniz equality.
If one wants to use the rewrite tactic over a specific occurrence in an assumption, one uses the keyword at followed by the index of the occurrence (counting from left to right):
rewrite -> ... in name_of_the_assumption at index_of_the_occurrence_.
The resource file illustrates this feature in the proof of Proposition p4.
All of the above (rewriting in the current goal, rewriting among the assumptions, and rewriting a specific occurrence) is achieved by writing <- instead of ->.
For example, let us revisit the first proposition:
Proposition p1' :
forall i j : nat,
i = j ->
forall f : nat -> nat,
f i = f j.
Proof.
intros i j H_i_j f.
The *goals* window then reads:
i, j : nat
H_i_j : i = j
f : nat -> nat
============================
f i = f j
We use the rewrite tactic from right to left over the assumption named H_i_j to replace j by i in the goal:
rewrite <- H_i_j.
The *goals* window then reads:
i, j : nat
H_i_j : i = j
f : nat -> nat
============================
f i = f i
Since both sides of the = sign are textually identical, we complete the proof by using the reflexivity tactic:
reflexivity.
Qed.
Sometimes, the rewrite tactic is used both from left to right and from right to left within the same proof, as in the following example. This example makes use of plus_Sn_m : forall n m : nat, S n + m = S (n + m) and plus_n_Sm : forall n m : nat, S (n + m) = n + S m:
Proposition p5 :
forall i j : nat,
S i + j = i + S j.
Proof.
intros i j.
Since plus_Sn_m i j denotes S i + j = S (i + j) and S i + j occurs in the goal, we can replace it by S (i + j) using the rewrite rule from left to right:
rewrite -> (plus_Sn_m i j).
The *goals* window then reads:
i, j : nat
============================
S i + j = i + S j
Since plus_n_Sm i j denotes S (i + j) = i + S j and i + S j occurs in the goal, we can replace it by S (i + j) using the rewrite rule from right to left:
rewrite <- (plus_n_Sm i j).
The *goals* window then reads:
i, j : nat
============================
S (i + j) = S (i + j)
The resource file contains 3 more examples (Propositions p6, p7, and p8) of rewriting left and right within the same proof. In passing, note how the proof of Proposition p7 uses Proposition p6 and how the proof of Proposition p8 uses Proposition p7.
By default, using the rewrite tactic without either of -> and <- is carried out from left to right, i.e., -> is implicit. However, for clarity, the recommended style here is to write -> explicitly.
In all the examples above and in all the accompanying files, the lemmas are fully applied. For example, just above, we wrote:
rewrite <- (plus_n_Sm i j).
Most of the time, however, there is no ambiguity, and therefore tCPA lets us write, for example:
rewrite <- plus_n_Sm.
This is a first step towards automation, but we are not there yet:
Warning
Until after the midterm project, lemmas should be fully applied, otherwise points will be deducted.
Rationale: the arguments are not always obvious, and specifying them sharpens one’s understanding in the short run and builds up effective muscle memory in the long run. Down the line, when suddenly tCPA does not do what we expect, we can fall back on this muscle memory and supply the arguments to disambiguate and move on, instead of being lost, not even knowing that we don’t know.
Not ignorance, but ignorance of ignorance, is the death of knowledge.
Halcyon (wisely): Not knowledge, but knowledge of knowledge, heralds the death of ignorance.
Fixed two typos, thanks to Kyriel Mortel Abad and Wong Kok Rui’s eagle eyes [09 Feb 2024]
Created [01 Feb 2024]