Exercises for Week 09

Exercise 00

1. There are no new keywords or tactics this week.
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.

Mandatory exercises

• Exercise 08 in Week 07: implementing an equality predicate of type option bool * list unit -> option bool * list unit -> bool and elegantly proving its soundness and completeness
• Exercise 01: formalizing summations
• Exercise 02 implementing a tail-recursive summation function that uses an accumulator
• Exercise 03: formalizing 2-by-2 matrices

Optional exercises

• in Week 07, state Proposition C_is_nilpotent_with_order_??? for the isometries in the equilateral triangle, and prove it (a) using brute force and then (b) as a corollary of the two previous propositions
• Exercise 05: proving that the quotient and the remainder are unique in Euclid’s division lemma
• Exercise 07: implementing the Euclidean division using structural induction over the dividend

Version

Added Exercise 02 [24 Mar 2024]

Created [22 Mar 2024]