TIEA1000 Topical Themes in Mathematical Information Technology: Dependently-Typed Programming and Proof Theory, 1–5 ECTS

This is the course plan drafted on 2019-05-01 and finalized on 2019-09-03.

Introduction

Welcome to a new course on using the Coq proof assistant to explore dependently-typed programming and proof theory. This course is mostly based on CIS 500 [1] as organized in the University of Pennsylvania, although we only have half the time and cover only about a quarter of the material. In particular, we cover

• basic functional programming, involving
  • terms and types,
  • recursion and
  • reduction,
• proof by induction, using
  • the usual induction principle on natural numbers,
  • structural induction on types, such as lists, and
  • path induction (or based path induction) on equalities,
• lists and polymorphism, featuring higher-order functions like
  • map and
  • fold (also known as reduce),
• interactive metaprogramming with tactics, focusing on
  • partial application,
  • pattern matching and
  • rewriting,
• mathematical logic, as in
  • truth and falsehood,
  • negation, conjunction and disjunction,
  • universal and existential quantification and
  • axioms, such as functional extensionality, exluded middle, double negation elimination, choice and univalence,
• inductive propositions, via case studies in
  • computational reflection and
  • matching regular expressions, and
• propositions as types, to tie it all together.

This course is not intended to make you an expert Coq user, but rather to give you a concrete feel of formal proofs. Understanding their essence is, in my experience, both practically useful and philosophically satisfying.

Prerequisites

Completing this course requires mathematical maturity and a good grasp of programming. While these requirements are difficult to quantify exactly, familiarity with some (say, three) of the following courses should suffice.

However, the lack of familiarity can be compensated with time and motivation.

Materials

The main material for this course, henceforth known as the book, is Software Foundations: Logical Foundations [2]. It is freely licensed and available online (see the section on completing the course about obtaining it). Supplementary material, or the other books, include Certified Programming with Dependent Types [3] and Homotopy Type Theory: Univalent Foundations of Mathematics [4]. They are also more or less freely licensed and available online.

The book contains all the necessary exposition and exercises we will need on this course. It is elementary in the sense that it can be understood completely by the end of the course. The other books are there just for the amusement of those who enjoy living inside their heads. They are not elementary at all, as they bring the reader to the forefront of research, where nobody understands the topics completely.

Schedule

This course begins with an introductory lecture on 2019-09-03 16:15 (local time, whatever that may be), features two classroom activities per week and ends by 2019-10-29 18:00. The classroom activities align with the book in the following way.

At the beginning of each week, a set of exercises is assigned from the book. Each set must be done before the next set is assigned, so there is exactly one week of time to do each one. However, nothing prevents doing future exercises ahead of time or going back to improve past exercises later (there are a few exercises that may benefit from doing this).

You may personally negotiate later deadlines, but this is generally not a good idea, because catching up is really difficult. Ideally, we would not have any deadlines at all, but experience suggests that they really improve outcomes.

Classroom Activities

The classroom activities on this course are primarily exercise sessions, where you can do exercises together and get guidance from an instructor. The activities may secondarily become lectures, in case general questions arise or I happen to have some interesting stories to tell, but the remaining time is always reserved for exercises. Participation is voluntary, but strongly encouraged.

The activities should take place in a computer classroom, but it is a good idea to bring your own laptop regardless.

Exercises, Grades and Credits

Exercises in the book are rated from one to five stars. The easiest exercises have the rating of one star and often take less than a minute to do, while the hardest exercises have the rating of five stars and can sometimes take several hours to get right. The scale is obviously nonlinear, but this is balanced out by the fact that there is a limited supply of exercises.

In the chapters covered on this course, there are

• 152 exercises worth 355 stars, consisting of
• 76 nonoptional nonadvanced exercises worth 154 stars,
• 48 optional nonadvanced exercises worth 121 stars and
• 28 advanced exercises worth 80 stars.

While these classifications provide some insight into the structure of the book, they do not affect your assessment in any way. Your grade \(\measuredangle\) or, more precisely, the number of credits you get from passing this course, is simply determined by feeding the number of stars \(\star\) you have gotten from fully completed exercises to the projection function \(\pi\), which is defined according to

\[\begin{eqnarray} {\star} & : & \mathcal U \\ {\star} & = & \{n : \mathbb N \mid n \le 355\} \\ {\measuredangle} & : & \mathcal U \\ {\measuredangle} & = & \{n : \mathbb N \mid n \le 5\} \\ \pi & : & {\star} \to {\measuredangle} \\ \pi (n) & = & \begin{cases} 0, & \phantom{00}0 \le n \le 177 \\ 1, & 178 \le n \le 213 \\ 2, & 214 \le n \le 248 \\ 3, & 249 \le n \le 284 \\ 4, & 285 \le n \le 319 \\ 5, & 320 \le n \le 355. \end{cases} \end{eqnarray}\]

I reserve the right to transparently hand out extra stars for doing harder exercises from the other books, pointing out mistakes in the material or being helpful in other ways.

Summative and Formative Assessment

I will grade your solutions within one month of you handing them in (see the section on completing the course for details).

Time permitting, I will also look over your solutions and provide feedback. The feedback will not affect your grade, unless your solutions are obviously plagiarized. If you happen to copy someone else’s answer, be honest about it and explain what lead you to do so and what you learned from it. As long as this does not happen too frequently, it will not be considered plagiarism.

Tests or Examinations

There is no written test, but there is a brief oral test at the end of the course. The oral test consists of one question and its sole purpose is to ensure that you did not blindly copy your solutions from the Internet or forcefully smack Coq into submission. It is not graded, but it can be failed (with a dedicated lack of effort).

Completing the Course

The following instructions explain how to complete this course, in as much detail as possible.

