The goal of this chapter is to introduce the simpl tactic, to reflect about the injection tactic, and to introduce the do tactic.
The simpl tactic allegedly simplifies the current goal – and it does, after a fashion, though in an unpredictable way. Example:
Lemma foo :
forall n : nat,
1 + n = n + 1.
Proof.
intro n.
The *goals* window reads:
n : nat
============================
1 + n = n + 1
Let us use the simpl tactic:
simpl.
The *goals* window reads:
n : nat
============================
S n = n + 1
Somehow, it has simplified the left-hand side, but not the right-hand side, which is unintuitive... unless we realize that part of what simpl does is unfolding the calls to recursive functions whose inductive variable is known. With that in mind, it is simple (so to speak) to reproduce – and therefore understand – what simpl does. Here, it exploits the fact that Nat.add is defined recursively on its first argument:
Print Nat.add.
The *response* window then reads ({struct n} is an internal annotation to convey that add is defined recursively over n):
Nat.add = fix add (n m : nat) {struct n} : nat := match n with
| 0 => m
| S p => S (add p m)
end
: nat -> nat -> nat
With that, let us reproduce what simpl just did:
Abort.
Definition fold_unfold_add_O := Nat.add_0_l.
Definition fold_unfold_add_S := plus_Sn_m.
Lemma foo :
forall n : nat,
1 + n = n + 1.
Proof.
intro n.
rewrite -> (fold_unfold_add_S 0 n).
rewrite -> (fold_unfold_add_O n).
The *goals* window reads:
n : nat
============================
S n = n + 1
We can then complete the proof:
rewrite <- (plus_n_Sm n 0).
rewrite -> (Nat.add_0_r n).
reflexivity.
Anton: Let me work out another example.
Alfrothul: Sure. Do you have one in mind?
Anton: I do:
Lemma bar :
forall n : nat,
1 * n = n * 1.
Proof.
intro n.
Alfrothul: OK.
Anton: If we use the simpl tactic, the *goals* window then reads:
n : nat
============================
n + 0 = n * 1
Alfrothul: OK. Why is that?
Anton: Let me check the definition of the multiplication function:
Print Nat.mul.
Alfrothul (helpful): The *response* window reads:
Nat.mul = fix mul (n m : nat) {struct n} : nat := match n with
| 0 => 0
| S p => m + mul p m
end
: nat -> nat -> nat
Anton: Well, it’s the canonical implementation that is recursive on its first argument, look:
Print mul.
Alfrothul (helpful): The *response* window reads:
mul = fix mul (n m : nat) {struct n} : nat := match n with
| 0 => 0
| S n' => m + mul n' m
end
: nat -> nat -> nat
Anton: See how the two printouts are the same?
Alfrothul: I do. The implementation is the canonical one that is recursive on its first argument.
Anton: Right. So when given 1 * n = n * 1, the simpl tactic unfolds the calls to the multiplication function when the top constructor of this argument is known.
Alfrothul: And that explains the resulting goal n + 0 = n * 1. On the left-hand side, i.e., 1 * n, which is syntactic sugar for Nat.mul 1 n, the call to Nat.mul is unfolded twice, which yields n + 0.
Anton: Whereas on the right-hand side, i.e., n * 1, the first argument is not constant and so the call to Nat.mul is not unfolded.
Alfrothul: Actually, on the left-hand side, the result is n + 0 – which is syntactic sugar for Nat.add n 0 – because Nat.add is recursive on its first argument too, and so since n is not constant, the call to Nat.add is not unfolded either.
Anton (definite): That explains.
Alfrothul (conciliatory): It probably does, but, huh, it explains what? And also what explains whatever it is that is explained, if I may ask?
Anton (animatedly): That explain two things: 1. why we needed to prove forall n : nat, n * 1 = n by induction, and 2. why we could prove forall n : nat, 1 * n = n with the fold-unfold lemmas associated to the multiplication function and to the addition function.
Alfrothul: Indeed it does, since we use the fold-unfold lemmas to unfold calls to functions that are recursive on one of their arguments when the top constructor of this argument is known.
Anton: So simpl automates that.
Mimer: Indeed it does.
Pablito: OK. So how do we complete the proof here?
Anton: We use Nat.add_0_r and Nat.mul_1_r, which were proved by induction. It all makes sense.
Bong-sun: Can I check something?
Anton: By all means.
Bong-sun: Let me see:
Lemma baz :
forall x y z : nat,
S x * y = S (S x) * z.
Proof.
intros x y z.
Alfrothul: This lemma clearly does not hold, but that is not why you stated it, right?
Bong-sun: Right. On the left-hand side, the first argument of the multiplication function has one known top constructor, and on the right-hand side, the first argument has two. So based on what you said, if we use the simpl tactic, three calls should be unfolded.
Alfrothul: I see. Then on the left-hand side, the result should be y + x * y.
Anton: And on the left-hand side, the result should be z + (z + x * z).
Bong-sun: Let’s try:
simpl.
Halcyon: Success! The *goals* window reads:
x, y, z : nat
============================
y + x * y = z + (z + x * z)
Dana: Most of the time, though, the simpl tactic is overzealous: if it finds something – anything – to simplify, it will simplify it, at the risk of the user losing their overview and sinking in a sea of irrelevant details.
Alfrothul: True, that. So the sane way to use the simpl tactic is to give it an argument, namely the expression in the goal that we want to simplify. This way, we stay in control.
Bong-sun: So just above, I should not have written simpl., I should first have written:
simpl (S x * y).
Pablito: And then the *goals* window would have read:
x, y, z : nat
============================
y + x * y = S (S x) * z
Bong-sun: Thanks. And then I should have written:
simpl (S (S x) * z).
Pablito: And then the *goals* window would have read:
x, y, z : nat
============================
y + x * y = z + (z + x * z)
Alfrothul: Which is the same result, but we are more in control.
Loki: So between not knowing that you don’t know and knowing that you know, you have chosen.
Bong-sun: I guess we have.
The sane way to use the simpl tactic is to give it an argument: the expression in the goal that we want to simplify. This way, we stay in control.
The accompanying resource file revisits the soundness and completeness of the parity predicates. At one point, the *goals* window reads:
n' : nat
EIHn' : (exists q : nat, n' = 2 * q) -> evenp n' = true
OIHn' : (exists q : nat, n' = S (2 * q)) -> oddp n' = true
q : nat
H_q : S n' = S (S (2 * q))
============================
exists q0 : nat, n' = S (2 * q0)
We want to use the injection tactic to strip the S constructor in the assumption denoted by H_q:
injection H_q as H_n'.
Unfortunaly tCPA first zealously simplifies the LHS and the RHS of H_n', and so the resulting assumption is not directly usable:
n' : nat
EIHn' : (exists q : nat, n' = 2 * q) -> evenp n' = true
OIHn' : (exists q : nat, n' = S (2 * q)) -> oddp n' = true
q : nat
H_n' : n' = S (q + (q + 0))
============================
exists q0 : nat, n' = S (2 * q0)
Since the simplification arises because the multiplier is constant (since the multiplication function is defined recursively over its first argument – a.k.a. the multiplier), to prevent the simplification, we can commute the multiplier and the multiplicand before and after using the injection tactic:
rewrite -> Nat.mul_comm in H_q; injection H_q as H_n'; rewrite <- Nat.mul_comm in H_n'.
The *goals* window then reads:
n' : nat
EIHn' : (exists q : nat, n' = 2 * q) -> evenp n' = true
OIHn' : (exists q : nat, n' = S (2 * q)) -> oddp n' = true
q : nat
H_n' : n' = S (2 * q)
============================
exists q0 : nat, n' = S (2 * q0)
And we can serenely proceed.
Halcyon (wisely): Mechanism, not solution.Mao Zedong: Yup.
Given a natural number n and a tactic t, the do tactic invokes t n times in a row:
If t cannot be invoked n times, an error occurs and t is not invoked at all.
So for example, rewrite <-3 plus_n_Sm and do 3 (rewrite <- plus_n_Sm) are equivalent.
Prove that for any natural number n strictly greater than 3, 2^n < n!.
See the accompanying resource file. The solution uses both simpl and do. It also selectively uses lemmas without applying them to all their arguments, when there is no ambiguity.
Given a tactic t, the repeat tactic invokes this tactic repeatedly until it does not apply anymore.
So for example, here are three equivalent proofs, the last of which illustrates the repeat tactic:
Lemma a_simple_example_for_the_repeat_tactic :
forall x : nat,
x + 4 = S (S (S (S (x + 0)))).
Proof.
intro x.
ring.
Restart.
intro x.
rewrite <-4 plus_n_Sm.
reflexivity.
Restart.
intro x.
repeat (rewrite <- plus_n_Sm).
reflexivity.
Qed.
An unbounded repetition can make tCPA diverge:
Lemma twice :
forall x : nat,
2 * x = x + x.
Proof.
intro x.
ring.
Restart.
intro x.
repeat (rewrite -> Nat.mul_comm).
Added a section about the repeat tactic and an interlude about the simpl tactic [06 Jun 2025]
Moved the section about the ring tactic and the interlude to Chapter The ring tactic in Week 07 [05 Jun 2025]
Added a section about the ring tactic, an interlude, and Section A perspicuous use of the injection tactic [30 Mar 2025]
Detailed the solution for Exercise 01 some more in the accompanying resource file [30 Mar 2025]
Fixed the name of a .v file, thanks to Lei Jianwen’s eagle eye [29 Mar 2025]
Created [28 Mar 2025]