For the sixth class, we are going to take a look at tactics by way of an exercise in Coq. Last week, 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.
Installation can be finicky, so please install the artifact before class using the instructions below. If you have any trouble, please post your questions in this thread. You can also drop any installation tips you have in that thread.
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:
- If you do not have opam, install it.
- Otherwise, if you do have opam, run
opam updateto fetch the latest versions of packages from the repository.
opam switch create 4.12.0to install OCaml 4.12.0 in a switch.
eval $(opam env)$to configure your environment to use that switch.
- Install Coq 8.14.0 by running
opam pin add coq 8.14.0.
- Install CoqIDE---the default IDE for Coq---by running
opam pin coqide 8.14.0.
eval $(opam env)$again to update the shell environment.
- Download Hello.v, the hello world file.
- Compile Hello.v (
coqc Hello.vfrom the command line) to test your Coq setup.
Hello.vin CoqIDE (
coqide Hello.vfrom the command line), and step to the bottom to check your CoqIDE setup.
- 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.
You can find the exercise we will do together in class below.