(** * Basics: Functional Programming in Coq *)
(* REMINDER:
#####################################################
### PLEASE DO NOT DISTRIBUTE SOLUTIONS PUBLICLY ###
#####################################################
(See the [Preface] for why.)
*)
(* ################################################################# *)
(** * 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. *)
(* ################################################################# *)
(** * Data and Functions *)
(* ================================================================= *)
(** ** 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
| tuesday
| wednesday
| thursday
| friday
| saturday
| sunday.
(** The type is called [day], and its members are [monday],
[tuesday], 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 *)
(** (We show Coq's responses in comments, but, if you have a
computer handy, this would be an excellent moment to fire up the
Coq interpreter under your favorite IDE -- either CoqIde or Proof
General -- and try this for yourself. Load this file, [Basics.v],
from the book's Coq sources, find the above example, submit it to
Coq, and observe the result.) *)
(** 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. *)
(* ================================================================= *)
(** ** Homework Submission Guidelines *)
(** If you are using _Software Foundations_ in a course, your
instructor may use automatic scripts to help grade your homework
assignments. In order for these scripts to work correctly (so
that you get full credit for your work!), please be careful to
follow these rules:
- The grading scripts work by extracting marked regions of the
[.v] files that you submit. It is therefore important that
you do not alter the "markup" that delimits exercises: the
Exercise header, the name of the exercise, the "empty square
bracket" marker at the end, etc. Please leave this markup
exactly as you find it.
- Do not delete exercises. If you skip an exercise (e.g.,
because it is marked Optional, or because you can't solve it),
it is OK to leave a partial proof in your [.v] file, but in
this case please make sure it ends with [Admitted] (not, for
example [Abort]).
- It is fine to use additional definitions (of helper functions,
useful lemmas, etc.) in your solutions. You can put these
between the exercise header and the theorem you are asked to
prove.
You will also notice that each chapter (like [Basics.v]) is
accompanied by a _test script_ ([BasicsTest.v]) that automatically
calculates points for the finished homework problems in the
chapter. These scripts are mostly for the auto-grading
infrastructure that your instructor may use to help process
assignments, but you may also like to use them to double-check
that your file is well formatted before handing it in. In a
terminal window either type [make BasicsTest.vo] or do the
following:
coqc -Q . LF Basics.v
coqc -Q . LF BasicsTest.v
There is no need to hand in [BasicsTest.v] itself (or [Preface.v]).
_If your class is using the Canvas system to hand in assignments_:
- If you submit multiple versions of the assignment, you may
notice that they are given different names. This is fine: The
most recent submission is the one that will be graded.
- To hand in multiple files at the same time (if more than one
chapter is assigned in the same week), you need to make a
single submission with all the files at once using the button
"Add another file" just above the comment box. *)
(* ================================================================= *)
(** ** Booleans *)
(** In a similar way, we can define the standard type [bool] of
booleans, with members [true] and [false]. *)
Inductive bool : Type :=
| true
| false.
(** 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 [Notation] command defines a new
symbolic notation for an existing definition. *)
Notation "x && y" := (andb x y).
Notation "x || y" := (orb x y).
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
[Admitted]s with real proofs. *)
(** **** Exercise: 1 star, standard (nandb)
Remove "[Admitted.]" and complete the definition of the following
function; then make sure that the [Example] assertions below can
each be verified by Coq. (I.e., fill in each proof, following the
model of the [orb] tests above.) The function should return [true]
if either or both of its inputs are [false]. *)
Definition nandb (b1:bool) (b2:bool) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Example test_nandb1: (nandb true false) = true.
(* FILL IN HERE *) Admitted.
Example test_nandb2: (nandb false false) = true.
(* FILL IN HERE *) Admitted.
Example test_nandb3: (nandb false true) = true.
(* FILL IN HERE *) Admitted.
Example test_nandb4: (nandb true true) = false.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 1 star, standard (andb3)
Do the same for the [andb3] function below. This function should
return [true] when all of its inputs are [true], and [false]
otherwise. *)
Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Example test_andb31: (andb3 true true true) = true.
(* FILL IN HERE *) Admitted.
Example test_andb32: (andb3 false true true) = false.
(* FILL IN HERE *) Admitted.
Example test_andb33: (andb3 true false true) = false.
(* FILL IN HERE *) Admitted.
Example test_andb34: (andb3 true true false) = false.
(* FILL IN HERE *) Admitted.
(** [] *)
(* ================================================================= *)
(** ** 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]." *)
(* ================================================================= *)
(** ** New Types from Old *)
(** The types we have defined so far are examples of "enumerated
types": their definitions explicitly enumerate a finite set of
elements, each of which is just a bare constructor. Here is a
more interesting type definition, where one of the constructors
takes an argument: *)
Inductive rgb : Type :=
| red
| green
| blue.
Inductive color : Type :=
| black
| white
| primary (p : rgb).
(** Let's look at this in a little more detail.
Every inductively defined type ([day], [bool], [rgb], [color],
etc.) contains a set of _constructor expressions_ built from
_constructors_ like [red], [primary], [true], [false], [monday],
etc.
The definitions of [rgb] and [color] say how expressions in the
sets [rgb] and [color] can be built:
- [red], [green], and [blue] are the constructors of [rgb];
- [black], [white], and [primary] are the constructors of [color];
- the expression [red] belongs to the set [rgb], as do the
expressions [green] and [blue];
- the expressions [black] and [white] belong to the set [color];
- if [p] is an expression belonging to the set [rgb], then
[primary p] (pronounced "the constructor [primary] applied to
the argument [p]") is an expression belonging to the set
[color]; and
- expressions formed in these ways are the _only_ ones belonging
to the sets [rgb] and [color]. *)
(** We can define functions on colors using pattern matching just as
we have done for [day] and [bool]. *)
Definition monochrome (c : color) : bool :=
match c with
| black => true
| white => true
| primary q => false
end.
(** Since the [primary] constructor takes an argument, a pattern
matching [primary] should include either a variable (as above --
note that we can choose its name freely) or a constant of
appropriate type (as below). *)
Definition isred (c : color) : bool :=
match c with
| black => false
| white => false
| primary red => true
| primary _ => false
end.
(** The pattern [primary _] here is shorthand for "[primary] applied
to any [rgb] constructor except [red]." (The wildcard pattern [_]
has the same effect as the dummy pattern variable [p] in the
definition of [monochrome].) *)
(* ================================================================= *)
(** ** Tuples *)
(** A single constructor with multiple parameters can be used
to create a tuple type. As an example, consider representing
the four bits in a nybble (half a byte). We first define
a datatype [bit] that resembles [bool] (using the
constructors [B0] and [B1] for the two possible bit values),
and then define the datatype [nybble], which is essentially
a tuple of four bits. *)
Inductive bit : Type :=
| B0
| B1.
Inductive nybble : Type :=
| bits (b0 b1 b2 b3 : bit).
Check (bits B1 B0 B1 B0).
(* ==> bits B1 B0 B1 B0 : nybble *)
(** The [bits] constructor acts as a wrapper for its contents.
Unwrapping can be done by pattern-matching, as in the [all_zero]
function which tests a nybble to see if all its bits are O.
Note that we are using underscore (_) as a _wildcard pattern_ to
avoid inventing variable names that will not be used. *)
Definition all_zero (nb : nybble) : bool :=
match nb with
| (bits B0 B0 B0 B0) => true
| (bits _ _ _ _) => false
end.
Compute (all_zero (bits B1 B0 B1 B0)).
(* ===> false : bool *)
Compute (all_zero (bits B0 B0 B0 B0)).
(* ===> true : 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). *)
(* Wed Jan 9 12:02:44 EST 2019 *)