• Download version 5.6 of the book for version 8.8.1 of Coq.
  • It is very important to get the right version of the book, which is why you should download it from our server [5]. You may also verify that the SHA-256 sum of the archive really is cc82826d5f382fe3e0552bca4533c6dbed36983ce3d9f38938a59e5777af0032.
• Install version 8.9.1 of Coq [6].
  • You may also use the existing installations available on the computer classroom machines.
  • It may be possible to use a newer version of Coq as well, but be warned that it may not be fully compatible with the book or the recommended version of Coq.
  • If you hand in your solutions and they happen to be incompatible with the recommended version of Coq, they will be graded as if they were wrong.
• Install an interactive editor for Coq, such as CoqIDE [6], Proof General [7] or Coqtail [8].
  • Again, existing installations of CoqIDE are available on the computer classroom machines.
  • While it is possible to use Coq from the command line, it makes for a miserable user experience (try it and see).
  • There is also an experimental web interface for Coq [9], [10], but, as the author says, “data loss is guaranteed”. Use it at your own risk.
• Open the source files of the book in your editor of choice and make sure you can interact with them properly.
  • There are a few things that can go wrong, such as your editor failing to read the _CoqProject file. It is good to work these wrinkles out ahead of time.
• Do the assigned exercises by only modifying the indicated lines or adding new lines nearby.
  • This makes it much easier for me to see your changes and give feedback based on them.
• Hand in your solutions by returning the modified source files.
  • From best to worst method, you can do this by
    • linking me a single Git repository that tracks the source files,
    • linking me a single Gzip archive that contains the source files,
    • linking me a single ZIP archive that contains the source files,
    • sending me an email with the source files as attachments,
    • sending me an email with a single Gzip archive that contains the source files as an attachment or
    • sending me an email with a single ZIP archive that contains the source files as an attachment.
  • You should learn how to do this by the beginning of the course (see the section on returning files for hints).
• Ask me to schedule an oral test for you and attend it.
  • This should only take a minute.

Returning Files

If you send me an archive, package the files instead of the directories and name the archive according to your university username.

To create a Gzip archive, you can use the following command.

$ tar -czf sapekiis.tar.gz \
  Preface.v Basics.v Induction.v Lists.v Poly.v \
  Tactics.v Logic.v IndProp.v ProofObjects.v Postscript.v

Make sure to check that you did not accidentally package your animes, because I do not want to see that garbage.

$ tar -tf sapekiis.tar.gz

To create a ZIP archive, you can use either of the following commands.

$ rm -f sapekiis.zip && zip -9q sapekiis.zip \
  Preface.v Basics.v Induction.v Lists.v Poly.v \
  Tactics.v Logic.v IndProp.v ProofObjects.v Postscript.v
$ jar -Mcf sapekiis.zip \
  Preface.v Basics.v Induction.v Lists.v Poly.v \
  Tactics.v Logic.v IndProp.v ProofObjects.v Postscript.v

Checking the packaging works analogously.

$ unzip -l sapekiis.zip
$ jar -tf sapekiis.zip

Making a public Git repository is a bit more involved, but can be done on the university network as follows.

Let us first create a remote repository with a random name.

$ ssh sapekiis@charra.it.jyu.fi
$ cd /autowebhome/home/sapekiis/public_html
$ echo "$(echo "$RANDOM" | sha256sum | head -c 6).git"
abcdef
$ mkdir abcdef
$ cd abcdef
$ git init --bare
Initialized empty Git repository in /autowebhome/home/sapekiis/public_html/abcdef/
$ mv hooks/post-update.sample hooks/post-update
$ git update-server-info
$ exit

Let us then create a local counterpart of the same repository.

$ cd
$ mkdir tiea1000
$ cd tiea1000
$ git init
Initialized empty Git repository in /home/sapekiis/tiea1000/.git/
$ touch Preface.v Basics.v Induction.v Lists.v Poly.v \
  Tactics.v Logic.v IndProp.v ProofObjects.v Postscript.v
$ git add Preface.v Basics.v Induction.v Lists.v Poly.v \
  Tactics.v Logic.v IndProp.v ProofObjects.v Postscript.v
$ git commit -m "Did all the exercises."
[master (root-commit) defaced] Did all the exercises.
  10 files changed, 0 insertions(+), 0 deletions(-)
  create mode 100644 Preface.v
  create mode 100644 Basics.v
  create mode 100644 Induction.v
  create mode 100644 Lists.v
  create mode 100644 Poly.v
  create mode 100644 Tactics.v
  create mode 100644 Logic.v
  create mode 100644 IndProp.v
  create mode 100644 ProofObjects.v
  create mode 100644 Postscript.v
$ git push --set-upstream sapekiis@charra.it.jyu.fi:/autowebhome/home/sapekiis/public_html/abcdef.git master
Counting objects: 3, done.
Writing objects: 100% (20/20), 420 bytes | 0 bytes/s, done.
Total 20 (delta 0), reused 0 (delta 0)
To sapekiis@charra.it.jyu.fi:/autowebhome/home/sapekiis/public_html/abcdef.git
  * [new branch]      master -> master
Branch master set up to track remote branch master from sapekiis@charra.it.jyu.fi:/autowebhome/home/sapekiis/public_html/abcdef.git.

Anyone can now clone the repository as follows.

$ cd /tmp
$ git clone http://users.jyu.fi/~sapekiis/abcdef.git
Cloning into 'abcdef'...
Checking connectivity... done.
$ cd abcdef
$ git ls-files
Preface.v
Basics.v
Induction.v
Lists.v
Poly.v
Tactics.v
Logic.v
IndProp.v
ProofObjects.v
Postscript.v

While Git is the best way to do and return your solutions, I would recommend against using it if you do not know how to do so properly.

References