To play this document inside your browser use ALT-N and ALT-P.

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.

Exercise 1:

  • look for lemmas supporting contrapositive reasoning
  • use the eqP view to finish the proof.

Exercise 2:

  • 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 3:

  • Prove this view by unfolding maxn and then using leqP

Exercise 4:

  • 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

Exercise 5:

  • Prove some reflection lemmas for the proposed reflect definition

  • A possible definition for reflect

Exercise 6:

  • Get excluded-middle when P is equivalent to a bool decidable

    • Equivalence definition

    Exercise 7:

    • Let's use standard reflect (and iffP, idP etc...)

    Exercise 8:

    If you have time.. more reflections

  • leq_max : use leq_total maxn_idPl
  • dvdn_fact: use leq_eqVlt dvdn_mulr dvdn_mull

    • For this section: only move=> h, move/V: h => h, case/V: h, by ... allowed

    No case analysis on b, b1, b2 allowed

    No xxxP lemmas allowed, but reflectT and reflectF and case analysis allowed ,

    Some arithmetics