Blog

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

`inversion_ex3`

`apply_exercise`

`beq_nat_sym`

`beq_nat_trans`

`filter_exercise`

`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.