Imp and IndProp

Excercises I will grade from Imp.v and IndProp.v are listed below. You can do more if you want and I will grade them, but this is what I will definitely incldue:

IndProp.v

Most of these are 1 star with a few more difficult proofs at the end. No 4 or 5 star proofs. I’m not asking you to prove The Pumping Lemma even though Pierce would.

• close_refl_trans
• perm
• ev_double
• inversion_pactice
• ev5_nonsense
• ev_sum
• ev'_ev
• ev_ev__ev
• ev_plus_plus
• total_relation
• empty_relation
• subsequence
• reflect

Imp.v

The Imp.v chapter doesn’t have too many truly 1 star problems. Set aside some time to work on these, but none of them are horrible.

• optimize_0plus_b_sound
• optimize (4 star, so be careful)
• bevalR
• ceval_example2
• loop_never_stops
• no_whiles_eqv
• stack_compiler (particularly cool)