See also
Warning
It is counter-productive to look for things online by default: doing so will keep you insecure in your knowledge, forever depending on others. Also, most of the time, online things
and then what.
The goal of this lecture note is to establish a comfort zone regarding functional programming in Gallina, tCPA’s resident programming language.
Edit the accompanying .v file to get started:
Under the assumption that (setq proof-three-window-mode-policy 'hybrid) is lying somewhere in one’s .emacs file , one should be editing this Gallina file with 3 windows:
We can split the left window any way we like (C-x 2 for example, to have a multiple view of our .v file, and then C-x 0 to eliminate the current window; or C-x 1 to edit our file with the full screen). At any point, typing C-c C-l brings us back to the canonical three windows.
Warning
Occasionally, Proof General might appear as it is confused. Then one should go back to the theorem or lemma one is proving, and continue from there.
One interacts with tCPA through a series of toplevel forms in the file that is edited in the left window. Each of these toplevel forms is ended with a period:
<toplevel-forms> ::= {<toplevel-form>.}*
<toplevel-form> ::= Compute <expression>
| Check <expression>
| <definition>
<type> ::= nat | bool | <type> * <type> | <type> -> <type> | ...
<definition> ::= Definition <identifier> { : <type> }? := <expression>
| Inductive <identifier> { : <type> }? := ...
<expression> ::= <natural-number>
| <boolean>
| <identifier>
| <expression> <expression>
| fun <identifier> { : <type> }? => <expression>
| (<expression>, <expression>)
| let <identifier> { : <type> }? := <expression> in <expression>
| ...
<natural-number> ::= 0 | 1 | 2 | ...
<boolean> ::= true | false
Like OCaml, Gallina provides syntactic sugar in the form of infix notations for arithmetic operations. So for example,
Pablito: Syntactic sugar?Bong-sun: It means “short-hand notation”.Dana: For example, e1 + e2 and plus e1 e2 are parsed into the same abstract-syntax tree.Alfrothul: So they really mean the same.Halcyon: The term is due to Peter Landin.
Check is given an expression and is used at the toplevel to ask tCPA about the type of this expression.
For example, let us issue the command:
Check true.
The effect of this command is that the *response* window now contains:
true
: bool
This content manifests that true has type bool.
Here is the declaration of bool in tCPA’s initial library. It is the type of booleans, a sum type:
Inductive bool : Type :=
true : bool
| false : bool
The constructors are true and false, which are nullary (i.e., take no arguments).
As in OCaml, in the declaration of an inductive data type, the first constructor may be preceded or not by |:
Inductive bool : Type :=
| true : bool
| false : bool
Likewise, one can check that 42 has type nat using the command Check 42.
Anton: Actually, plus is an alias for Nat.add.Pablito: How do you know?Anton: I evaluated Check plus.Pablito: Ah.Anton (helpfully): So addition is implemented with a function add.Pablito: And this function add is defined in the library Nat, I get it.Halcyon: And likewise, minus is an alias for Nat.sub.
The Check command comes handy when we need to exhibit an expression that has a given type. For example, we used it just above to verify that true has type bool.
Here are more examples of this use:
Say we are asked to exhibit an expression that has type nat * bool. We know that pairs are constructed with two matching parentheses with an infix comma – i.e., (..., ...), so all we need is two expressions: one of type nat – e.g., 1, and one of type bool – e.g., false. So our putative expression is (1, false):
Check (1, false).
The *response* window now contains:
(1, false)
: nat * bool
This content manifests that (1, false) has type nat * bool, and so this expression can be one that we can exhibit.
Say we are asked to exhibit an expression that has type nat -> nat. We know that functions are constructed using the fun keyword – i.e., as something like fun (x : ...) => .... Since the domain of nat -> nat is nat, the type of x has to be nat, so our putative expression can be fun (x : nat) => .... And now we need to replace ... with an expression that has type nat. This expression could be a Peano number – e.g., 2, or a name that has type nat – e.g., x, or the result of a computation that has type nat – e.g., S x. Either way, that gives us a putative expression that we can give to the Check command:
Check (fun (x : nat) => S x).
The *response* window now contains:
fun x : nat => S x
: nat -> nat
This content manifests that fun x : nat => S x has type nat -> nat, and so this expression can be one that we can exhibit.
Say we are asked to exhibit an expression that has type nat -> bool -> nat * bool.
We know that functions are constructed using the fun keyword and that the domain of nat -> bool -> nat * bool is nat. So the type of the formal parameter has to be nat, and our putative expression can start with fun (n : nat) => ....
Now instead of ..., we need to exhibit an expression of type bool -> nat * bool. Again, we know that functions are constructed using the fun keyword and that the domain of bool -> nat * bool is bool. So the type of the formal parameter has to be bool, and our putative expression can start with fun (b : bool) => ....
Now instead of ..., we need to exhibit an expression of type nat * bool. We know that pairs are constructed with two matching parentheses with an infix comma, so all we need is two expressions: one of type nat – e.g., n since it was just declared in fun (n : nat) => ... just above, and one of type bool – e.g., b since it was just declared in fun (b : bool) => ... also just above. So our putative expression is (n, b).
All in all, we posit that fun (n : nat) => fun (b : bool) => (n, b) has type nat -> bool -> nat * bool and we verify this claim using the Check command:
Check (fun (n : nat) => fun (b : bool) => (n, b)).
The *response* window now contains:
fun (n : nat) (b : bool) => (n, b)
: nat -> bool -> nat * bool
This content manifests that our putative expression has the required type, and so this expression can be one that we can exhibit.
The Inductive keyword is used to declare a new type and to give it a name, as in the bool example just above. Likewise, the Definition keyword is use to name the result of evaluating an expression.
Names and their denotation are held in “the environment”. We say that a name is bound to its denotation in the environment.
Initially, the environment is empty. Each successve declaration extends the environment with a new binding of a name to its denotation.
In Gallina, names cannot be re-declared.
Compute is given an expression and is used at the toplevel to ask tCPA to compute this expression.
For example, let us issue the command:
Compute (123 + 321).
The effect of this command is that the *response* window now contains:
= 444
: nat
Likewise, one can compute 6 * 9, which actually yields 54 in base 10.
Halcyon (wondering): What is this? A hitch-hiker guide?Bong-sun (facepalming): ...
Here is the declaration of nat in tCPA’s initial library. It is the type of natural numbers, a recursive sum type since natural numbers are represented as Peano numbers, i.e., in base 1:
Inductive nat : Type :=
O : nat
| S : nat -> nat
The constructors are O (which is nullary, i.e., take no arguments) and S (which is unary, i.e., take one argument). So:
By default, natural numbers are read (desugared) and printed (sugared) as the ordinary arabic numbers in base 10. So for example, 0 (the digit) and O (the letter) can be used interchangeably.
Food for thought:
Evaluate Check 0. and Check O..
How do the results of evaluation compare? Why?
Evaluate Check 1., Check (S 0)., and Check (S O)..
How do the results of evaluation compare? Why?
Evaluate Check 2., Check (S (S 0))., and Check (S (S O))..
How do the results of evaluation compare? Why?
There is a single answer to all these questions: The argument of Check is parsed into the same abstract syntax tree, and what is then printed is first unparsed into ordinary arabic numbers in base 10.
Alfrothul: So the grammar above can be made more precise.
Anton: Right. Instead of writing:
<natural-number> ::= 0 | 1 | 2 | ...
Alfrothul: ...we can write:
<natural-number> ::= O | S <natural-number>
Anton: Right. A self-referential but finite description of arbitrary large data instead of arbitrarily many grammar rules.
Inductive data are decomposed with a match expression that enumerates all the possible constructors and their arguments:
match <expression> with
<constructor> {<identifier>}* => <expression>
| ...
| <constructor> {<identifier>}* => <expression>
end
Unlike in OCaml, match expressions are terminated with end.
And as in OCaml, in a match expression, the first constructor may be preceded or not by |:
match <expression> with
| <constructor> {<identifier>}* => <expression>
| ...
| <constructor> {<identifier>}* => <expression>
end
So for example, we can define a predicate (i.e., a function that returns a boolean) that tests whether a given boolean is true or not:
Definition truep_v0 : bool -> bool :=
fun b =>
match b with
true =>
true
| false =>
false
end.
(Adding a “p” at the end of the name of a predicate is known as “the p convention” and dates back to the Lisp programming language. In Gallina, a “b convention” is used; for example, Nat.eqb and Bool.eqb are equality predicates that return a boolean value and negb is the negation function for booleans.)
As in OCaml, we can declare the formal parameters of a named function right after its name, a convenient syntactic sugar:
Definition truep_v1 (b : bool) : bool :=
match b with
true =>
true
| false =>
false
end.
Anton: This truep function...
Alfrothul: ...suspiciously looks like the identity function.
Halcyon (cleverly): True that.
Alfrothul: And that means that the falsep function...
Pablito (helpfully): Here it is, here it is:
Definition falsep (b : bool) : bool :=
match b with
true =>
false
| false =>
true
end.
Anton: ...looks like the negation function.
Halcyon (enjoying himself): Which is not false.
Dana: Er, guys, could we move on?
Pablito: Er, before we do that, can you clarify what happens when the function denoted by falsep is applied to a boolean?
Dana: Certainly. As you correctly say, evaluating the declaration above has the effect of extending the current environment...
Halcyon: Er, environment?
Dana: The environment holds together the names and what these names denote.
Halcyon: OK, thanks.
Dana: So as Pablito correctly said, evaluating the declaration above has the effect of extending the current environment with a new name – falsep – that denotes the function that is the result of evaluating fun b => match b with true => false | false => true end.
Halcyon: OK.
Dana: Let me spell out what happens when we evaluate the expression falsep true, for example.
Pablito: Please do.
Dana: This expression is an application, and evaluating an application e0 e1 in an environment reduces to applying the result of evaluating e0 in this environment to the result of evaluating e1 in this environment.
Loki (coughing in his hand): Call by value.
Dana: Thanks, Loki. Yes, call by value: The argument is evaluated before the function is applied. We could use call by name, i.e., delay the evaluation of the argument until it is needed, but it doesn’t matter here, since Gallina is a pure and total language and so we cannot distinguish whether it is implemented using call by value or using call by name.
Pablito: Let’s say that I take that on faith for now. Can we move on?
Dana: Sure, let’s. Here, we evaluate falsep true in an environment where falsep denotes a function. Evaluating falsep yields this function, evaluating true yields true, and so evaluating falsep true reduces to applying this function to true. OK so far?
Pablito: OK so far.
Dana: Applying the function that is the result of evaluating fun b => match b with true => false | false => true end to true reduces to evaluating match b with true => false | false => true end in an environment where b denotes true. OK?
Pablito: match b with true => false | false => true end is the body of falsep, right?
Dana: Right.
Pablito: OK, please proceed.
Dana: To evaluate match b with true => false | false => true end in an environment where b denotes true, we first evaluate b in this environment. Since b denotes true, the result of evaluating b is true. So evaluating match b with true => false | false => true end reduces to evaluating false, which is the expression the true clause. OK?
Pablito: You mean that if e evaluates to a value that was constructed with, e.g., the constructor C, then evaluating match e with ... | C => e' | ... end would reduce to evaluating e'?
Dana: Yes. Here, C is nullary.
Alfrothul: And if e evaluates to a value that was constructed with, e.g., a constructor X that takes two arguments, then evaluating match e with ... | X a b => e' | ... end would reduce to evaluating e' in an extension of the current environment where a denotes the first argument of X and where b denotes the second argument of X.
Pablito: OK.
Dana: And we are done here, since evaluating false yields false. Overall, evaluating falsep true in an environment where falsep is defined yields false.
Pablito: Thank you.
Mimer: Consider a program that implements this evaluation mechanism. What is this program?
Pablito: An interpreter?
Mimer: Yup. And you guys will implement interpreters later on.
So for another example, we can define a function that tests whether a given natural number is 0 or not:
Definition zerop_v1 (n : nat) : bool :=
match n with
| O =>
true
| S n' =>
false
end.
Since S is a unary constructor, its argument is declared in the S clause.
Here, in the S clause, n' is not used, so as in OCaml, we can not declare it and put an underscore instead:
Definition zerop_v2 (n : nat) : bool :=
match n with
O =>
true
| S _ =>
false
end.
Note how in the match-expression, the clauses are in the same order as in the type declaration of nat. Using the same ordering is considered good style.
Inductive data are processed by recursive functions, which are declared using Fixpoint:
<definition> ::= Fixpoint <identifier> {({<identifier>}+ { : <type> }?)}+ := <expression>
In Gallina, the only possible recursive functions are structural, i.e., they are defined over an inductive data type and they follow its structure. Therefore all Gallina programs terminate.
For example, let us revisit the nat type:
Inductive nat : Type :=
O : nat
| S : nat -> nat
Here is its associated structural-induction principle (a.k.a. mathematical induction, since Peano numbers represent natural numbers, including 0):
P O forall n' : nat, P n' -> P (S n')
----------------------------------------
forall n : nat, P n
In this inference rule, P O is the base case and forall n' : nat, P n' -> P (S n') is the induction step. And in this induction step, P n' is the induction hypothesis.
Here is the prototypical skeleton of a recursive function over nat:
Fixpoint prototypical_skeleton_nat (n : nat) : ... :=
match n with
O =>
...
| S n' =>
... (prototypical_skeleton_nat n') ...
end.
In this skeleton, the first clause (n = O) implements the base case and the second clause (n = S n') implements the induction step. And this second clause, the recursive call implements the induction hypothesis.
Having only structurally recursive functions, we shall uniformly reason about them by structural induction.
The identity function over natural numbers is very simple to declare recursively:
Fixpoint identity_nat (n : nat) : nat :=
match n with
O =>
O
| S n' =>
S (identity_nat n')
end.
This declaration is recursive because the name identity_nat is used on the right-hand side of the declaration. The expression match n with ... end is said to be the “body” of identity_nat. Henceforth the name identity_nat denotes a recursive function of type nat -> nat, as can be verified by typing:
Check identity_nat.
For example, say that we apply the function denoted by identity_nat to 3, i.e., to S (S (S O)). Here is what happens, in complete detail, indenting these details to account for the recursive calls:
identity_nat (S (S (S O))) is evaluated in an environment where identity_nat denotes the recursive function; evaluating the application of this recursive function to S (S (S O)) reduces to evaluating the body of identity_nat in an environment where n denotes S (S (S O)) and identity_nat denotes the recursive function;
to evaluate match n with ... end, n is first evaluated; the result is 3, which is represented as S (S (S O)), which is S n', where n' denotes S (S O); the S clause is selected, and evaluating match n with ... end reduces to evaluating S (identity_nat n') in an environment where n' denotes S (S O) and identity_nat denotes the recursive function; to evaluate S (identity_nat n'), which is the application of the S constructor to identity_nat n', we first evaluate identity_nat n', which is the application of the name identity_nat to the name n';
identity_nat denotes the recursive function and n' denotes S (S O); evaluating the application of this recursive function to S (S O) reduces to evaluating the body of identity_nat in an environment where n denotes S (S O) and identity_nat denotes the recursive function;
to evaluate match n with ... end, n is first evaluated; the result is 2, which is represented as S (S O), which is S n', where n' denotes S O; the S clause is selected, and evaluating match n with ... end reduces to evaluating S (identity_nat n') in an environment where n' denotes S O and identity_nat denotes the recursive function; to evaluate S (identity_nat n'), which is the application of the S constructor to identity_nat n', we first evaluate identity_nat n', which is the application of the name identity_nat to the name n';
identity_nat denotes the recursive function and n' denotes S O; evaluating the application of this recursive function to S O reduces to evaluating the body of identity_nat in an environment where n denotes S O and identity_nat denotes the recursive function;
to evaluate match n with ... end, n is first evaluated; the result is 1, which is represented as S O, which is S n', where n' denotes O; the S clause is selected, and evaluating match n with ... end reduces to evaluating S (identity_nat n') in an environment where n' denotes O and identity_nat denotes the recursive function;
to evaluate S (identity_nat n'), which is the application of the S constructor to identity_nat n', we first evaluate identity_nat n', which is the application of the name identity_nat to the name n';
identity_nat denotes the recursive function and n' denotes O; evaluating the application of this recursive function to O reduces to evaluating the body of identity_nat in an environment where n denotes O and identity_nat denotes the recursive function;
to evaluate match n with ... end, n is first evaluated; the result is 0, which is represented as O; the O clause is selected, and evaluating match n with ... end reduces to evaluating O, which yields 0;
we then apply the denotation of the S constructor to 0, which yields 1;
we then apply the denotation of the S constructor to 1, which yields 2;
we then apply the denotation of the S constructor to 2, which yields 3.
So all in all, evaluating identity_nat (S (S (S O))) in an environment where identity_nat denotes the recursive function yields 3.
Which mathematical functions do the following Gallina functions compute?
foo:
Fixpoint foo (n : nat) : nat :=
match n with
O =>
O
| S n' =>
S (S (foo n'))
end.
Here is how to determine which mathematical function is computed by foo.
Let us first apply the function denoted by foo to 0, 1, 2, etc. The successive results are 0, 2, 4, etc., suggesting that foo multiplies its argument by 2: for all a and b of type nat, if applying foo to a yields b then b = 2 * a.
Let us implement a function that tests this conjecture:
Definition testing_the_conjecture_about_foo (a : nat) : bool :=
let b := foo a in
Nat.eqb b (2 * a).
We can verify that applying the function denoted by testing_the_conjecture_about_foo to 0, 1, 2, etc. always yields true.
N.B.: Soon, we will prove this conjecture rather than test it.
bar:
Fixpoint bar (n : nat) : nat :=
match n with
O =>
O
| S n' =>
S (S (S (bar n')))
end.
Here is how to determine which mathematical function is computed by bar.
Let us first apply the function denoted by bar to 0, 1, 2, etc. The successive results are 0, 3, 6, etc., suggesting that bar multiplies its argument by 3: for all a and b of type nat, if applying foo to a yields b then b = 3 * a.
Let us implement a function that tests this conjecture:
Definition testing_the_conjecture_about_bar (a : nat) : bool :=
let b := foo a in
Nat.eqb b (3 * a).
We can verify that applying the function denoted by testing_the_conjecture_about_bar to 0, 1, 2, etc. always yields true.
N.B.: Soon, we will prove this conjecture rather than test it.
baz_x and baz_y:
Fixpoint baz_aux (n : nat) (b : bool) : nat :=
match n with
O =>
O
| S n' =>
if b
then baz_aux n' (negb b)
else S (baz_aux n' (negb b))
end.
Definition baz_x (n : nat) : nat :=
baz_aux n true.
Definition baz_y (n : nat) : nat :=
baz_aux n false.
Here is how to determine which mathematical function is computed by baz_x.
Let us first apply the function denoted by baz_x to 0, 1, 2, etc., all the way to 9. The successive results are 0, 0, 1, 1, 2, 2, etc., suggesting that bar_x divides its argument by 2: for all a and b of type nat, if applying baz_x to 2 * a yields b then b = a and if applying baz_x to 2 * a + 1 yields b then b = a.
Let us implement a function that tests this conjecture:
Definition testing_the_conjecture_about_baz_x (a : nat) : bool :=
(let b_even := baz_x (2 * a) in Nat.eqb b_even a)
&&
(let b_odd := baz_x (S (2 * a)) in Nat.eqb b_odd a).
We can verify that applying the function denoted by testing_the_conjecture_about_baz_x to 0, 1, 2, etc. always yields true.
N.B.: Soon, we will prove this conjecture rather than test it.
Here is how to determine which mathematical function is computed by baz_y.
Then let us apply the function denoted by baz_y to 0, 1, 2, etc., all the way to 9. The successive results are 0, 1, 1, 2, 2, 3, etc., suggesting that bar_y also divides its argument by 2: for all a and b of type nat, if applying baz_y to 2 * a yields b then b = a and if applying baz_x to 2 * a + 1 yields b then b = a + 1.
Let us implement a function that tests this conjecture:
Definition testing_the_conjecture_about_baz_y (a : nat) : bool :=
(let b_even := baz_y (2 * a) in Nat.eqb b_even a)
&&
(let b_odd := baz_y (S (2 * a)) in Nat.eqb b_odd (S a)).
We can verify that applying the function denoted by testing_the_conjecture_about_baz_y to 0, 1, 2, etc. always yields true.
N.B.: Soon, we will prove this conjecture rather than test it.
For example, let us consider the addition function over natural numbers, based on the following inductive specification of addition. Given an integer j,
Here is a direct implementation of this inductive specification. This implementation is recursive and the recursive call implements the induction hypothesis:
Definition add_v1 (n j : nat) : nat :=
let fix visit i :=
match i with
O =>
j
| S i' =>
S (visit i')
end
in visit n.
The declaration of add_v1 is lambda dropped in that it uses a lexical block where visit is declared. This lexical block is used to declare visit. This local declaration is scope sensitive because the definiens uses j, which is declared outside this block.
The declaration of add_v1 is not recursive because it contains no call to add_v1. The local declaration of visit is recursive because of the recursive call to visit in the conditional branch for positive numbers. So add_v1 is declared with Definition and visit is declared with let fix.
Alternatively, we can implement the addition function with the following lambda-lifted recursive function:
Fixpoint add_v2 (i j : nat) : nat :=
match i with
O =>
j
| S i' =>
S (add_v2 i' j)
end.
The declaration of add_v2 is recursive because of the recursive call to add_v2 in the conditional branch for positive numbers. So add_v2 is declared with Fixpoint.
The declaration of add_v2 is lambda lifted in that it is a toplevel recursive declaration. This declaration is scope insensitive in that all the variables it uses are declared as their formal parameters.
In OCaml, it is a good idea to “lambda-drop” one’s programs, i.e., to define them with lexical blocks, as in the declaration of add_v1 above, so that the declaration of visit is local (i.e., invisible outside the declaration of add_v1). In Gallina, it is a better idea to “lambda-lift” one’s programs, i.e., only have toplevel recursive functions, as in the declaration of add_v2 above, so that we can refer to their name when reasoning about them.
We say that add_v2 is the “lambda-lifted” counterpart of add_v1 and conversely that add_v1 is the “lambda-dropped” counterpart of add_v2.
Here is another implementation of the addition function:
Fixpoint add_v3 (i j : nat) : nat :=
match i with
O =>
j
| S i' =>
add_v3 i' (S j)
end.
This declaration is recursive because of the recursive call to add_v3. It is lambda lifted in that it is a toplevel recursive declaration. It is also tail recursive because the recursive call to add_v3 is a tail call.
The .v file that accompanies the present lecture note also features a unit-test function for addition.
Bong-sun: Question.
Mimer: Yes, Bong-sun?
Bong-sun: How do we know that these three declarations implement the inductive specification of addition?
Dana: Right. And how do we know these declarations are equivalent?
Mimer: Excellent questions! In previous courses, these are things that we tested. And here, we are going to prove them. Stay tuned.
Go through the standard functions over natural numbers in the accompanying .v file and program them in Gallina, including unit tests: addition, multiplication, exponentiation, factorial function, Fibonacci function, and evenness / oddness predicates.
The goal of this exercise is to become familiar with the notation and use of Gallina, so the more declarations you write, the better.
Things to keep in mind:
Bong-sun: Let’s see. Multiplication is iterated addition, right?
Pablito: Iterated addition?
Bong-sun: You know, three times four is four plus four plus four, where we add four three times.
Pablito: True that.
Alfrothul: Dibs on the unit-test function:
Definition test_mult (candidate: nat -> nat -> nat) : bool :=
true
&&
(Nat.eqb (candidate 0 0) 0)
&&
(Nat.eqb (candidate 0 10) 0)
&&
(Nat.eqb (candidate 10 0) 0)
&&
(Nat.eqb (candidate 1 10) 10)
&&
(Nat.eqb (candidate 10 1) 10)
&&
(Nat.eqb (candidate 2 3) 6)
(* etc. *)
.
Anton: OK, an intuitive sample of numbers.
Dana: The first test is redundant, but then emacs uniformly indents all the other tests.
Bong-sun: Let me also add the intuitive characterization:
Definition test_mult (candidate: nat -> nat -> nat) : bool :=
...
&&
(Nat.eqb (candidate 3 4) (4 + 4 + 4))
(* etc. *)
.
Alfrothul: Let me add a test for commutativity:
Definition test_mult (candidate: nat -> nat -> nat) : bool :=
...
&&
(let x := 3
in let y := 4
in Nat.eqb (candidate x y) (candidate y x))
(* etc. *)
.
Anton: And another for associativity:
Definition test_mult (candidate: nat -> nat -> nat) : bool :=
...
&&
(let x := 3 in
let y := 4 in
let z := 5 in
Nat.eqb (candidate x (candidate y z))
(candidate (candidate x y) z))
(* etc. *)
.
Halcyon: Er... I notice that you guys do not write nested let-expressions consistently?
Alfrothul: Right. I prefer to vertically align let and in so that the nested lexical blocks appear more clearly, look:
let x := 3
in +------------+
| let y := 4 |
| in +-----+ |
| | ... | |
| +-----+ |
+------------+
Anton: And I prefer to vertically align the keyword let:
let x := 3 in
let y := 4 in
let z := 5 in
...
Anton: Most of the time it doesn’t matter, and that is the case here since the definiens 4 does not refer to x and since the definiens 5 does not refer to x nor y. In OCaml, I would write:
let x = 3 and y = 4 and z = 5 in
...
Alfrothul: Whereas I would write:
let x = 3 and y = 4 and z = 5
in ...
Alfrothul: ...which admittedly is more pedantic. Either that or:
let x = 3
and y = 4
and z = 5
in ...
Alfrothul: ...which is also pedantic.
Dana: Thanks, guys, but we are in Gallina here, not in OCaml. How about we test your unit-test function with the resident multiplication?
Halcyon: Let’s:
Compute (test_mult mult).
Pablito (helpfully): The *response* buffer reads:
= true
: bool
Halcyon: Good.
Bong-sun: Ah, I notice that mult is an alias for Nat.mul.
Dana: Or Init.Nat.mul, depending on your version of tCPA.
Halcyon: Er... How do you know that?
Dana: We just evaluated Check mult..
Alfrothul: Now let’s specify multiplication inductively, in the manner of the inductive specification of addition just before. Given an integer j,
Bong-sun: Aha. I notice that the intuitive sample of numbers includes an instance of the base case?
Anton: Good point. Let me add an instance of the induction step:
Definition test_mult (candidate: nat -> nat -> nat) : bool :=
...
&&
(let j := 10 in
let i' := 3 in
Nat.eqb (candidate (S i') j) (j + candidate i' j))
(* etc. *)
.
Bong-sun: And let me expand the intuitive characterization:
Definition test_mult (candidate: nat -> nat -> nat) : bool :=
...
&&
(Nat.eqb (candidate 3 4) (4 + (4 + (4 + 0))))
(* etc. *)
.
Anton: Actually, we could also test that multiplication distributes over addition:
Definition test_mult (candidate: nat -> nat -> nat) : bool :=
...
&&
(let x := 3 in
let y := 4 in
let z := 5 in
Nat.eqb (candidate x (y + z))
(candidate x y + candidate x z))
(* etc. *)
.
Alfrothul (concentrating): Now for implementing the specification... It is parameterized with the second argument of the multiplication, which suggests a lambda-dropped implementation:
Definition mult_v1 (n j : nat) : nat :=
let fix visit i :=
match i with
O =>
0
| S i' =>
let ih := visit i' (* <- the recursive call implements the induction hypothesis *)
in j + ih
end
in visit n.
Dana: Right – visit is declared in a new lexical block and j is declared outside this block. So this block is scope-sensitive.
Bong-sun: And visit is recursive to account for the inductive specification.
Halcyon: Let’s check whether mult_v1 passes the unit tests:
Compute (test_mult mult_v1).
Pablito (helpfully): The *response* buffer reads:
= true
: bool
Halcyon: Good.
Anton: Do we need to be pedantic here?
Alfrothul (tolerantly): Maybe not – there is no reason to name the result of the recursive call:
Definition mult_v1' (n j : nat) : nat :=
let fix visit i :=
match i with
O =>
0
| S i' =>
j + visit i'
end
in visit n.
Halcyon: Let’s check whether mult_v1' passes the unit tests:
Compute (test_mult mult_v1').
Pablito (helpfully): The *response* buffer reads:
= true
: bool
Halcyon: Good.
Dana: Here is a lambda-lifted implementation:
Fixpoint mult_v2 (i j : nat) : nat :=
match i with
O =>
0
| S i' =>
j + mult_v2 i' j
end.
Bong-sun: Right – there is no block structure, just a toplevel recursive declaration.
Halcyon: Let’s check whether mult_v2' passes the unit tests:
Compute (test_mult mult_v2).
Pablito (helpfully): The *response* buffer reads:
= true
: bool
Halcyon: Good.
For example, binary trees of natural numbers with payloads in their leaves are declared as follows:
Inductive binary_tree_nat : Type :=
Leaf_nat : nat -> binary_tree_nat
| Node_nat : binary_tree_nat -> binary_tree_nat -> binary_tree_nat.
The constructors are Leaf_nat (which is unary) and Node_nat (which is binary). Given a Peano number, we can construct a leaf using Leaf_nat, and given two binary trees, we can construct a node using Leaf_node.
Here is the associated structural-induction principle:
forall n : nat, P (Leaf_nat n) forall t1 : binary_tree_nat, P t1 -> forall t2 : binary_tree_nat, P t2 -> P (Node_nat t1 t2)
------------------------------------------------------------------------------------------------------------------------------
forall t : binary_tree_nat, P t
Or again, with implicit types:
forall n, P (Leaf_nat n) forall t1, P t1 -> forall t2, P t2 -> P (Node_nat t1 t2)
------------------------------------------------------------------------------------
forall t, P t
In this inference rule, forall n, P (Leaf_nat n) is the base case and forall t1, P t1 -> forall t2, P t2 -> P (Node_nat t1 t2) is the induction step. And in this induction step, P t1' and P t2' are the induction hypotheses. (There are two induction hypotheses since we are considering a binary tree. For a ternary tree, there would be three induction hypotheses since the node of a ternary tree contains three subtrees.)
Here is the prototypical skeleton of a recursive function over binary_tree_nat:
Fixpoint prototypical_skeleton_binary_tree_nat (t : binary_tree_nat) : ... :=
match t with
Leaf_nat n =>
...
| Node_nat t1 t2 =>
... (prototypical_skeleton_binary_tree_nat t1') ... (prototypical_skeleton_binary_tree_nat t2') ...
end.
In this skeleton, the first clause (t = Leaf_nat n) implements the base case and the second clause (t = Node_nat t1 t2) implements the induction step. And this second clause, the two recursive calls implement the two induction hypotheses.
For example, here is how to compute the number of leaves in a given binary tree:
Fixpoint number_of_leaves_v1 (t : binary_tree_nat) : nat :=
match t with
Leaf_nat n =>
1
| Node_nat t1 t2 =>
(number_of_leaves_v1 t1) + (number_of_leaves_v1 t2)
end.
Go through the standard functions over binary trees in the accompanying .v file and program them in Gallina, including unit tests: number of nodes, smallest leaf (using <? to compare two natural numbers, which is an infix notation for Nat.ltb), weight, height, well-balancedness of a mobile, and mirror.
The goal of this exercise is to become familiar with the notation and use of Gallina, so the more declarations you write, the better.
Incidentally, the option type in Gallina is the same as in OCaml in that it features the same constructors Some and None.
The previous declaration of binary trees of natural numbers had payloads in the leaves. Binary trees of natural numbers with payloads in the nodes are declared as follows:
Inductive binary_tree_nat' : Type :=
Leaf_nat' : binary_tree_nat'
| Node_nat' : binary_tree_nat' -> nat -> binary_tree_nat' -> binary_tree_nat'.
Implement a function that counts the number of leaves and another that counts the number of nodes in these binary trees.
Declare a type of binary trees of natural numbers with payloads both in the leaves and in the nodes, and implement a function that counts the number of leaves and another that counts the number of nodes in these binary trees.
To visualize whether, for example, + associates implicitly to the left or to the right, check out, e.g., the following pair:
Check (1 + (2 + 3), (1 + 2) + 3).
The *response* window then contains:
(1 + (2 + 3), 1 + 2 + 3)
: nat * nat
The parentheses indicate that + associates implicitly to the left.
Tuples of course are available. For example, evaluating Check (1, 2, 3). yields:
(1, 2, 3)
: nat * nat * nat
Internally, tuples are represented as nested pairs, as can be visualized by evaluating Check (1, (2, 3)). and Check ((1, 2), 3).:
indicating that tuples are represented as nested pairs that are linked to the left and unparsed without parentheses on the left.
In case of confusion, one should simply add parentheses in one’s programs and proofs.
Reformatted test_mult with an opening redundant test [16 Feb 2025]
Added a section about a practical use of the Check command [02 Feb 2025]
Aligned the definitions of testing_the_conjecture_about_baz_x and of testing_the_conjecture_about_baz_y with their informal description [30 Jan 2025]
Added a section about declarations [19 Jan 2025]
Expanded the first section about binary trees to align it with the section about Peano numbers [18 Jan 2025]
Expanded the narrative, added more examples, and removed all mentions of accumulators [17 Jan 2025]
Fleshed out the narrative [17 Jan 2025]
Created [14 Jan 2025]