Class 12: Custom Tactics in Ltac

For the tenth class, we are going to dive into the StructTact library! This library contains the "structural tactics" that we read about for Tuesday's class, in Planning for Change. This is again implemented on top of Coq, so if you missed the artifact from two weeks ago, I recommend installing it and playing around with it first.

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.

Installation Instructions

Please follow these instructions, which are adapted from the StructTact README:

1. Run eval $(opam env) to sync your opam environment.
2. Run git clone https://github.com/uwplse/StructTact.git to clone the StructTact repository.
3. Run cd StructTact && make && make install to build and install StructTact.
4. Download this file, and open it and step through it in CoqIDE to make sure it works.

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.

During class, we will again divide up into groups. We will then do the exercise in this file. You can do this on your own if you cannot make it to class, or enter a Zoom breakout if you're remote. Let me know if you can't attend, but would 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.