Project 1 - Program Equivalence

The objective of this project is to gain some familiarity with program equivalence by working some problems from Pierce. Prove the following theorems and turn in your Rocq source:

1. Exercise: 2 stars, standard (skip_right)
2. Exercise: 2 stars, standard, especially useful (if_false)
3. Exercise: 3 stars, standard (swap_if_branches)
4. Exercise: 2 stars, standard, especially useful (while_true)
5. Exercise: 2 stars, standard, especially useful (assign_aequiv)
6. Exercise: 3 stars, standard, optional (CSeq_congruence)
7. Exercise: 3 stars, standard (CIf_congruence)

I would prefer you do your proofs by adding to the Equiv.v file. If you prefer extracting the proofs into your own file, that’s fine. However, it will be more difficult to get everything set up correctly.

Let me emphasize again that using LLMs is just fine as long as you tell me and submit your prompt file as a part of your solution.

Update: I deleted what was the 5th problem because it wasn’t a problem.