Exercise 1:

  • use no lemma to prove the following statement

Exercise 2:

  • look up what ==> is check if there are relevant views
  • prove that as you like

Exercise 3:

  • look for lemmas supporting contrapositive reasoning

Exercise 4:

  • what is (+) ?
  • find the right view to prove this statement
  • now find another proof without the view

Exercise 5:

  • it helps to find out what is behind ./2 and .*2 in order to Search
  • any proof would do, but there is one not using implyP

Exercise 6:

  • prove that using case:
  • then prove that without using case:

Exercise 7:

  • look up the definition of iter
  • prove this tatement by induction

Exercise 8:

  • look up the definition of iter (note there is an accumulator varying during recursion)
  • prove the following statement by induction

Exercise 9:

  • the only tactics allowed are rewrite and by
  • use Search to find the relevant lemmas (all are good but for ltn_neqAle) or browse the online doc
  • proof sketch: 
            m < n = ~~ (n <= m)
              = ~~ (n == m || n < m)
              = n != m && ~~ (n < m)
              = ...

Exercise 10:

  • there is no need to prove reflect with iffP: here just use rewrite and apply
  • check out the definitions and theory of leq and maxn
  • proof sketch: 
       n <= m = n - m == 0
          = m + n - m == m + 0
          = maxn m n == m

save script