Logic, Programs & Verification

Standard Exercises

• Basics.v: All 1 star (10 total) and 2 star (7 total) exercises
• Induction.v: All 2 star (9 total) exercises
• Lists.v: All 1 star (7 total) and 2 star (5 total) exercises
• Poly.v: All 1 star (3 total) and 2 star (11 total) exercises
• Tactics.v: All 1 star (2 total) and 2 star (5 total) exercises
• Logic.v: All 1 star (10 total) and 2 star (12 total) exercises
• IndProp.v: All 1 star (8 total) and 2 star (8 total) exercises before the final extended exercise
• ProofObjects.v: All 1 star (4 total) and 2 star (10 total) exercises
• IndPrinciples.v: All 1 star (6 total) and 2 star (3 total) exercises
• Rel.v: All 1 star (3 total) and 2 star (9 total) exercises

Advanced Exercises

• Induction.v: All 3 star (4 total) exercises
• Lists.v: All 3 star (7 total) exercises
• Poly.v: All 3 star (6 total) exercises
• Tactics.v: All 3 star (10 total) exercises
• Logic.v: All 3 star (7 total) exercises
• IndProp.v: All 3 star (8 total) exercises before the final extended exercise

Extra Challenges

• Induction.v: The 4 star exercise bin_nat_bin
• Logic.v: The 5 star exercise classical_axioms (no using auto!) bonus: see how many direction you can do without using exfalso or inversion
• IndProp.v: The 4 star exercise subsequence
• IndProp.v: The 4 star exercise re_not_empty
• IndProp.v: The 5 star exercise weak_pumping or pumping (only need to do one, only one counts)
• IndProp.v: The 4 & 5 star exercises filter_challenge and filter_challenge_2
• IndProp.v: The 4 & 5 star exercises palindrome and palindrome_converse
• IndProp.v: The 4 star exercise NoDup (be sure to specify and prove a few properties)
• IndProp.v: The 4 star exercise pigeonhole_principle
• IndProp.v: The extended exercises (8 total) on a verified regular expression matcher

Choose Your Own Adventure!

Some students will have previous experience with functional programming, some with formal mathematical proofs, and some will be completely new to the area. For that reason, everyone will get their own choice of which exercises to tackle throughout the semester.

The summary is that you will have to complete 10 things by the end of the semester. What is a "thing?" A set of exercises from one of the chapters of Software Foundations. The exercise sets will come in three different groups of increasing difficulty:

1. Standard: All of the 1 star and 2 star exercises of a chapter, some of which we will do together in class.
2. Advanced: All of the 3 star exercises of a chapter.
3. Challenge: A single, select 4 star or 5 star exercise.

When in doubt, stick with the Standard exercises for the chapters we cover in class. If those become too easy, try your hand at some Advanced exercises. If you have success with those, and see a Challenge problem that piques your interest, feel free to have a go.

There are also many more chapters and books to the Software Foundations series covering other, specialized topics. If one of those are of interest to you, talk to the professor to pick some exercises to work on, since explicit permission is needed if you go outside the scope of the in-class lectures. Otherwise, there are some exercise sets listed above that have been pre-approved for you.

Mechanical vs Prosaic

Both traditional "pen-and-paper" proofs written in natural human language and the newer machine-checked proofs written in a formal programming language have their own advantages and disadvantages. On the one hand, traditional proofs are written in a prose style that fits well with the human's understanding of the problem and elides obvious details. However, many students first learning this style have difficulty understanding what is really necessary to say, what is obvious or not, and whether the statements made have any meaning at all. On the other hand, machine-checked proofs are written using a formally rigorous and structured language that removes any ambiguity, and whose correctness can be automatically confirmed. However, the level of detail can make it easy to miss the forest for the trees, and the inflexible structure can overshadow the bigger-picture idea that is more useful to humans than computers.

That's why, in this class, you will be writing both styles of proofs for the same exercises. To fully complete a given set of exercises requires two parts:

1. for all the exercises, write the proofs formally in Coq as stated in Software Foundations, and
2. for half the exercises rounded up, write an accompanying informal proof in English prose.

That means there will always be at least one informal English proof, even for a one-question Challenge exercise. The informal proof may be done in comments next to the formal proof in the same file, or they may be gathered in a separate file. Either way, be sure to document where these may be found in a way that someone else can find them (see below).

To have the best success in class, the formal and informal proofs should be seen as complementary parts of the same thing as opposed to two separate and unrelated tasks. As the exercises become more challenging, here is a suggested workflow that integrates both formal and informal aspects to harness their complementary strengths:

1. Start with some introductory tactics in the formal proof (like intros and induction) to let the computer guide the overall structure of the proof. For example, what cases do you have, and what do your induction hypotheses look like in each case.
2. Begin an informal proof with that same structure, and in each case, convince yourself why that case should be true. You can hand-wave over some of the more obvious details, and instead focus on the essential challenge of why the case is correct. Sometimes this is trivial. Sometimes you have to just apply the inductive hypothesis. Sometimes you need to use a previous fact already proved before.
3. Having informally convinced yourself, you now need to convince the computer. Try to use the intuitive reason why each case is correct to guide your tactics in Coq. There may be some additional symbolic manipulation that needs to happen inbetween steps in your informal proof to connect the gaps.
4. Finally, after finishing the formal proof, look back at your informal proof to check for mistakes. Did you forget an important step that was worth explaining to antoher person? Was one of your assumptions or conclusions actually incorrect?

If you follow this plan for the more challenging exercises, then you will end up with both formal and informal proofs in the same time it takes to just do one on its own. It is easy to write a wrong English proof, but the computer won't be convinced. It is easy to spend all day spamming Coq tactics until you get to Qed without understanding what is going on.

Repository

Using version control is good practice whenever you have some code or text that evolves over time. By the end of the semester, you must turn in all your work in the form of a single git repository holding all of your solutions. This can be shared with the professor either via email or a PRIVATE github repository (to avoid plagiarism).

Progress

At the beginning of the semester, you should start by creating an initial git repository with the entire Logical Foundations book source files. As you work on exercises, commit your partial progress at regular intervals. In fact, committing incomplete, and even incorrect, throughout the semester is highly encouraged as a way to "show your work." These will provide valuable hints for feedback mid-semester, and only the final solutions at the end will be graded. There will never be a penalty or negative judgement for mistakes made along the way.

Documentation

To help another person (i.e., the grader) find your work, you need to properly document what you did. The top-level of your repository must have a README file that lists what exercises you did, and in what files to find your formal Coq proofs and informal English proofs. This list should look like the following example, which includes a numbered list of each exercise set completed and which files the formal and informal proofs can be found:

1. All 1 and 2 star exercises from Functional Programming in Coq
   * Formal: Basics.v
   * Informal: Basics.v
2. All 3 star exercises from Proof by Induction
   * Formal: Induction.v
   * Informal: Induction.md
3. 4 star exercise bin_nat_bin
   * Formal: Induction.v
   * Informal: Bin.pdf

WARNING: anything not listed in this README file will not be looked at, and not be graded. If your repository has no README documenting what was done, then the grade is automatically 0.