Exercises for Week 04

You are expected to use your quota of time dedicated to LPP this week to solve as many exercises as possible, and then stop. Three words of advice:

0. interleave the writing of your .v file and of your .pdf file: as soon as you have completed a proof in the .v file, report it in your .pdf file; this way, when your time quota for the week is about to be reached, you can write the introduction and the conclusion in the report and be done;
1. the .v file, in your handin, should not contain admit. / Admitted. if at all possible; and
2. the .pdf file, in your handin, should be as concise as humanly possible: if a proof is routine, just say so; and if a eureka lemma is required, just explain this requirement; in particular, there is no need this week to provide more than one informal proof and compare it with one of your formal proofs.

Reminder: A commented code listing does not a report make. And the .pdf file should be understandable without reading the .v file.

Exercise 00

1. The index of concepts for this week is in a separate chapter. Peruse it and make sure that its entries make sense to you (otherwise, click on them to check them out).
2. The lecture notes start with updates (Chapter Updates). Make sure to check them out regularly, as they reflect the development of the lecture.
3. Do take the time to peruse the lecture notes of this week and to reproduce their technical content.
4. Summarize your current understanding of the tutorial about fold-unfold lemmas.

Standard mandatory exercise

• Exercise 00: reflecting on the material of this week

Mandatory exercise in the form of a mini-project

• Exercise 18: about a predicate deciding whether two trees are mirror of each other

Remaining mandatory exercises, modulo your time quota for LPP this week

As many of the exercises in Chapter Reasoning about arithmetical functions as you have the time for.

Do make sure to prove at least one interesting property of addition and multiplication

• where both addition and multiplication are defined recursively,
• where addition is defined recursively and multiplication is defined tail recursively with an accumulator,
• where addition is defined tail recursively with an accumulator and multiplication is defined recursively, and
• where both addition and multiplication are defined tail recursively with an accumulator.

This way, you will build an informed appreciation of the costs and benefits of accumulators, and you will be in position to document this appreciation in your report.

Warning

The goal of these exercises is to practice, practice, and practice,

not to avoid practice by proving properties as corollaries of other properties.

Morpheus: Stop trying to be smart and be smart!

Version

Created [09 Feb 2024]