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.

Exercise 1:

  • Extend the definitions introduced in Lesson 6, so that the proof of the test1 lemma succeeds without changing the proof script.

Exercise 2. We define a type tuple for polymorphic lists with a prescribed length, given as a parameter. This type is a dependent pair. This condition is expressed as a (boolean) constraint on the size of a list, coerced to Prop via the usual is_true coercion. The infix == notation refers to the notation available on instances of the eqType structure, as defined by the library loaded in this section. This structure is isomorphic to the one we used in Lesson 6. In particular, it is endowed with a reflection lemma eqP, relating the boolean test with equality.

Fill the missing parts so that the test lemmas are proved without changing their script.