The goal of this lecture note is to make the transition from an informal proof on pen and paper to a formal proof in tCPA.
The learning goals of this lecture note are as follows:
Let us review a few typical high-school algebra problems and their informal proof.
Knowing that 0 is both left-neutral and right-neutral with respect to addition (infix +), we are asked to prove that for all natural numbers denoted by n, the following purported equality holds:
n + 0 = 0 + n
The proof proceeds by replacing equals by equals. It goes in two steps as follows.
Since 0 is right-neutral with respect to +, we know that the following equality holds for all natural numbers denoted by x:
x + 0 = x
In particular, this equality holds for n (and it then reads n + 0 = n), and so let us replace n + 0 by n on the left-hand side of the purported equality, which then reads:
n = 0 + n
(The right-hand side hasn’t changed.)
Since 0 is left-neutral with respect to +, we know that the following equality holds for all natural numbers denoted by x:
0 + x = x
In particular, this equality holds for n (and it then reads 0 + n = n), and so let us replace 0 + n by n on the right-hand side of the purported equality, which then reads:
n = n
(The left-hand side hasn’t changed.)
Since any number is equal to itself (or again, to be pedantic, since equality is a reflexive relation), the purported equality holds.
The order of the steps does not matter since they are independent: we could swap them.
If we swap them, the purported equality after the (formerly second and now) first step reads:
n + 0 = n
This purported equality holds since 0 is right-neutral with respect to +.
Overall, we have articulated the proof into logical steps, each of which we independently know to be correct.
What we actually have proved is the following stand-alone statement:
forall n : nat,
n + 0 = 0 + n
In other words, the quantification of n is part of the statement.
And the first step of the proof is: let’s pick such an n, and then prove the equality above.
In practice, one tends to write “for all natural numbers n” rather than “for all natural numbers denoted by n”.
Dana: I think there is a simpler proof than this first informal proof.
Alfrothul: Try me.
Dana: Well, yes, what we need to prove is an instance of the commutativity rule for + applied to n and 0.
Alfrothul: True that.
Pablito: The commutativity rule?
Dana: You know – for all natural numbers x and y, x + y = y + x.
Pablito: Ah, right.
Dana: Here we apply the commutativity rule to n and 0, which gives n + 0 = 0 + n.
Pablito: OK, thanks. And yes, I see what you mean: we have proved an instance of the commutativity rule.
Anton (facetious): What about instantiating the commutativity rule for + with 0 and n?
Alfrothul: That would give:
0 + n = n + 0
Dana: Well, equality is symmetric, right?
Loki: How pedantic.
Mimer: Still, Dana is right. For all natural numbers denoted by i and j, the equalities i = j and j = i are equivalent. So yes, equality is symmetric.
Alfrothul: Reflexive too.
Dana: And transitive as well.
Bong-sun: So equality is an equivalence relation?
Mimer: It is.
Knowing that + is associative and commutative, we are asked to prove that for all natural numbers denoted by x, y, and z, the following purported equality holds:
x + (y + z) = y + (x + z)
What does it mean that + is associative? It means that for all natural numbers a, b, and c, the following equality holds:
a + (b + c) = (a + b) + c
Likewise, + is commutative means that for all natural numbers a and b, the following equality holds:
a + b = b + a
The proof proceeds by (1) picking 3 natural numbers x, y, and z, and replacing equals by equals:
Applying the associativity rule to x, y, and z means that the following equality holds:
x + (y + z) = (x + y) + z
So the purported equality is equivalent to the following one, replacing the left-hand side of the equality just above by its right-hand side:
(x + y) + z = y + (x + z)
where we have operated on the left-hand side of the purported equality.
Applying the commutativity rule to x and y means that the following equality holds:
x + y = y + x
So the purported equality in Step 1 is equivalent to the following one, replacing the left-hand side of the equality just above by its right-hand side:
(y + x) + z = y + (x + z)
where we have operated on the left-hand side of the purported equality.
Applying the associativity rule to y, x, and z means that the following equality holds:
y + (x + z) = (y + x) + z
So the purported equality in Step 2 is equivalent to the following one, replacing the right-hand side of the equality just above by its left-hand side:
y + (x + z) = y + (x + z)
where we have operated on the left-hand side of the purported equality.
The left-hand side of the purported equality of Step 3 is identical to its right-hand side. Since equality is reflexive, this purported equality holds.
Still knowing that 0 is both left-neutral and right-neutral with respect to +, we are asked to prove that for all natural numbers n, the following purported equality holds:
n + 0 + 0 = 0 + 0 + n
And now is as good a time for another interlude as any, so here is one.
Anton: I know! I know! We should proceed as in the first informal proof, and argue twice that 0 is left-neutral with respect to +, and then twice that 0 is right-neutral with respect to +.
Alfrothul: Indeed. And we would end with the equality n = n.
Dana: Which holds since equality is reflexive.
Mimer: This third proof could be carried out more elegantly, though.
Anton: Now what.
Mimer: Well, we could use the first equality we proved.
Alfrothul (stonily): The first equality we proved.
Mimer (encouragingly): Yes. Look. Changing variable for clarity...
Dana: Sorry, my math is rusty. What do you mean by changing variable?
Mimer: I mean by picking another name than n in the formerly-purported-and-now-proved first equality.
Anton (slowly): OK?
Mimer: All I mean is to write it with x instead of with n. For all natural numbers x, the equality reads:
x + 0 = 0 + x
Alfrothul (slowly too): OK?
Mimer: So in particular, if we pick n + 0 as the denotation of x...
Dana: Sorry again. What do you mean by the denotation?
Mimer: I mean what x denotes. What it stands for. What it is equal to. Its value, if you like.
Dana (none too fast either): OK...
Mimer: Ah, come on. Last time, we have written definitions in Gallina, haven’t we?
Dana: Yes, for example:
Definition three : nat :=
3.
though the type annotation is optional.
Anton (helpfully): And also:
Definition successor (n : nat) : nat :=
S n.
though the type annotation is also optional.
Alfrothul (joining the fray): And this definition can also be written as:
Definition successor : nat -> nat :=
fun n : nat => S n.
though the type annotation is still optional.
Mimer: Excellent. Each definition declared a name. Here, these names are three and successor. So three, for example, denotes 3.
Loki: Magritte, here we come.
Dana: So three stands for 3.
Anton: So three is equal to 3.
Alfrothul: So 3 is, like, the value of three.
Mimer: Precisely. And you can say the same for the name successor and the function that maps a natural number to its successor. OK?
Anton, Alfrothul, and Dana (nodding): OK.
Mimer: Let’s get back to the equality:
x + 0 = 0 + x
then. In particular, if we pick n + 0 as the denotation of x, ...
Alfrothul, Dana, and Anton: Yes.
Mimer: ...this equality reads:
n + 0 + 0 = 0 + n + 0
Let me put parentheses to make it extra clear that x is replaced by n + 0:
(n + 0) + 0 = 0 + (n + 0)
Dana: Aha. So you want to use this equality from left to right and replace (n + 0) + 0 by 0 + (n + 0) in the left-hand side of the new purported equality?
Mimer: Yes.
Dana: So the new purported equality reads:
0 + (n + 0) = 0 + 0 + n
Mimer: Yes.
Anton: But now there are parentheses.
Alfrothul: Yes, but it doesn’t matter because addition is associative.
Anton: Ah, right, we can perform the two additions in either order. In fact, we can remove the parentheses:
0 + n + 0 = 0 + 0 + n
Alfrothul (reminiscing): Remember Scheme and Lisp? Parentheses are not parenthetical there.
Anton (keeping a straight face): Parentheses? Which parentheses?
Dana: Yes, yes, Anton, you are enlightened, we get it. At any rate, I think I see your point, Mimer. We can now use the first equality from left to right to replace n + 0 by 0 + n on the left-hand side, or from right to left to replace 0 + n by n + 0 on the right-hand side. Either way, we obtain an equality with the same left-hand side and right-hand side, and since equality is reflexive, we are done.
Anton: Right. If we replace n + 0 by 0 + n on the left-hand side, we obtain:
0 + (0 + n) = 0 + 0 + n
Alfrothul: And if we replace 0 + n by n + 0 on the right-hand side, we obtain:
0 + n + 0 = 0 + (n + 0)
Dana: Yes. And since addition is associative, both equalities hold.
Anton: Notice how we haven’t used the fact that 0 is neutral with respect to addition in this proof?
Alfrothul: We haven’t used it explicitly, but we have used it implicitly since it was used in the first proof.
Alfrothul: We could also use the fact that 0 + 0 = 0.
Anton: A fact? It is a corollary that 0 is neutral with respect to +.
Dana: Hum. Commutativity doesn’t help at all here.
Mimer: You guys look ready to start formalizing proofs in tCPA.
Stating a named logical statement (i.e., a lemma, or a theorem, or a proposition, or a property), tCPA issues this logical statement as a goal in the *goals* window. We then write Proof. and proceed with various proof tactics that will alter the goal until it is solved. We then conclude the proof with Qed.
So let us valiantly formalize the informal proof of the first purported equality:
Proposition first_formal_proof :
forall n : nat,
n + 0 = 0 + n.
TCPA reacts to this statement by shifting into proof mode and issuing a goal in the *goals* window:
============================
forall n : nat, n + 0 = 0 + n
In words: with no assumption, we need to prove the forall-statement. If there are any assumptions, there stand above the horizontal bar, and what we want to prove (here: a forall-statement) the goal. This goal is below the horizontal bar.
To signal that our proof is about to start, we use the following syntactic sugar:
Proof.
And from here on, we process each goal with a specific tactic.
The first step of the proof is to pick such an n, which is done with the intro tactic:
intro n.
(We could pick any other name than n, which is sometimes useful.)
The new goal reads as follows:
n : nat
============================
n + 0 = 0 + n
In words: assuming that n denotes a natural number, we need to prove the equality.
Using the Search facility, we had found that Nat.add_0_r is the theorem capturing that 0 is neutral on the right for +. Let us instantiate it with n:
Check (Nat.add_0_r n).
The following named equality appears in the *response* window:
Nat.add_0_r n
: n + 0 = n
To replace n + 0 by n in the goal (since they are equal), we use the rewrite tactic from left to right:
rewrite -> (Nat.add_0_r n).
The new goal reads as follows:
n : nat
============================
n = 0 + n
Likewise, instantiating Nat.add_0_l with n gives us the equality:
Nat.add_0_l n
: 0 + n = n
To replace 0 + n by n in the goal (since they are equal), we use the rewrite tactic from left to right:
rewrite -> (Nat.add_0_l n).
The new goal reads as follows:
n : nat
============================
n = n
The two sides of the equality are identical, and so we use the reflexivity tactic:
reflexivity.
The *response* window now says:
No more subgoals.
The proof is therefore complete, and we conclude the proof script with Qed. TCPA then exits the proof mode and comes back to its toplevel mode.
All in all, the proposition and its proof read:
Proposition first_formal_proof :
forall n : nat,
n + 0 = 0 + n.
Proof.
intro n.
rewrite -> (Nat.add_0_r n).
rewrite -> (Nat.add_0_l n).
reflexivity.
Qed.
Each step in the informal proof is echoed by a step in the formal proof.
And from now on, we can use first_formal_proof as we have used Nat.add_0_r and Nat.add_0_l. To wit, tCPA responds to Check first_formal_proof. with:
first_formal_proof
: forall n : nat, n + 0 = 0 + n
That said, are these steps the only way to carry out the proof? Of course not. For example, we could start with the right-hand side instead of the left-hand side. In tCPA, we can either re-declare the proposition and carry out the proof:
Proposition first_formal_proof' :
forall n : nat,
n + 0 = 0 + n.
Proof.
intro n.
rewrite -> (Nat.add_0_l n).
rewrite -> (Nat.add_0_r n).
reflexivity.
Qed.
Or we can tell tCPA that we want to restart the proof:
Proposition first_formal_proof'' :
forall n : nat,
n + 0 = 0 + n.
Proof.
intro n.
rewrite -> (Nat.add_0_r n).
rewrite -> (Nat.add_0_l n).
reflexivity.
Restart.
intro n.
rewrite -> (Nat.add_0_l n).
rewrite -> (Nat.add_0_r n).
reflexivity.
Qed.
Anton: I think there is a simpler proof than this first formal proof.
Alfrothul (prudent): By all means give it a try.
Dana: Well, yes, what we need to prove is an instance of Nat.add_comm applied to n and 0:
Check (Nat.add_comm n 0).
Alfrothul: Why, yes – the *response* window now contains:
Nat.add_comm n 0
: n + 0 = 0 + n
Mimer (jumping in): And rather than using rewrite and then reflexivity, we can exploit this coincidence between the goal and the instance of Nat.add_comm applied to n and 0 using the exact tactic. Look:
exact (Nat.add_comm n 0).
Anton: Indeed – the *response* window now says:
No more subgoals.
Alfrothul: The proof is therefore complete, and we can conclude it with Qed.
Anton (facetious): As I said in the interlude about the first informal proof, what about instantiating the commutativity rule for + with 0 and n? Look:
Check (Nat.add_comm 0 n).
Alfrothul: Well, the *response* window now says:
Nat.add_comm 0 n
: 0 + n = n + 0
Mimer: And actually, tCPA features a tactic called symmetry to swap both sides of the equality in the goal.
Anton: Ah. So all we need to do is write:
symmetry.
exact (Nat.add_comm 0 n).
Mimer: That’s the spirit.
So far, we know:
Let us consolidate this knowledge by formalizing another proof.
So let us intrepidly formalize the informal proof of the second purported equality:
Proposition second_formal_proof :
forall x y z : nat,
x + (y + z) = y + (x + z).
TCPA reacts to this statement by issuing a goal in the *goals* window:
============================
forall x y z : nat, x + (y + z) = y + (x + z)
In words: with no assumption, we need to prove the forall-statement.
To signal that our proof is about to start, we use the following syntactic sugar:
Proof.
And from here on, we process each goal with a specific tactic.
The first step of the proof is to pick such an x, which is done with the intro tactic:
intro x.
The new goal reads as follows:
x : nat
============================
forall y z : nat, x + (y + z) = y + (x + z)
In words: assuming that x denotes a natural number, we need to prove the quantified equality.
The next goal is also a universal quantification, and so will the goal after it, so we use the intro tactic twice more:
intro y.
intro z.
The new goal reads as follows:
x, y, z : nat
============================
x + (y + z) = y + (x + z)
In words: assuming that x, y, and z denote natural numbers, we need to prove the equality.
In practice, rather than using the intro tactic repeatedly, we use the intros tactic once:
Restart.
intros x y z.
The goal is the same as just above.
In the informal proof, we applied the associativity rule to x, y, and z. In the formal proof, the associativity rule is called Nat.add_assoc, and we can apply it too:
Check (Nat.add_assoc x y z).
The following named equality appears in the *response* window:
Nat.add_assoc x y z
: x + (y + z) = x + y + z
To replace x + (y + z) by x + y + z in the goal (since they are equal, by the named equality), we use the rewrite tactic from left to right:
rewrite -> (Nat.add_assoc x y z).
The new goal in the *goals* window reads as follows:
x, y, z : nat
============================
x + y + z = y + (x + z)
In the informal proof, we then applied the commutativity rule to x and y. In the formal proof, the commutativity rule is called Nat.add_comm, and we can apply it too:
Check (Nat.add_comm x y).
The following named equality appears in the *response* window:
Nat.add_comm x y
: x + y = y + x
To replace x + y by y + x in the goal (since they are equal, by the named equality), we use the rewrite tactic from left to right:
rewrite -> (Nat.add_comm x y).
The new goal in the *goals* window reads as follows:
x, y, z : nat
============================
y + x + z = y + (x + z)
In the informal proof, we then applied the associativity rule to y, x, and z. In the formal proof, the commutativity rule is called Nat.add_comm, and we can apply it too:
Check (Nat.add_assoc y x z).
The following named equality appears in the *response* window:
Nat.add_assoc y x z
: y + (x + z) = y + x + z
To replace y + x + z by y + (x + z) in the goal (since they are equal, by the named equality), we use the rewrite tactic from right to left:
rewrite <- (Nat.add_assoc y x z).
The new goal reads as follows:
x, y, z : nat
============================
y + (x + z) = y + (x + z)
The two sides of the equality are identical, and so we use the reflexivity tactic:
reflexivity.
The *response* window now says:
No more subgoals.
The proof is therefore complete, and we conclude the proof script with Qed. All in all, the proposition and its proof read:
Proposition second_formal_proof :
forall x y z : nat,
x + (y + z) = y + (x + z).
Proof.
intros x y z.
rewrite -> (Nat.add_assoc x y z).
rewrite -> (Nat.add_comm x y).
rewrite <- (Nat.add_assoc y x z).
reflexivity.
Qed.
Each step in the informal proof is echoed by a step in the formal proof.
And as for the first formal proof, these steps are not the only way to carry out the proof.
So let us fearlessly formalize the informal proof of the third purported equality:
Proposition third_formal_proof :
forall n : nat,
n + 0 + 0 = 0 + 0 + n.
TCPA reacts to this statement by issuing a goal in the *goals* window:
============================
forall n : nat, n + 0 + 0 = 0 + 0 + n
In words: with no assumption, we need to prove the forall-statement.
Let us start our proof:
Proof.
Since the goal is a forall-statement, we use the intro tactic:
intro n.
The new goal reads as follows:
n : nat
============================
n + 0 + 0 = 0 + 0 + n
In words: assuming that n denotes a natural number, we need to prove an equality.
Anton: I think I know. Let’s proceed as in the first formal proof,and argue twice that 0 is neutral on the left of +, and then twice that 0 is neutral on the right of +.
Alfrothul: Nat.add_0_r should do the job. Let me check:
Check (Nat.add_0_r n).
Anton: It does, witness the following named equality in the *response* window:
Nat.add_0_r n
: n + 0 = n
Alfrothul: Assuming I understand right, to replace n + 0 by n in the goal, we should use the rewrite tactic from left to right:
rewrite -> (Nat.add_0_r n).
Anton: That is correct. Look at the new goal in the *goals* window:
n : nat
============================
n + 0 = 0 + 0 + n
Alfrothul: Well, we have another occurrence of n + 0, so I guess we should do the same again:
rewrite -> (Nat.add_0_r n).
Anton: That is correct too, witness the new goal in the *goals* window:
n : nat
============================
n = 0 + 0 + n
Pablito: I know! I know! We should just do the same, but this time with Nat.add_0_l to simplify the addition on the left:
rewrite -> (Nat.add_0_l n).
Pablito: Ah, I actually don’t know. We get the following message in the *response* window:
Error: Found no subterm matching "0 + n" in the current goal.
Anton: How about we check first:
Check (Nat.add_0_l n).
Pablito: Well, the result is as it should be in the *response* window:
Nat.add_0_l n
: 0 + n = n
Pablito: I don’t get what I see.
Dana: And yet what you don’t see is what you get. Addition is associative and tCPA doesn’t print parentheses, but the goal is actually (0 + 0) + n.
Alfrothul: Ah, so we should go with Nat.add_0_l 0:
rewrite -> (Nat.add_0_l 0).
Anton: That has the effect of replacing 0 + 0 by 0 in the goal, look:
n : nat
============================
n = 0 + n
Dana (kindly): And now we can use your idea, Pablito:
rewrite -> (Nat.add_0_l n).
Pablito: I get it, thanks. And then we can use the reflexivity tactic since the goal is n = n. Or we could have used the symmetry tactic, which would exactly give us the equality provided by Nat.add_0_l n. See?
Alfrothul: Either way, Qed, here we come.
Anton: Wait. Didn’t Mimer mumble something about elegance, in the informal interlude?
Pablito (helpfully): He said we could use the first equality we proved.
Alfrothul: But then we should write Restart., which sure enough restores the initial goal in the *goals* window:
============================
forall n : nat, n + 0 + 0 = 0 + 0 + n
Dana: Let me check this first equality:
Check first_formal_proof.
Dana: Right. The result is in the *response* window:
first_formal_proof
: forall n : nat, n + 0 = 0 + n
Anton: Mimer said we should apply it to n + 0:
intro n.
Check (first_formal_proof (n + 0)).
Alfrothul: Check out the result in the *response* window:
first_formal_proof (n + 0)
: n + 0 + 0 = 0 + (n + 0)
Anton: I guess we could rewrite n + 0 + 0 in the goal:
rewrite -> (first_formal_proof (n + 0)).
Alfrothul: Aha. The *goals* windows now reads:
n : nat
============================
0 + (n + 0) = 0 + 0 + n
Dana: And now we could use the first equality again, this time by applying it to n:
Check (first_formal_proof n).
Alfrothul: Check out the result in the *response* window:
first_formal_proof n
: n + 0 = 0 + n
Anton: So let’s replace n + 0 by 0 + n:
rewrite -> (first_formal_proof n).
Alfrothul: The *goals* window now reads:
n : nat
============================
0 + (0 + n) = 0 + 0 + n
Dana: The goal is an instance of Nat.add_assoc, isn’t it:
Check (Nat.add_assoc 0 0 n).
Alfrothul: Indeed it is. Check out the result in the *response* window:
Nat.add_assoc 0 0 n
: 0 + (0 + n) = 0 + 0 + n
Anton: So we can use the exact tactic:
exact (Nat.add_assoc 0 0 n).
Pablito. And we are done. Qed, anyone?
Alfrothul: Wait. Couldn’t we use the fact that 0 + 0 = 0?
Anton (virtuously): You mean the corollary that 0 is left-neutral with respect to +?
Loki: Or right-neutral.
Anton: Either way:
Restart.
intro n.
Check (Nat.add_0_l 0).
Alfrothul: Yes, yes, the *response* window says at much:
Nat.add_0_l 0
: 0 + 0 = 0
Anton: So here we go:
rewrite -> (Nat.add_0_l 0).
Alfrothul: And now the *goals* window reads:
n : nat
============================
n + 0 + 0 = 0 + n
Anton: We can replace n + 0 by n:
rewrite -> (Nat.add_0_r n).
Alfrothul: Wow, we obtain our first equality:
n : nat
============================
n + 0 = 0 + n
Anton: So we can conclude the proof with:
exact (first_formal_proof n).
Pablito. And we are done. Again. Qed, anyone?
Dana: What is it with mathematicians wanting to re-prove their theorems? I mean same same is not that different.
Loki: Practicing our Singlish are we.
Dana: The point is that once a theorem is proved, it is proved, so why proving it again? I now understand the temptation, witness the present interlude, but why is that?
Pablito: I once heard a writer say that to write is to rewrite.
Alfrothul: But to prove is to improve?
Anton: Mimer did mumble something about elegance.
Mimer (judiciously): What is it with computer scientists wanting to re-implement their programs?
Anton: That’s different.
Mimer: Is it?
Halcyon (wondering): So to curse is to recurse?Loki: Yup. And to dress is to redress.Dana (playing along): And to act is to react?Alfrothul: To heat is to reheat?Halcyon (enjoying himself): To verse is to reverse.Loki: Well, for palindromes, maybe.Mimer (who could not resist): To do nothing is to re-reverse.
Prove, in more than one way, that the following propositions hold:
Proposition foo :
forall n1 n2 n3 n4 : nat,
n1 + (n2 + (n3 + n4)) = ((n1 + n2) + n3) + n4.
Proposition bar :
forall n1 n2 n3 n4 : nat,
((n1 + n2) + n3) + n4 = n4 + (n3 + (n2 + n1)).
Proposition baz :
forall n1 n2 n3 n4 : nat,
((n1 + n3) + n2) + n4 = n4 + (n2 + (n3 + n1)).
Prove that the following propositions hold, without using Nat.add_1_r:
Proposition plus_one :
forall n : nat,
n + 1 = S n.
Proposition plus_two :
forall n : nat,
n + 2 = S (S n).
Proposition plus_three :
forall n : nat,
n + 3 = S (S (S n)).
Prove the binomial expansion at rank 2:
Proposition binomial_expansion_2 :
forall x y : nat,
(x + y) * (x + y) = x * x + 2 * (x * y) + y * y.
N.B.: Make sure to supply all the arguments to all the lemmas that you apply.
Mimer: You guys want some guidance?
Dana: Sure. And thanks.
Mimer: First, let’s prove some warmup lemmas.
Alfrothul: Warmup lemmas?
Mimer: Good point, Alfrothul. The reality of proving is that you first start a proof and see where it leads you, and then at the end you identify how to state your proof in a way that is simpler, or more structured, or more telling, or more reusable. Typically you then write a couple of auxiliary lemmas that will streamline the proof of your theorem, and then you rewrite this proof.
Alfrothul: So to prove is really to improve, it was not just a pun.
Mimer: Indeed it wasn’t.
Pablito: How do we write auxiliary lemmas?
Mimer: There is no simple answer to that, but with a bit of practice you will soon get the hang of it.
Alfrothul: And stating auxiliary lemmas is not predicting the future, it is a sign that the proof has been redone.
Mimer: Very often, yes.
Dana: So, the warmup lemmas?
Mimer: First, let’s prove that 1 is neutral on the left of multiplication.
Anton: Why should we do that? This lemma is in one of the Coq libraries, look:
Check Nat.mul_1_l.
Pablito (helpful): The *response* window reads:
Nat.mul_1_l : forall n : nat, 1 * n = n
Dana: Also, this property is kind of a long way from proving the correctness of binomial expansion at rank 2.
Mimer: You are both right of course. But the proof of this lemma is a warmup for the proof of the next lemma, and also their proof use the inductive properties of the multiplication function, which you are now familiar with, look:
Search (0 * _ = _).
Pablito: The *response* window reads:
Nat.mul_0_l: forall n : nat, 0 * n = 0
Anton: Ah, right, it’s the base case of the multiplication function.
Mimer: Yes it is. And now let’s look for the induction step of the multiplication function:
Search (S _ * _ = _ + _).
Pablito: The *response* window reads:
Nat.mul_succ_l: forall n m : nat, S n * m = n * m + m
Alfrothul: OK Mimer. As usual, you make us start from what we know. Please play on.
Mimer: Here we go:
Lemma mul_1_l :
forall x : nat,
1 * x = x.
Proof.
intro x.
Check (Nat.mul_succ_l 0 x).
Pablito: The *response* window reads:
Nat.mul_succ_l 0 x : 1 * x = 0 * x + x
Mimer: Let us use this Leibniz equality to rewrite 1 * x in the goal:
rewrite -> (Nat.mul_succ_l 0 x).
Pablito: The *goals* window now reads:
x : nat
============================
0 * x + x = x
Mimer: And now we can use the base case of multiplication, look:
Check (Nat.mul_0_l x).
Pablito: The *response* window reads:
Nat.mul_0_l x : 0 * x = 0
Mimer: Let us use this Leibniz equality to rewrite 0 * x in the goal:
rewrite -> (Nat.mul_0_l x).
Pablito: The *goals* window now reads:
x : nat
============================
0 + x = x
Mimer: And that’s a case for the base case of the addition function, which you are also familiar with by now:
Check (Nat.add_0_l x).
Pablito: The *response* window reads:
Nat.add_0_l x : 0 + x = x
Mimer: This Leibniz equality coincides with the goal, so we can use the exact tactic to complete the proof:
exact (Nat.add_0_l x).
Qed.
Dana: OK.
Mimer: Here is a second warmup lemma:
Lemma twice :
forall x : nat,
x + x = 2 * x.
Proof.
intro x.
Dana: We are still a long way from proving the correctness of binomial expansion at rank 2, but I do see that to prove Lemma twice, we are going to use an instance of the induction step of the multiplication function:
Check (Nat.mul_succ_l 1 x).
Pablito: The *response* window reads:
Nat.mul_succ_l 1 x : 2 * x = 1 * x + x
Mimer: Yes. Let us use this Leibniz equality to rewrite 2 * x in the goal:
rewrite -> (Nat.mul_succ_l 1 x).
Pablito: The *goals* window now reads:
x : nat
============================
x + x = 1 * x + x
Anton: I see 1 * x in the goal, so we are going to use mul_1_l, right?
Bong-sun: Let me see:
Check (mul_1_l x).
Pablito: The *response* window reads:
mul_1_l x : 1 * x = x
Mimer: Yes, let’s:
rewrite -> (mul_1_l x).
Pablito: The *goals* window now reads:
x : nat
============================
x + x = x + x
Mimer: The left-hand side of the equality is the same as its right-hand side, so since Leibniz equality is reflexive, we use the reflexivity tactic to complete the proof:
reflexivity.
Qed.
Anton: OK. So that’s two warmup lemmas, and I do see how the first warmed us up for the second. Shall we prove the theorem now?
Mimer: Almost. Let me first state the following helpful lemma:
Lemma helpful :
forall a b c : nat,
a + b + b + c = a + 2 * b + c.
Proof.
intros a b c.
Pablito: The *goals* window now reads:
a, b, c : nat
============================
a + b + b + c = a + 2 * b + c
Mimer: The issue here is that addition is left-associative:
Check Nat.add_assoc.
Pablito: The *response* window reads:
Nat.add_assoc : forall n m p : nat, n + (m + p) = n + m + p
Alfrothul: Ah, right. So we need to reassociate the additions in order to have b + b as a sub-expression in the left-hand side, and then we can use Lemma twice.
Mimer: Precisely:
Check (Nat.add_assoc a b b).
Pablito: The *response* window reads:
Nat.add_assoc a b b : a + (b + b) = a + b + b
Mimer: The right-hand side of this Leibniz equality is a sub-expression in the goal, so let us replace this sub-expression by the left-hand side of this Leibniz equality:
rewrite <- (Nat.add_assoc a b b).
Pablito: The *goals* window now reads:
a, b, c : nat
============================
a + (b + b) + c = a + 2 * b + c
Mimer: As you said, Alfrothul, we are now in position to use Lemma twice:
Check (twice b).
Pablito: The *response* window reads:
twice b : b + b = 2 * b
Mimer: The left-hand side of this Leibniz equality is a sub-expression in the goal, so let us replace this sub-expression by the right-hand side of this Leibniz equality:
rewrite -> (twice b).
Pablito: The *goals* window now reads:
a, b, c : nat
============================
a + 2 * b + c = a + 2 * b + c
Mimer: The left-hand side of the equality is the same as its right-hand side, so let use the reflexivity tactic to complete the proof:
reflexivity.
Qed.
Dana: OK. Will we need other auxiliary lemmas?
Mimer: Actually no, we are good to go:
Theorem binomial_expansion_2 :
forall x y : nat,
(x + y) * (x + y) = x * x + 2 * (x * y) + y * y.
Proof.
intros x y.
Pablito: The *goals* window now reads:
x, y : nat
============================
(x + y) * (x + y) = x * x + 2 * (x * y) + y * y
Mimer: Let us distribute (x + y) over the addition of x and y from right to left.
Anton: Sounds good. How do we do that?
Bong-sun: Let me see. How about we use the Search facility:
Search ((_ + _) * _ = _).
Pablito: The *response* window reads:
Nat.mul_add_distr_r: forall n m p : nat, (n + m) * p = n * p + m * p
Anton: Ah, OK.
Mimer: Let’s instantiate Nat.mul_add_distr_r with x, y, and (x + y):
Check (Nat.mul_add_distr_r x y (x + y)).
Pablito: The *response* window reads:
Nat.mul_add_distr_r x y (x + y) : (x + y) * (x + y) = x * (x + y) + y * (x + y)
Mimer: The left-hand side of this Leibniz equality is a sub-expression in the goal, so let us replace this sub-expression by the right-hand side of this Leibniz equality:
rewrite -> (Nat.mul_add_distr_r x y (x + y)).
Pablito: The *goals* window now reads:
x, y : nat
============================
(x + y) * (x + y) = x * x + 2 * (x * y) + y * y
Mimer: Now let us distribute x over the addition of x and y from left to right.
Anton: Let me guess:
Check Nat.mul_add_distr_l.
Pablito: The *response* window reads:
Nat.mul_add_distr_l : forall n m p : nat, n * (m + p) = n * m + n * p
Mimer: Good guess, Anton. Let’s instantiate Nat.mul_add_distr_l with x, x, and y:
Check (Nat.mul_add_distr_l x x y).
Pablito: The *response* window reads:
Nat.mul_add_distr_l x x y : x * (x + y) = x * x + x * y
Mimer: The left-hand side of this Leibniz equality is a sub-expression in the goal, so let us replace this sub-expression by the right-hand side of this Leibniz equality:
rewrite -> (Nat.mul_add_distr_l x x y).
Pablito: The *goals* window now reads:
x, y : nat
============================
x * x + x * y + y * (x + y) = x * x + 2 * (x * y) + y * y
Mimer: Good. Now let us distribute y over the addition of x and y from left to right:
Check (Nat.mul_add_distr_l y x y).
Pablito: The *response* window reads:
Nat.mul_add_distr_l y x y : y * (x + y) = y * x + y * y
Mimer: The left-hand side of this Leibniz equality is a sub-expression in the goal, so let us replace this sub-expression by the right-hand side of this Leibniz equality:
rewrite -> (Nat.mul_add_distr_l y x y).
Pablito: The *goals* window now reads:
x, y : nat
============================
x * x + x * y + (y * x + y * y) = x * x + 2 * (x * y) + y * y
Mimer: Now we need to reassociate these additions:
Check Nat.add_assoc.
Pablito: The *response* window reads:
Nat.add_assoc : forall n m p : nat, n + (m + p) = n + m + p
Mimer: Let me see. How about we instantiate Nat.add_assoc with the first argument of the outer addition, i.e., x * x + x * y...
Anton: The first argument of the outer addition?
Dana: That’s because Gallina implicitly associates additions to the left.
Mimer: Correct. ...and then with the first argument of the inner addition and with its second argument:
Check (Nat.add_assoc (x * x + x * y) (y * x) (y * y)).
Pablito: The *response* window reads:
Nat.add_assoc (x * x + x * y) (y * x) (y * y) : x * x + x * y + (y * x + y * y) = x * x + x * y + y * x + y * y
Mimer: Good. The left-hand side of this Leibniz equality is a sub-expression in the goal, so let us replace this sub-expression by the right-hand side of this Leibniz equality:
rewrite -> (Nat.add_assoc (x * x + x * y) (y * x) (y * y)).
Pablito: The *goals* window now reads:
x, y : nat
============================
x * x + x * y + y * x + y * y = x * x + 2 * (x * y) + y * y
Mimer: Now we have x + y and y + x in the goal. Let us commute this second addition:
Check Nat.mul_comm.
Pablito: The *response* window reads:
Nat.mul_comm : forall n m : nat, n * m = m * n
Mimer: Let us instantiate Nat.mul_comm with y and x to get what we need:
Check (Nat.mul_comm y x).
Pablito: The *response* window reads:
Nat.mul_comm y x : y * x = x * y
Mimer: Good. The left-hand side of this Leibniz equality is a sub-expression in the goal, so let us replace this sub-expression by the right-hand side of this Leibniz equality:
rewrite -> (Nat.mul_comm y x).
Pablito: The *goals* window now reads:
x, y : nat
============================
x * x + x * y + x * y + y * y = x * x + 2 * (x * y) + y * y
Mimer: Now we have an instance of the helpful lemma:
Check (helpful (x * x) (x * y) (y * y)).
Pablito: The *response* window reads:
helpful (x * x) (x * y) (y * y) : x * x + x * y + x * y + y * y = x * x + 2 * (x * y) + y * y
Mimer: So we can conclude the proof using rewrite and then reflexivity or more simply using exact:
exact (helpful (x * x) (x * y) (y * y)).
Qed.
Alfrothul: Thanks, Mimer.
Mimer: You are most welcome. Hope you found this guidance to be helpful.
Dana: It was, thanks, especially how the helpful lemma is helpful right at the end of the proof.
Alfrothul: In that sense, Lemma twice is a helpful lemma for Lemma helpful.
Bong-sun: And Lemma mul_1_l is a helpful lemma for Lemma twice.
Mimer: Guys, that’s exactly the idea.
Loki (sotto voce): Your helpful lemmas have helpful lemmas.
Mimer: And when a helpful lemma is repeatedly used, it is promoted into a library.
Alfrothul: It’s not unlike programming. We use auxiliary functions that might have auxiliary functions, and when an auxiliary function is repeatedly used, we put it into a library.
Mimer: After a while, you guys will be less and less interested in other people’s proofs, but you will always be interested in their helpful lemmas.
At the end of the solution for Exercise 03, the proof of Theorem binomial_expansion_2 starts by distributing on the right, and then it continues by distributing on the left. Write an alternative proof that starts by distributing on the left, and then continues by distributing on the right.
Prove the following theorems as corollaries of what you have proved so far:
Theorem foo :
forall x : nat,
(x + 1) * (x + 1) = x * x + 2 * x + 1.
Theorem bar :
forall x : nat,
S x * S x = S (x * x + 2 * x).
Theorem baz :
forall x : nat,
S x * S x = S (S (S x) * x).
Hint: For any given x : nat, consider an instance of Theorem binomial_expansion_2 with x and 1, i.e., write:
intro x.
Check (binomial_expansion_2 x 1).
Using Nat.add_assoc and Nat.add_comm, prove the following lemmas found in the Arith library:
Lemma add_shuffle0 :
forall n m p : nat,
n + m + p = n + p + m.
Proof.
exact Nat.add_shuffle0.
Restart.
Abort.
Lemma add_shuffle1 :
forall n m p q : nat,
n + m + (p + q) = n + p + (m + q).
Proof.
exact Nat.add_shuffle1.
Restart.
Abort.
Lemma add_shuffle2 :
forall n m p q : nat,
n + m + (p + q) = n + q + (m + p).
Proof.
exact Nat.add_shuffle2.
Restart.
Abort.
Added Exercise 06 [02 Feb 2025]
Added the solution for Exercise 03, Exercise 04, and Exercise 05 [02 Feb 2025]
Created [31 Jan 2025]