Introduction
The functional programming style is founded on simple, everyday mathematical intuition: If a procedure or method has no side effects, then (ignoring efficiency) all we need to understand about it is how it maps inputs to outputs — that is, we can think of it as just a concrete method for computing a mathematical function. This is one sense of the word "functional" in "functional programming." The direct connection between programs and simple mathematical objects supports both formal correctness proofs and sound informal reasoning about program behavior.
The other sense in which functional programming is "functional" is that it emphasizes the use of functions (or methods) as first-class values — i.e., values that can be passed as arguments to other functions, returned as results, included in data structures, etc. The recognition that functions can be treated as data gives rise to a host of useful and powerful programming idioms.
Other common features of functional languages include algebraic data types and pattern matching, which make it easy to construct and manipulate rich data structures, and sophisticated polymorphic type systems supporting abstraction and code reuse. Coq offers all of these features.
The first half of this chapter introduces the most essential elements of Coq's functional programming language, called Gallina. The second half introduces some basic tactics that can be used to prove properties of Coq programs.
Enumerated Types
One notable aspect of Coq is that its set of built-in features is extremely small. For example, instead of providing the usual palette of atomic data types (booleans, integers, strings, etc.), Coq offers a powerful mechanism for defining new data types from scratch, with all these familiar types as instances.
Naturally, the Coq distribution comes preloaded with an extensive standard library providing definitions of booleans, numbers, and many common data structures like lists and hash tables. But there is nothing magic or primitive about these library definitions. To illustrate this, we will explicitly recapitulate all the definitions we need in this course, rather than just getting them implicitly from the library.
Days of the Week
To see how this definition mechanism works, let's start with a very simple example. The following declaration tells Coq that we are defining a new set of data values — a type.
Inductive day : Type :=
| monday : day
| tuesday : day
| wednesday : day
| thursday : day
| friday : day
| saturday : day
| sunday : day.
The type is called day, and its members are monday, tuesday, etc. The second and following lines of the definition can be read "monday is a day, tuesday is a day, etc."
Having defined day, we can write functions that operate on days.
Definition next_weekday (d:day) : day :=
match d with
| monday ⇒ tuesday
| tuesday ⇒ wednesday
| wednesday ⇒ thursday
| thursday ⇒ friday
| friday ⇒ monday
| saturday ⇒ monday
| sunday ⇒ monday
end.
One thing to note is that the argument and return types of this function are explicitly declared. Like most functional programming languages, Coq can often figure out these types for itself when they are not given explicitly — i.e., it can do type inference — but we'll generally include them to make reading easier.
Having defined a function, we should check that it works on some examples. There are actually three different ways to do this in Coq. First, we can use the command Compute to evaluate a compound expression involving next_weekday.
Compute (next_weekday friday).
(* ==> monday : day *)
Compute (next_weekday (next_weekday saturday)).
(* ==> tuesday : day *)
Second, we can record what we expect the result to be in the form of a Coq example:
Example test_next_weekday:
(next_weekday (next_weekday saturday)) = tuesday.
This declaration does two things: it makes an assertion (that the second weekday after saturday is tuesday), and it gives the assertion a name that can be used to refer to it later. Having made the assertion, we can also ask Coq to verify it, like this:
Proof. simpl. reflexivity. Qed.
The details are not important for now (we'll come back to them in a bit), but essentially this can be read as "The assertion we've just made can be proved by observing that both sides of the equality evaluate to the same thing, after some simplification."
Third, we can ask Coq to extract, from our Definition, a program in some other, more conventional, programming language (OCaml, Scheme, or Haskell) with a high-performance compiler. This facility is very interesting, since it gives us a way to go from proved-correct algorithms written in Gallina to efficient machine code. (Of course, we are trusting the correctness of the OCaml/Haskell/Scheme compiler, and of Coq's extraction facility itself, but this is still a big step forward from the way most software is developed today.) Indeed, this is one of the main uses for which Coq was developed. We'll come back to this topic in later chapters.
Booleans
In a similar way, we can define the standard type bool of booleans, with members true and false.
Inductive bool : Type :=
| true : bool
| false : bool.
Although we are rolling our own booleans here for the sake of building up everything from scratch, Coq does, of course, provide a default implementation of the booleans, together with a multitude of useful functions and lemmas. (Take a look at Coq.Init.Datatypes in the Coq library documentation if you're interested.) Whenever possible, we'll name our own definitions and theorems so that they exactly coincide with the ones in the standard library.
Functions over booleans can be defined in the same way as above:
Definition negb (b:bool) : bool :=
match b with
| true ⇒ false
| false ⇒ true
end.
Definition andb (b1:bool) (b2:bool) : bool :=
match b1 with
| true ⇒ b2
| false ⇒ false
end.
Definition orb (b1:bool) (b2:bool) : bool :=
match b1 with
| true ⇒ true
| false ⇒ b2
end.
The last two of these illustrate Coq's syntax for multi-argument function definitions. The corresponding multi-argument application syntax is illustrated by the following "unit tests," which constitute a complete specification — a truth table — for the orb function:
Example test_orb1: (orb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb2: (orb false false) = false.
Proof. simpl. reflexivity. Qed.
Example test_orb3: (orb false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb4: (orb true true) = true.
Proof. simpl. reflexivity. Qed.
We can also introduce some familiar syntax for the boolean operations we have just defined. The Infix command defines a new symbolic notation for an existing definition.
Infix "&&" := andb.
Infix "||" := orb.
Example test_orb5: false || false || true = true.
Proof. simpl. reflexivity. Qed.
A note on notation: In .v files, we use square brackets to delimit fragments of Coq code within comments; this convention, also used by the coqdoc documentation tool, keeps them visually separate from the surrounding text. In the html version of the files, these pieces of text appear in a different font.
The command Admitted can be used as a placeholder for an incomplete proof. We'll use it in exercises, to indicate the parts that we're leaving for you — i.e., your job is to replace Admitteds with real proofs.
Function Types
Every expression in Coq has a type, describing what sort of thing it computes. The Check command asks Coq to print the type of an expression.
Check true.
(* ===> true : bool *)
Check (negb true).
(* ===> negb true : bool *)
Functions like negb itself are also data values, just like true and false. Their types are called function types, and they are written with arrows.
Check negb.
(* ===> negb : bool -> bool *)
The type of negb, written bool → bool and pronounced "bool arrow bool," can be read, "Given an input of type bool, this function produces an output of type bool." Similarly, the type of andb, written bool → bool → bool, can be read, "Given two inputs, both of type bool, this function produces an output of type bool."
Modules
Coq provides a module system, to aid in organizing large developments. In this course we won't need most of its features, but one is useful: If we enclose a collection of declarations between Module X and End X markers, then, in the remainder of the file after the End, these definitions are referred to by names like X.foo instead of just foo. We will use this feature to introduce the definition of the type nat in an inner module so that it does not interfere with the one from the standard library (which we want to use in the rest because it comes with a tiny bit of convenient special notation).
Module NatPlayground.
Numbers
The types we have defined so far are examples of "enumerated types": their definitions explicitly enumerate a finite set of elements. A more interesting way of defining a type is to give a collection of inductive rules describing its elements. For example, we can define (a unary representation of) the natural numbers as follows:
Inductive nat : Type :=
| O : nat
| S : nat → nat.
The clauses of this definition can be read:
- O is a natural number (note that this is the letter "O," not the numeral "0").
- S is a "constructor" that takes a natural number and yields another one — that is, if n is a natural number, then S n is too.
Every inductively defined set (day, nat, bool, etc.) is actually a set of expressions built from constructors like O, S, true, false, monday, etc. The definition of nat says how expressions in the set nat can be built:
- O and S are constructors;
- the expression O belongs to the set nat;
- if n is an expression belonging to the set nat, then S n is also an expression belonging to the set nat; and
- expressions formed in these two ways are the only ones belonging to the set nat.
The same rules apply for our definitions of day and bool. (The annotations we used for their constructors are analogous to the one for the O constructor, indicating that they don't take any arguments.)
The above conditions are the precise force of the Inductive declaration. They imply that the expression O, the expression S O, the expression S (S O), the expression S (S (S O)), and so on all belong to the set nat, while other expressions built from data constructors, like true, andb true false, S (S false), and O (O (O S)) do not.
A critical point here is that what we've done so far is just to define a representation of numbers: a way of writing them down. The names O and S are arbitrary, and at this point they have no special meaning — they are just two different marks that we can use to write down numbers (together with a rule that says any nat will be written as some string of S marks followed by an O). If we like, we can write essentially the same definition this way:
Inductive nat' : Type :=
| stop : nat'
| tick : nat' → nat'.
The interpretation of these marks comes from how we use them to compute.
We can do this by writing functions that pattern match on representations of natural numbers just as we did above with booleans and days — for example, here is the predecessor function:
Definition pred (n : nat) : nat :=
match n with
| O ⇒ O
| S n' ⇒ n'
end.
The second branch can be read: "if n has the form S n' for some n', then return n'."
End NatPlayground.
Definition minustwo (n : nat) : nat :=
match n with
| O ⇒ O
| S O ⇒ O
| S (S n') ⇒ n'
end.
Because natural numbers are such a pervasive form of data, Coq provides a tiny bit of built-in magic for parsing and printing them: ordinary arabic numerals can be used as an alternative to the "unary" notation defined by the constructors S and O. Coq prints numbers in arabic form by default:
Check (S (S (S (S O)))).
(* ===> 4 : nat *)
Compute (minustwo 4).
(* ===> 2 : nat *)
The constructor S has the type nat → nat, just like the functions minustwo and pred:
Check S.
Check pred.
Check minustwo.
These are all things that can be applied to a number to yield a number. However, there is a fundamental difference between the first one and the other two: functions like pred and minustwo come with computation rules — e.g., the definition of pred says that pred 2 can be simplified to 1 — while the definition of S has no such behavior attached. Although it is like a function in the sense that it can be applied to an argument, it does not do anything at all! It is just a way of writing down numbers. (Think about standard arabic numerals: the numeral 1 is not a computation; it's a piece of data. When we write 111 to mean the number one hundred and eleven, we are using 1, three times, to write down a concrete representation of a number.)
For most function definitions over numbers, just pattern matching is not enough: we also need recursion. For example, to check that a number n is even, we may need to recursively check whether n-2 is even. To write such functions, we use the keyword Fixpoint.
Fixpoint evenb (n:nat) : bool :=
match n with
| O ⇒ true
| S O ⇒ false
| S (S n') ⇒ evenb n'
end.
We can define oddb by a similar Fixpoint declaration, but here is a simpler definition:
Definition oddb (n:nat) : bool := negb (evenb n).
Example test_oddb1: oddb 1 = true.
Proof. simpl. reflexivity. Qed.
Example test_oddb2: oddb 4 = false.
Proof. simpl. reflexivity. Qed.
(You will notice if you step through these proofs that simpl actually has no effect on the goal — all of the work is done by reflexivity. We'll see more about why that is shortly.)
Naturally, we can also define multi-argument functions by recursion.
Module NatPlayground2.
Fixpoint plus (n : nat) (m : nat) : nat :=
match n with
| O ⇒ m
| S n' ⇒ S (plus n' m)
end.
Adding three to two now gives us five, as we'd expect.
Compute (plus 3 2).
The simplification that Coq performs to reach this conclusion can be visualized as follows:
(* plus (S (S (S O))) (S (S O))
==> S (plus (S (S O)) (S (S O)))
by the second clause of the match
==> S (S (plus (S O) (S (S O))))
by the second clause of the match
==> S (S (S (plus O (S (S O)))))
by the second clause of the match
==> S (S (S (S (S O))))
by the first clause of the match
*)
As a notational convenience, if two or more arguments have the same type, they can be written together. In the following definition, (n m : nat) means just the same as if we had written (n : nat) (m : nat).
Fixpoint mult (n m : nat) : nat :=
match n with
| O ⇒ O
| S n' ⇒ plus m (mult n' m)
end.
Example test_mult1: (mult 3 3) = 9.
Proof. simpl. reflexivity. Qed.
You can match two expressions at once by putting a comma between them:
Fixpoint minus (n m:nat) : nat :=
match n, m with
| O , _ ⇒ O
| S _ , O ⇒ n
| S n', S m' ⇒ minus n' m'
end.
The _ in the first line is a wildcard pattern. Writing _ in a pattern is the same as writing some variable that doesn't get used on the right-hand side. This avoids the need to invent a variable name.
End NatPlayground2.
Fixpoint exp (base power : nat) : nat :=
match power with
| O ⇒ S O
| S p ⇒ mult base (exp base p)
end.
网友评论