Exercises for Week 09

Exercise 00

1. The index of concepts for this week is in a separate chapter. Go through them and make sure that they make sense to you.
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 in a personal session with tCPA.
4. Summarize your understanding of using ; instead of . after invoking a tactic.

Mandatory exercises

• Exercise 00: reflecting on the material of this week
• Exercise 01: proving the sketchy characterization of list map
• Exercise 02: instantiating the sketchy characterization of list map
• Exercise 03: proving the sketchy characterization of list fold-right
• Exercise 04: instantiating the sketchy characterization of list fold-right
• Exercise 05: proving the sketchy characterization of list fold-left
• Exercise 06: instantiating the sketchy characterization of list fold-left

Exercises from Week 08

• Exercise 00: reflecting on the material of this week
• Exercise 06: formalizing a proof of Euclid’s division lemma
• Exercise 07: formalizing a proof of an alternative version of Euclid’s division lemma
• Exercise 09: proving a corollary of (either version of) Euclid’s division lemma

Exercises from Week 07

• Exercise 00: reflecting on the material of this week
• Formalize and prove that the product of two consecutive natural numbers is even. How does your formal proof compare to your informal proof?
• Exercise 33: pondering about the arc from Exercise 21 to Exercise 32 and beyond

Version

Added Exercise 00 from Week 07 and Exercise 00 from Week 08 [19 May 2025]

Added the exercises [22 Mar 2025]

Created [21 Mar 2025]