Project 3 - Decorated Programs

The objective of this project is to gain experience with decorated programs and loop invariants by working problems from Pierce. Complete the following exercises from Hoare.v and Hoare2.v and turn in your Rocq source:

1. Exercise: 2 stars, standard, optional (if_minus_plus_reloaded) from Hoare2.v
2. Exercise: 2 stars, standard (slow_assignment) from Hoare2.v
3. Exercise: 2 stars, standard (slow_assignment_dec) from Hoare2.v
4. Exercise: 4 stars, advanced (factorial_correct) from Hoare2.v

I would prefer you do your proofs by adding to the Hoare.v and/or Hoare2.v files. 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.

As with previous projects, using LLMs is fine as long as you tell me and submit your prompt file as part of your solution.