More Exercises

Boolean_functions

Use the knowledge taught so far to solve the theorem:

Identity_fn_applied_twice (f: Bool/ -> Bool/) (e: (x: Bool/) -> Equal/ Bool/ (f x) x) (b : Bool/) : Equal/ Bool/ (f (f b)) b
Identity_fn_applied_twice f e b = ?

Then, solve the negation_fn_applied_twice theorem, which is the same as the previous one, but changing the hypothesis to Equal (f x) (Not x)

Andb_eq_orb

Prove the following theorem (Remember that you can prove intermediate theorems separately):

Andb_eq_orb (b: Bool/) (c: Bool/) (e: Equal/ Bool/ (Andb b c) (Orb b c)) : Equal/ Bool/ b c
Andb_eq_orb b c prf = ?

Binary

Consider a different representation of natural numbers using a binary system instead of unary. That is, instead of having only zero or one successor of a number, we can have:

  • zero;
  • twice a number;
  • twice a number plus 1.
  1. First, write an inductive definition of this type, calling it Bin. (Remember that, in essence, the definition of Nat as zero or succ n has no intrinsic meaning. It only says that an element of Nat can be a zero or a succ n if n is also Nat. The interpretation of this as a system of values 0, 1, 2, etc., comes from how we work with this type Nat. Your definition of Bin ideally will be as simple as well. It will be the functions you make on Bin that will give mathematical sense to it).
  2. Then write an Incr function to increment a Bin, and a Bin_to_nat function to convert from Bin to Nat.
  3. Write five proofs that test your increment and conversion functions. Note that incrementing a binary and then converting it should result in the same result as converting it first and then incrementing the Nat.