This is the doc of seq, use it!

Exercise 1:

  • 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

save script