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 (which is short for “the Coq Proof Assistant”).
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.
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.
TCPA provides another form of toplevel form, named logical statements:
<toplevel-form> ::= Compute <expression>
| Check <expression>
| <definition>
| <named-logical-statement>
<named-logical-statement> ::= <qualifier> <identifier> : <proposition>
<qualifier> ::= Theorem | Lemma | Proposition | Property | Corollary
<proposition> ::= <expression> = <expression>
| True
| False
| ~ <proposition>
| <proposition> -> <proposition>
| <proposition> /\ <proposition>
| <proposition> \/ <proposition>
| forall <identifier> { : <type> }?, <proposition>
| exists <identifier> { : <type> }?, <proposition>
| <identifier>
In words:
Thus equipped, we can formalize the soundness, e.g., of the evenp predicate as follows:
Theorem soundness_of_evenp (evenp : nat -> bool) :
forall n : nat,
evenp n = true ->
exists m : nat,
n = 2 * m.
(In words: if applying the evenp predicate to a natural number yields true, then this natural number is even.)
And likewise for its completeness:
Theorem completeness_of_evenp (evenp : nat -> bool) :
forall n : nat,
(exists m : nat,
n = 2 * m) ->
evenp n = true.
(In words: if a natural number is even, then applying applying the evenp predicate to this natural number yields true.)
These two statements are syntactically correct with respect to the grammar above, witness the following derivation and the following abstract-syntax tree:
the (left-to-right) derivation:
<toplevel-form>
-->
<named-logical-statement>
-->
<qualifier> <identifier> : <proposition>
-->
Theorem <identifier> : <proposition>
-->
Theorem soundness_of_evenp : <proposition>
-->
Theorem soundness_of_evenp : forall <identifier> : <type>, <proposition>
-->
Theorem soundness_of_evenp : forall even : <type>, <proposition>
-->
Theorem soundness_of_evenp : forall even : <type> -> <type>, <proposition>
-->
Theorem soundness_of_evenp : forall even : nat -> <type>, <proposition>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, <proposition>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall <identifier> : <type>, <proposition>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : <type>, <proposition>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : nat, <proposition>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : nat, <proposition> -> <proposition>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : nat, <expression> = <expression> -> <proposition>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : nat, <expression> <expression> = <expression> -> <proposition>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : nat, <identifier> <expression> = <expression> -> <proposition>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : nat, evenp <expression> = <expression> -> <proposition>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : nat, evenp <identifier> = <expression> -> <proposition>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : nat, evenp n = <expression> -> <proposition>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : nat, evenp n = <boolean> -> <proposition>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : nat, evenp n = true -> <proposition>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : nat, evenp n = true -> exists <identifier> : <type>, <proposition>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : nat, evenp n = true -> exists m : <type>, <proposition>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : nat, evenp n = true -> exists m : nat, <proposition>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : nat, evenp n = true -> exists m : nat, <expression> = <expression>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : nat, evenp n = true -> exists m : nat, <identifier> = <expression>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : nat, evenp n = true -> exists m : nat, n = <expression>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : nat, evenp n = true -> exists m : nat, n = <expression> * <expression>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : nat, evenp n = true -> exists m : nat, n = <natural-number> * <expression>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : nat, evenp n = true -> exists m : nat, n = 2 * <expression>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : nat, evenp n = true -> exists m : nat, n = 2 * <identifier>
-->
Theorem soundness_of_evenp : forall even : nat -> bool, forall n : nat, evenp n = true -> exists m : nat, n = 2 * m
where Theorem soundness_of_evenp (evenp : nat -> bool) : ... is syntactic sugar for Theorem soundness_of_evenp : forall evenp : nat -> bool, ....
(the beginning of) the abstract-syntax tree:
<toplevel-form>
|
<named-logical-statement>
/ | \
<qualifier> <identifier> <proposition>
| | \
Theorem completeness_of_evenp : <propo si tion>
| | \
forall <identifier> : <type>, <propo si tion>
| / \ \ \ \
even <type> -> <type> forall <identifier> : <type>, <pro position>
| | | | / \
nat bool n nat <proposition> -> <proposition>
| |
... ...
Alfrothul: Aha.
Bong-sun: Aha?
Alfrothul: I know, right?
Bong-sun: Er, I am not sure I do?
Alfrothul: These informal specifications last week...
Bong-sun: Oh. Right. They can be written as propositions in tCPA.
Pablito: You mean, for example, the specification of addition in Section Example of recursive definition: the addition function?
Given an integer j,
- base case: adding 0 to j yields j;
- induction step: given a number i' such that adding it to j yields ih (which is the induction hypothesis), adding S i' to j should yield S ih.
Alfrothul: Yes. We can write it as a proposition in tCPA:
Definition lambda_dropped_specification_of_the_addition_function (add : nat -> nat -> nat) : Prop :=
forall j : nat,
(add O j = j)
/\
(forall i' ih : nat,
add i' j = ih ->
add (S i') j = S ih).
Pablito: Harrumph.
Alfrothul (kindly): Right. We declare a name, “lambda_dropped_specification_of_the_addition_function”, of type (nat -> nat -> nat) -> nat -> Prop.
Pablito (with a small voice): OK?
Alfrothul: And we use tCPA’s syntactic sugar. We might as well have written:
Definition lambda_dropped_specification_of_the_addition_function : Prop :=
forall (add : nat -> nat -> nat)
(j : nat),
... /\ ....
Bong-sun: Or we could have written:
Definition lambda_dropped_specification_of_the_addition_function (add : nat -> nat -> nat) (j : nat) : Prop :=
... /\ ....
Pablito (with a firmer voice): OK, it’s all syntactic sugar, I get that: these three definitions are parsed into the same abstract-syntax tree. But you named it “lambda_dropped” why?
Alfrothul: Because the conjunction is quantified by j.
Bong-sun: Look, here is a lambda-lifted specification:
Definition lambda_lifted_specification_of_the_addition_function (add : nat -> nat -> nat) : Prop :=
(forall j : nat,
add O j = j)
/\
(forall j i' ih : nat,
add i' j = ih ->
add (S i') j = S ih).
Pablito: And this specification is lambda-lifted because each conjunct is quantified by j?
Bong-sun: Yup.
Dana: Question.
Alfrothul: Yes, Dana?
Dana: So now we have two specifications for the addition function?
Alfrothul: We do.
Dana (pointedly): Do they specify the same function?
Mimer: Yes, they are equivalent, and we will prove this equivalence with the following theorem:
Theorem equivalence_of_the_two_specifications_of_addition :
forall add : nat -> nat -> nat,
lambda_lifted_specification_of_addition add
<->
lambda_dropped_specification_of_addition add.
Anton: Now what.
Mimer: The above declares a theorem named equivalence_of_the_two_specifications_of_addition. This theorem says that for all given functions named add and that have type nat -> nat -> nat, the proposition lambda_lifted_specification_of_addition add and the proposition lambda_dropped_specification_of_addition add are equivalent, which is written with the infix notation <->.
Anton: OK...
Mimer: Equivalence means that if a given add satisfies the lambda-lifted specification, then it also satisfies the lambda-dropped specification, and that if it satisfies the lambda-dropped specification, then it also satisfies the lambda-lifted specification.
Halcyon: Equivalence is otherwise known as bi-implication.
Everybody looks at him.
Halcyon: What? I was paying attention during our common curriculum.
Mimer: Halcyon is absolutely right, and <-> is syntactic sugar for the conjunction of two implications.
Bong-sun: You mean that the theorem could be written as a conjunction:
Theorem equivalence_of_the_two_specifications_of_addition :
forall add : nat -> nat -> nat,
(lambda_lifted_specification_of_addition add -> lambda_dropped_specification_of_addition add)
/\
(lambda_dropped_specification_of_addition add -> lambda_lifted_specification_of_addition add).
Mimer: Yes I do. And well done, Bong-sun.
Dana: Next thing you are going to tell us is that we will not just test, but prove that our implementations satisfy the specifications.
Mimer: Indeed, Dana:
Theorem add_v1_satisfies_the_lambda_lifted_specification_of_addition :
lambda_lifted_specification_of_addition add_v1.
Pablito: So we will have to prove three theorems? One for add_v1, one for add_v2, and one for add_v3?
Mimer: Yes. And three, not six, since the two specifications of addition are equivalent:
Theorem add_v2_satisfies_the_lambda_lifted_specification_of_addition :
lambda_lifted_specification_of_addition add_v2.
Theorem add_v3_satisfies_the_lambda_lifted_specification_of_addition :
lambda_lifted_specification_of_addition add_v3.
Alfrothul: What about testing?
Mimer: Another theorem:
Theorem add_v1_passes_the_unit_tests :
test_add add_v1 = true.
Pablito: So we will have to prove three theorems? One for add_v1, one for add_v2, and one for add_v3?
Mimer: Not necessarily. We could just prove that the unit tests are sound with respect to the specification of addition.
Anton: Sound?
Mimer: Yes, sound. In words, if a function satisfies the specification of addition, then it passes the unit tests:
Theorem soundness_of_test_add :
forall add : nat -> nat -> nat,
lambda_lifted_specification_of_addition add ->
test_add add = true.
Loki: What about completeness?
Mimer: That we don’t have, since we cannot enumerate all existing natural numbers. Remember Dijkstra?
Alfrothul, Dana, Halcyon, Anton, Bong-sun, and Pablito (in one voice): Yes we do:
Testing only proves the presence of errors, not their absence.
Testing is incomplete in general.
Mimer: There you go.
Bong-sun: Let’s see. The lambda-dropped specification of addition reads:
Definition lambda_dropped_specification_of_addition (add : nat -> nat -> nat) : Prop :=
forall j : nat,
add 0 j = j
/\
forall i' : nat,
add (S i') j = S (add i' j).
Dana: Well, this specification is sound if for all functions that satisfy it, if applying this function to two numbers yields a third number, then this third number is the sum of these two numbers, using the resident + in Gallina.
Alfrothul: OK. Let’s say that the first two numbers are x and y and that the third number is z:
Theorem soundness_of_the_lambda_dropped_specification_of_addition :
forall add : nat -> nat -> nat,
lambda_dropped_specification_of_addition add ->
forall x y z : nat,
add x y = z ->
z = x + y.
Mimer: Yup.
Pablito: OK, I get it. Here is the lambda-lifted specification of addition:
Definition lambda_lifted_specification_of_addition (add : nat -> nat -> nat) : Prop :=
(forall j : nat,
add 0 j = j)
/\
(forall i' j : nat,
add (S i') j = S (add i' j)).
Bong-sun: Right. This specification is complete if for all functions that satisfy it, if adding two numbers yields a third number, then this third number is the result of applying this function to these two numbers.
Alfrothul: OK. Let’s say that the first two numbers are x and y and that the third number is z:
Theorem completeness_of_the_lambda_lifted_specification_of_addition :
forall add : nat -> nat -> nat,
lambda_lifted_specification_of_addition add ->
forall x y z : nat,
x + y = z ->
z = add x y.
Mimer: Yup.
Halcyon: So soundness and completeness are really the converse of each other.
Mimer: They are. And never mind the proof of these theorems for now.
Pablito: What about the soundness and completeness of our implementations from last week? For example:
Fixpoint add_v1 (i j : nat) : nat :=
match i with
O =>
j
| S i' =>
S (add_v1 i' j)
end.
Bong-sun: Let’s see. This implementation is sound with respect to the resident addition function in Gallina whenever if running it on two numbers yields a third number, then the third number is the result of adding these two numbers, look:
Theorem soundness_of_add_v1 :
forall x y z : nat,
add_v1 x y = z ->
z = x + y.
Pablito: I see. And it is complete with respect to the resident addition function in Gallina whenever if adding two numbers yields a third number, then this third number is the result of running our implementation on these two numbers:
Theorem completeness_of_add_v1 :
forall x y z : nat,
x + y = z ->
z = add_v1 x y.
Mimer: Yup.
Dana: So what about the theorem about add_v1 satisfying one of specification of addition:
Theorem add_v1_satisfies_the_lambda_lifted_specification_of_addition :
lambda_lifted_specification_of_addition add_v1.
Alfrothul: Ah, right. Is it related to soundness and completeness?
Mimer: Not explicitly, since soundness and completeness are about an implication, and there is no implication in this theorem.
Anton: Harumph.
Mimer: We shall revisit the notion of specification in Week 03.
Anton: And we remember how implication, conjunction, and disjunction associate how?
Alfrothul: We don’t. We use Check instead. For example:
Check (forall P : Prop, (P -> (P -> P)) * ((P -> P) -> P)).
Anton: OK. The *response* window reads:
forall P : Prop, (P -> P -> P) * ((P -> P) -> P) : Prop
Alfrothul: Yup. So implication associates to the right.
Dana: Just like the arrow type for functions in OCaml...
Bong-sun: ...and in Gallina.
Loki: Coincidence?
Mimer: Nope.
TCPA provides its user with many theorems, and we search for them with another toplevel form:
<toplevel-form> ::= Compute <expression>
| Check <expression>
| <definition>
| <named-logical-statement>
| Search <pattern>
<pattern> ::= _
| <pattern> -> <pattern>
| <pattern> /\ <pattern>
| <pattern> \/ <pattern>
| (<pattern>)
| <pattern-expression>
<pattern-expression> ::= _
| <pattern-expression> = <pattern-expression>
| <pattern-expression> + <pattern-expression>
| <pattern-expression> - <pattern-expression>
| ...
For example, let us query the libraries with the pattern of the associativity of +:
Search (_ + (_ + _) = _).
Among several other answers in the *response* window, here is the relevant one:
Nat.add_assoc: forall n m p : nat, n + (m + p) = n + m + p
Likewise, we can query the libraries with the pattern of the commutativity of +:
Search (_ + _ = _ + _).
Among a number of other answers (which include Nat.add_assoc), here is the relevant one:
Nat.add_comm: forall n m : nat, n + m = m + n
The statement and proof of these theorems can be found in the library Nat.
For another example, let us query the libraries with the pattern of 0 being right-neutral with respect to +:
Search (_ + 0 = _).
The *response* window contains one answer:
Nat.add_0_r: forall n : nat, n + 0 = n
TCPA’s naming conventions being what they are, chances are that Nat.add_0_l is the converse lemma, which we can check with:
Check Nat.add_0_l.
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 instanciate 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?
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_warmup :
forall x y : nat,
(x + y) * (x + y) = x * x + x * y + x * y + y * y.
Proposition binomial_expansion_2 :
forall x y : nat,
(x + y) * (x + y) = x * x + 2 * (x * y) + y * y.
Hint: search for (_ * (_ + _) = _).
N.B.: Make sure to supply all the arguments to all the lemmas that you apply.
Added the precision in the statement of Exercise 05 [30 Jan 2024]
Fixed a typo in the specifications of the addition function, thanks to Wong Kok Rui’s eagle eye in class [26 Jan 2024]
Created [25 Jan 2024]