Day01_intro
Intro: Functional Programming in Coq
From Coq Require Export String.
(* REMINDER:
########################## # PLEASE DO NOT DISTRIBUTE SOLUTIONS PUBLICLY # ##########################
(See the Preface for why.)
*)
(* REMINDER:
########################## # PLEASE DO NOT DISTRIBUTE SOLUTIONS PUBLICLY # ##########################
(See the Preface for why.)
*)
Introduction
- functional programming, and
- (inductive) proof.
- a functional programming part in Coq (YOU ARE HERE),
- a formal proof part in Coq, and
- an informal proof part on paper.
- Some students skip the intro course (CS051), and we want
everyone to have the same programming fundamentals. Teaching
functional programming is a good way to achieve that.
- A lot of what people teach in discrete math courses isn't that relevant to many computer scientists. We'd rather focus on the parts that are most important.
What is functional programming?
Getting the tools in order
- https://coq.inria.fr/download
- Windows:
http://mirrors.ocf.berkeley.edu/gnu/emacs/windows/emacs-27/emacs-27.1-x86_64.zip
- macOS: https://emacsformacosx.com/ (or brew cask install
emacs)
- Linux: apt install emacs (depending on distro)
- https://cs.pomona.edu/classes/cs54/downloads/init.el
Enumerated Types
Days of the Week
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.
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 several different ways to check your work
in Coq. Later on, we'll prove our work correct! For now, we can
use the Check command to type check an expression and Compute
command to evaluate an expression involving next_weekday.
Check friday.
(* ==> friday : day *)
Check (next_weekday friday).
(* ==> next_weekday friday : day*)
Compute (next_weekday friday).
(* ==> monday : day *)
Compute (next_weekday (next_weekday saturday)).
(* ==> tuesday : day *)
(* ==> friday : day *)
Check (next_weekday friday).
(* ==> next_weekday friday : day*)
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 in
VS Code and try this for yourself. Load this file, Day01_intro.v, from the book's Coq sources, find the above example, submit it to Coq, and observe the result.)
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
won't really talk about extraction more in this course.
Homework Submission Guidelines
- 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.
- As we work our way through the files, keep in mind that we'll grade you in terms of our old definitions, not yours. If you want to use a helper function from an earlier file in a later one, be sure to copy it over.
Booleans
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. First, we can use booleans to define a predicate, a
function that identifies some subset of a given set:
Definition is_weekday (d:day) : bool :=
match d with
| monday ⇒ true
| tuesday ⇒ true
| wednesday ⇒ true
| thursday ⇒ true
| friday ⇒ true
| saturday ⇒ false
| sunday ⇒ false
end.
match d with
| monday ⇒ true
| tuesday ⇒ true
| wednesday ⇒ true
| thursday ⇒ true
| friday ⇒ true
| saturday ⇒ false
| sunday ⇒ false
end.
We can also define some of the usual operations on
booleans. First comes not or negation, which is often written
as the operator !.
Coq also lets you use conventional if/then/else notation for
booleans, as in:
Every other datatype will need you to use match, though!
Depending on other languages you've learned, you may have seen a
"one-armed if" before. You can't do that in Coq---every
expression must return a value, and a missing else branch would
leave Coq wondering what to return.
Another common way of expressing functions from booleans to
booleans is with a truth table.
Each row of the truth table gives a possible assignment: you can
read the first row as saying that if b = true, then negb b =
false; the second row says that if b = false, then negb b =
true.
|---|--------| | b | negb b | |---|--------| | T | F | | F | T | |---|--------|Each column of the truth table represents an expression of type bool. Here the first column represents an arbitrary input b, which can be true (written T) or false (written F). It's typical to consider the initial columns of a truth table as representing inputs and the final column as representing an output.
When constructing a truth table with more than one input,
it's important to make sure your truth table has every possible
input configuration accounted for. People have different ways of
doing so, but I tend to like the following format, where we
exhaust all of the possibilities for the first column to be true,
and then we consider the cases where the first column is
false. Electrical engineers, however, like to do it the opposite
way: when false is 0 and true is 1, it makes sense to count "up".
It doesn't particularly matter which method you choose, but it's
important to be consistent!
|----|----|------------| | b1 | b2 | andb b1 b2 | |----|----|------------| | T | T | T | | T | F | F | | F | T | F | | F | F | F | |----|----|------------|
|----|----|-----------| | b1 | b2 | orb b1 b2 | |----|----|-----------| | T | T | T | | T | F | T | | F | T | T | | F | F | F | |----|----|-----------|
Compute (orb true true ).
Compute (orb true false).
Compute (orb false true ).
Compute (orb false false).
Compute (orb true false).
Compute (orb false true ).
Compute (orb false false).
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.
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.
You can use negb, but please do not use andb when you're
defining this function.
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. (Remove "Admitted." and 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.
(* Do not modify the following line: *)
Definition manual_grade_for_nandb : option (nat×string) := None.
☐
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(* Do not modify the following line: *)
Definition manual_grade_for_nandb : option (nat×string) := None.
☐
(* What's that box symbol? It represents the end of an exercise. Since
it's in a comment, it doesn't _do_ anything. It shouldn't hurt if
you remove it, but there's no need to. *)
Compute (nandb true true ).
Compute (nandb true false).
Compute (nandb false true ).
Compute (nandb false false).
it's in a comment, it doesn't _do_ anything. It shouldn't hurt if
you remove it, but there's no need to. *)
Compute (nandb true true ).
Compute (nandb true false).
Compute (nandb false true ).
Compute (nandb false false).
Truth tables are a particularly nice way of calculating
compound expressions involving booleans. In addition to having
input and output columns, we can have intermediate columns
representing subexpressions of the boolean we're interested in.
When building such a truth table, every subexpression of
the final result should show up as a column.
|---|--------|-----------------| | b | negb b | orb b (negb b) | |---|--------|-----------------| | T | F | T | | F | T | T | |---|--------|-----------------|
Exercise: 1 star, standard (impb)
Write a function impb such that impb b1 b2 has the same truth table as orb (negb b1) b2. Don't just trivially define it as orb (negb b1) b2, though! Try using a match.
Definition impb (b1:bool) (b2:bool) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(* Do not modify the following line: *)
Definition manual_grade_for_impb : option (nat×string) := None.
☐
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(* Do not modify the following line: *)
Definition manual_grade_for_impb : option (nat×string) := None.
☐
Function Types
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.
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."
You might think of the function orb as taking two arguments, but every
function in Coq takes one argument at a time. Each argument gets its own arrow. You can think of this as saying that orb is a function that takes a
boolean and returns another function that takes another boolean... and that returns a boolean. Look:
Check (orb true).
(* ===> orb true : bool -> bool *)
Check (orb true false).
(* ===> true || false : bool *)
(* ===> orb true : bool -> bool *)
Check (orb true false).
(* ===> true || false : bool *)
Function types are right associative, i.e., parentheses go on the right,
i.e., A → B → C is the same as A → (B → C).
Function application is left associative, i.e., parentheses go on the left, i.e., a b c is the same (a b) c.
The Fail prefix says that we expect a command to not work. It's
useful for examples like this!
Fail Check (orb (true false)).
(* ===>
The command has indeed failed with message:
Illegal application (Non-functional construction):
The expression "true" of type "bool"
cannot be applied to the term
"false" : "bool"
*)
(* ===>
The command has indeed failed with message:
Illegal application (Non-functional construction):
The expression "true" of type "bool"
cannot be applied to the term
"false" : "bool"
*)
Case study: DNA nucleotides
DNA has a double helix structure comprising two paired
strands, where each C corresponds to a G and each A
corresponds to T. We won't get to defining DNA strands for a few
weeks, but we can already start thinking about DNA in a more
detailed way.
The DNA double helix has 'complementary' structure: if you know
the bases of one strand, you know the bases of the other.
We can express this idea with a function that computes the
complement for a given base.
Exercise: 1 star, standard (xorb)
Here is the truth table for xorb (eXclusive OR on Booleans).|----|----|---------| | b1 | b2 | xorb b1 | |----|----|---------| | T | T | F | | T | F | T | | F | T | T | | F | F | F | |----|----|---------|
(* FILL IN HERE *)
(* Do not modify the following line: *)
Definition manual_grade_for_xorb : option (nat×string) := None.
☐
(* Do not modify the following line: *)
Definition manual_grade_for_xorb : option (nat×string) := None.
☐
Exercise: 2 stars, standard (is_classday)
Write a function is_classday : day → bool that returns true exactly when it's a day we have CS054 (in FA2021, that's TR). It should be of type day → bool.
(* Do not modify the following line: *)
Definition manual_grade_for_is_classday : option (nat×string) := None.
☐
Definition manual_grade_for_is_classday : option (nat×string) := None.
☐
Exercise: 2 stars, standard (eq_base)
Write a function eq_base : base → base → bool that returns true exactly when two bases are equal.
Definition eq_base (b1 b2 : base) : bool (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
☐
☐
How to succeed in this course
(* 2021-09-28 15:37 *)