Project 4 - Small Step Semantics

1. Define a small-step semantics for a repeat loop that checks its loop condition after execution rather than before.
2. Define a theorem for proving the small-step semantics for plus equivalent to the large-step semantics.
3. Define a small-step semantics for assignment.
4. Define a small-step semantics for the sequence command.
5. Define a Rocq relation for small-step Imp evaluation.
6. Define a Rocq theorem that specifies when the small-step semantics is correct with respect to the natural semantics.
7. If you are brave, try to prove the previous theorem.