To play this document inside your browser use ALT-N and ALT-P. If you get stack overflow errors, try to use Google Chrome or Chromium with the command line option --js-flags="--harmony-tailcalls".

You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.

This is the doc of seq, use it!

• look up the documentation of take and drop
• prove this by induction (mind the recursive argument)

Exercise 2:

• look at the definition of take and size and prove the following lemma
• the proof goes by cases

Exercise 3:

• another proof by cases

Exercise 4:

• Look up the definition of rot
• Look back in this file the lemma cat_take_drop
• can you rewrite with it right-to-left in the right-hand-side of the goal?

Exercise 5:

• which is the size of an empty sequence?
• Use lemmas about size and filter

Exercise 6:

• prove that by induction

Exercise 7:

• prove that view (one branch is by induction)

Exercise 8:

• induction once more

Exercise 9:

• prove this by induction on s