The goal of this lecture note is to make the transition from an informal statement on pen and paper to a formal one in tCPA (which is short for “the Coq Proof Assistant”).
The learning goals of this lecture note are as follows:
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 :
forall evenp : nat -> bool,
forall n : nat,
evenp n = true ->
exists m : nat,
n = 2 * m.
(In words: Any given evenp predicate is sound with respect to the mathematical definition of evenness whenever applying this predicate to a natural number yields true implies that this natural number is even.)
And likewise for its completeness:
Theorem completeness_of_evenp :
forall evenp : nat -> bool,
forall n : nat,
(exists m : nat,
n = 2 * m) ->
evenp n = true.
(In words: Any given evenp predicate is complete with respect to the mathematical definition of evenness whenever given an even number, applying this predicate to this even 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 evenp : <type>, <proposition>
-->
Theorem soundness_of_evenp : forall evenp : <type> -> <type>, <proposition>
-->
Theorem soundness_of_evenp : forall evenp : nat -> <type>, <proposition>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, <proposition>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall <identifier> : <type>, <proposition>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : <type>, <proposition>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : nat, <proposition>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : nat, <proposition> -> <proposition>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : nat, <expression> = <expression> -> <proposition>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : nat, <expression> <expression> = <expression> -> <proposition>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : nat, <identifier> <expression> = <expression> -> <proposition>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : nat, evenp <expression> = <expression> -> <proposition>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : nat, evenp <identifier> = <expression> -> <proposition>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : nat, evenp n = <expression> -> <proposition>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : nat, evenp n = <boolean> -> <proposition>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : nat, evenp n = true -> <proposition>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : nat, evenp n = true -> exists <identifier> : <type>, <proposition>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : nat, evenp n = true -> exists m : <type>, <proposition>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : nat, evenp n = true -> exists m : nat, <proposition>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : nat, evenp n = true -> exists m : nat, <expression> = <expression>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : nat, evenp n = true -> exists m : nat, <identifier> = <expression>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : nat, evenp n = true -> exists m : nat, n = <expression>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : nat, evenp n = true -> exists m : nat, n = <expression> * <expression>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : nat, evenp n = true -> exists m : nat, n = <natural-number> * <expression>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : nat, evenp n = true -> exists m : nat, n = 2 * <expression>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : nat, evenp n = true -> exists m : nat, n = 2 * <identifier>
-->
Theorem soundness_of_evenp : forall evenp : nat -> bool, forall n : nat, evenp n = true -> exists m : nat, n = 2 * m
(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>
| / \ \ \ \
evenp <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 Peano numbers?
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 : Prop :=
forall add : nat -> nat -> nat,
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 Prop.
Pablito (with a small voice): OK?
Alfrothul: Or we could use tCPA’s syntactic sugar. We might as well have written:
Definition lambda_dropped_specification_of_the_addition_function (add : nat -> nat -> nat) : Prop :=
forall (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. There are two local occurrences of forall j : nat,.
Pablito: Whereas the other specification is lambda-dropped because both conjuncts are quantified?
Bong-sun: Yup. There is one global occurrence of forall j : nat,.
Pablito: OK, thanks.
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_alt :
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 if a function satisfies the specification of addition, then it passes the unit tests:
Theorem correctness_of_test_add :
forall add : nat -> nat -> nat,
lambda_lifted_specification_of_addition add ->
test_add add = true.
Dana: In other words, the specification is sound with respect to the unit tests?
Mimer: Yes. In words, for any given add function, the specification of addition is sound with respect to the tests whenever add satisfying the specification of addition implies that it passes the unit tests.
Loki: What about completeness?
Mimer: Let’s see. For any given add function, the specification of addition would be complete with respect to the tests whenever add passing the unit tests implies that it satisfies the specification of addition. And that we do not have, since we cannot test 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.
Pablito: Hmm...
Bong-sun: Yes, Pablito?
Pablito: What about the soundness and the completeness of the tests with respect to the specification?
Bong-sun: I think we can figure this one by ourselves. Let me see... The tests would be sound with respect to the specification whenever for any given add function, if this function passes the tests, then it satisfies the specification.
Pablito: OK, I think I am getting it. And the tests would be complete with respect to the specification whenever for any given add function, if this function satisfies the specification, then it passes the tests.
Bong-sun: Right, that’s the definition.
Anton: Can we be concrete here for a second?
Bong-sun: Er, sure.
Anton: If there is a bug in our unit tests, shouldn’t it mean that they are unsound?
Alfrothul: Well, that means that they are incorrect.
Bong-sun: Right. They are incorrect either because they accept an incorrect program or because they reject a correct program.
Anton: Er, OK. Yes.
Dana: An incorrect program doesn’t satisfy the specification of the function this program is supposed to implement.
Anton: Yes.
Dana: Let us say that the incorrect tests accept this incorrect program.
Anton: OK. Then what?
Dana: Well, it means that this program passing the unit tests does not imply that it satisfies the specification. So the specification is not complete with respect to the tests.
Alfrothul: And the tests are not sound with respect to the specification.
Anton: OK. What about the other possibility, i.e., the tests reject a correct program?
Dana: Do you agree that a program is correct if and only if it satisfies the specification?
Anton: Yes.
Dana: So the situation is that a program satisfying the specification does not imply that it passes the tests.
Anton: Yes.
Dana: Then the specification is unsound with respect to the buggy tests and the buggy tests are incomplete with respect to the specification.
Anton: OK, I guess. At least I see the symmetry.
Bong-sun: And you, Pablito?
Pablito: OK too. At least I see the points of view.
Mimer: The issue is that we use tests to disprove that a program satisfies a specification:
not (test_add buggy_add) -> not (specification_of_addition buggy_add)
Pablito: That’s true – if a program does not pass the tests, it is not correct.
Mimer: And likewise, here is Dijkstra’s point in logical form:
not (test_add add -> specification_of_addition add)
Anton: That’s true too – even though a program passes the tests, it may not be correct.
Alfrothul: Right. A program passing the tests does not imply that this program is correct.
Mimer: As long as you see this clearly, you are good to go.
Pablito: But what about soundness and completeness?
Mimer: When we state the soundness of a function with respect to something that relates an input and an output, we state that if applying the function to X yields Y, then X and Y are in the relation. And when we state the completeness of a function with respect to something that relates an input and an output, we state that if X and and Y are in the relation, then applying the function to X yields Y. In other words, for all X and Y,
For the primality predicate in Week 01, the relation is:
{(X, Y) | Y = true implies that X is only divisible by 1 and by itself}
For the evenness predicate, the relation is:
{(X, Y) | Y = true implies that there exists a nat Z such that X = 2 * Z}
Pablito: Ah, OK. So our Gallina function evenp is sound with respect to this relation whenever if it maps a given number n to true, then (n, true) is in the relation and so the given number is even.
Anton: And conversely, evenp is complete with respect to this relation whenever if (n, true) is in the relation, i.e., n is even, then evenp maps n to true.
Bong-sun: And to implement addition ourselves, the relation is:
{((X, Y), Z) | Z = X + Y}
Dana: And our Gallina function add is sound with respect to this relation whenever if it maps two given numbers n1 and n2 to the number n3, then ((n1, n2), n3) is in the relation and so n3 denotes the result of adding n1 and n2.
Alfrothul: And our Gallina function add is complete with respect to this relation whenever if ((n1, n2), n3) is in the relation, i.e., n3 denotes the result of adding n1 and n2, then add maps n1 and n2 to n3.
Mimer: You guys are on top of things.
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: Harrumph.
Mimer: We shall revisit the notion of specification in Week 03.
Bong-sun: These exercises are not complicated <pause> complicated.Dana: But they sharpen our minds.Bong-sun: They do, don’t they?
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.
Anton: Mind revisiting the food for thought from last week?
Alfrothul: In the light of the present chapter, you mean?
Anton: Yes.
Alfrothul: Go ahead.
Anton: Let’s start with foo:
Fixpoint foo (n : nat) : nat :=
match n with
O =>
O
| S n' =>
S (S (foo n'))
end.
Alfrothul: Right. Which mathematical function does it compute?
Anton: How about we apply the scientific method? We successively apply foo to a series of numbers, and we try to detect a pattern in the series of results. And then we formulate a hypothesis, which we test with another series of numbers.
Alfrothul: Sure, let’s do that:
Compute (foo 0, foo 1, foo 2, foo 3, foo 4).
Pablito (helpful): The *response* window reads:
= (0, 2, 4, 6, 8)
: nat * nat * nat * nat * nat
Anton: Which suggests that foo multiplies its argument by 2:
Definition testing_the_hypothesis_about_foo (x : nat) : bool :=
let y := foo x
in Nat.eqb y (2 * x).
Anton: And now we can test this hypothesis with more numbers:
Compute ((testing_the_hypothesis_about_foo 0)
&&
(testing_the_hypothesis_about_foo 1)
&&
(testing_the_hypothesis_about_foo 2)
&&
(testing_the_hypothesis_about_foo 3)
&&
(testing_the_hypothesis_about_foo 4)
&&
(testing_the_hypothesis_about_foo 5)
&&
(testing_the_hypothesis_about_foo 6)
&&
(testing_the_hypothesis_about_foo 7)).
Pablito (helpful): The *response* window reads:
= true
: bool
Alfrothul: So the hypothesis is not invalidated by the new tests.
Anton: Right. But since testing is not proving...
Alfrothul: ...in the light of the present chapter, ...
Anton: ...we can state a theorem.
Alfrothul: So we quantify x and y universally...
Anton: ...and then we say that if applying foo too x yields y ...
Alfrothul: ...then y is twice x, an implication:
Theorem about_foo :
forall x y : nat,
foo x = y ->
y = 2 * x.
Anton: Which we admit for now, using the keyword Admitted.
Go through an analogue of the postlude just above with bar.
Tuned the end of the interlude about formalizing informal specifications and added the continuation of this interlude following a perceptive email by Liew Zhao Wei [04 Feb 2025]
Changed the name of the present file and of the accompanying .v file [31 Jan 2025]
Added the postlude about the food for thought in Week 01 and two subsequent exercises [26 Jan 2025]
Adjusted the title of this chapter and of the section about the tCPA libraries [24 Jan 2025]
Created [24 Jan 2025]