EECS 755

Software Requirements Modeling and Analysis


Project 3

Work the following exercises from the chapter Tactics: More Basic Tactics:

  1. inversion_ex3
  2. apply_exercise
  3. beq_nat_sym
  4. beq_nat_trans
  5. filter_exercise
  6. forall_exists_challenge

The filter_exercise is marked as challenging. It is, but it is quite doable. The forall_exists_challenge will be your first time verifying a function you write. Pay attention to the structure of the problem as well as the proofs themselves.

Submit your Project 3 proofs and definitions via blackboard. It is important that you use the theorem names as defined in the text. Feel free to add and prove any lemmas you feel are useful, but keep the names of the theorems in order and the same.