Class 8: Tactics

For the eighth class, we are going to take a look at tactics by way of an exercise in Coq. Recently, we looked at proof objects in Agda---Coq is built on very similar foundations to Agda, so the proof objects are similar, though with a few differences we'll see during our exercise. Tactics in Coq are search procedures in a tactic language called Ltac that search for these proof objects.

For some continuity, we will start by building off of the same proofs as last week, but in Coq rather than in Agda. (If time allows, we'll move on to some new proofs in the end, too.) In the process, we'll look at some design decisions that Coq makes a bit differently from Agda---and what the implications are for our proofs. More importantly for this class, we'll get a sense of the user experience of writing proofs with tactics.

As before, you have a choice between installation (below) and the pre-installed gitpod (here). Whichever you choose, please test out the artifact before class. If you have any trouble, please post your questions in this thread. You can also drop any installation tips you have in that thread.

Installation Instructions

If you already have Coq 8.14.0 installed, you do not need to do anything. It is OK if you are on a different OCaml installation, or if you are using a different IDE for proof development. If you do not have Coq installed, though, please follow these instructions:

1. If you do not have opam, install it.
2. Otherwise, if you do have opam, run opam update to fetch the latest versions of packages from the repository.
3. Run opam switch create 4.12.0 to install OCaml 4.12.0 in a switch.
4. Run eval $(opam env)$ to configure your environment to use that switch.
5. Install Coq 8.14.0 by running opam pin add coq 8.14.0.
6. Install CoqIDE---the default IDE for Coq---by running opam pin coqide 8.14.0.
7. Run eval $(opam env)$ again to update the shell environment.
8. Download Hello.v, the hello world file.
9. Compile Hello.v (coqc Hello.v from the command line) to test your Coq setup.
10. Open Hello.v in CoqIDE (coqide Hello.v from the command line), and step to the bottom to check your CoqIDE setup.
11. Download this file, which we will work on in class.

If installation fails, and the class forums are no help, do not panic; we will try to match you with someone in class for whom installation worked. (Folks last semester had particular trouble with the latest Apple computers---please let me know if this applies to you.)

You can find the exercise we will do together in class below.

During class, we will again divide up into groups, pairing up people who already have experience with people who are totally new to this. We will then do the exercise in this file. You can do this on your own if you cannot make it to class, or let me know if you'd like me to find you a partner or make an exception.

There is a discussion question at the bottom of the file. This is the only graded part. Please have your group post your answers in this thread, following the directions from the file.