Class 10: Reflection in Action

This class, we'll do an exercise on reflection in Coq. The exercise can be found in this file. Throughout, it is likely that you will find the demo file from Tuesday's class helpful!

Thanks again to our wonderful TA, there's a Gitpod link here! Otherwise, please follow the installation instructions below. Either way, please get the artifact running before class. If you have any trouble, please post your questions in this class forum 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.

Coming soon!

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.