Use ALT-(up-arrow) and ALT-(down-arrow) to process this document inside your browser, line-by-line. Use ALT-(right-arrow) to go to the cursor. You can save your edits inside your browser and load them back. Finally, you can download your working copy of the file, e.g., for sending it to teachers.

maxn defines the maximum of two numbers

We define the maximum of three number as folllows

Try to prove the following facts (you may use properties of maxn provided by the library)

Exercise 1

Exercise 2

Exercise 3

Exercise 4

Exercise 5

The next exercise consists in proving an alternative induction scheme on type list, whose base case is the last element in the list.

For this purpose, we first define a concatenation operation between lists and prove a few lemmas about it.

The 'rcons' operation is provided by the underlying library, and appends its last argument to the end of its first, which is a list.

The exercise is self-contained : you should not use results that you did not prove yourself.

Definition of the concatenation operation

Exercise 5

Exercise 6

Exercise 7

Exercise 8

Exercise 9.

(Hint: this proof does not require an induction step)

Exercise 10.

Prove lemma last_ind using first the intermediate lemma hcat,

and then by induction. Hint: use the lemmas you have proved so far on function cat.