Exercises for Week 04

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. What is the Light of Inductil and what is it good for?

Mandatory exercises

• Exercise 00: reflecting on the material of this week
• Exercise 01: revisiting the binomial expansion at rank 2
• Exercise 08: are the two specifications of addition equivalent?
• Exercise 09: as specified, is addition associative?
• Exercise 12: are the specifications of mirror, number_of_leaves, and number_of_nodes ambiguous? (if time is too short, only consider two of these specifications, or even one, your choice)

Optional exercises

• Exercise 02: revisiting a first bit of food for thought from Week 01
• Exercise 03: revisiting a second bit of food for thought from Week 01
• Exercise 11 from Week 02: revisit this exercise, this time with proofs, using the accompanying file

Exercise for the overachievers (which means you, I mean, like, right, you right here you)

• Exercise about ternary trees: figuring out a relation between the number of leaves and the number of nodes in a ternary tree and proving it

Halcyon: I think that Mimer wants the gift of our time.

Pablito: Right. He does, doesn’t he.

Bong-sun: At least we are his students.

Mimer: Harrumph.

Dana: Cheer up, Mimer, it was not embarrassing at all.

Mimer: Twas...

Bong-sun: OK. Maybe a little bit.

Anton: Er, guys? What happened?

Alfrothul: Not much.

The fourth wall: You had to be there.

Exercise about ternary trees

Here is a declaration for ternary trees with payloads in the leaves:

Inductive ternary_tree (V : Type) : Type :=
  Leaf3 : V -> ternary_tree V
| Node3 : ternary_tree V -> ternary_tree V -> ternary_tree V -> ternary_tree V.

These trees are ternary because each node has three subtrees.

Surely there must be a relation between the number of leaves in a given ternary tree and the number of nodes in this ternary tree? Figure out this relation and prove it, using the accompanying file.

N.B.: Since the trees are ternary, each node has three subtrees and each induction proof has three induction hypotheses.

Resources

• The accompanying file (latest version: 10 Feb 2025).

Version

Added Exercise 11.m and Exercise 11.n in the accompanying file [10 Feb 2025]

Added Exercise 00.d and the exercise about ternary trees [07 Feb 2025]

Added Exercise 11 from Week 02 [08 Feb 2025]

Added Exercise 00.d and the exercise about ternary trees [07 Feb 2025]

Created [07 Feb 2025]