I’m slowly making my way through the Logical Foundations book - the first volume of Software Foundations. As with most theorem provers, the introductory chapter has you setting up your own inductive type for natural numbers and then proving different properties about the numbers.

At the end of the chapter the book has some optional exercise, which I’ve been doing as part of my learning and this is the first slightly more involved set of proofs I’ve had to write.

…

Lowering a grade actually lowers it

We need to prove the following theorem:

Theorem lower_grade_lowers :
  forall (g : grade),
    grade_comparison (Grade F Minus) g = Lt ->
    grade_comparison (lower_grade g) g = Lt.

Which can be read as for all grades g, if the value of g is strictly greater than an F-, then applying the lower_grade function to it, produces some g' which is strictly less than g.

To prove that we must perform a case analysis on the different grades we have. Recall that a grade is made up of 3 components:

Inductive grade : Type := Grade (l:letter) (m:modifier).

• Grade is the type constructor
• l is the letter component (A | B | C | D | F)
• m is the modifier (+ | natural | - )

Inductive letter : Type :=
  | A | B | C | D | F.

Inductive modifier : Type :=
  | Plus | Natural | Minus.

First, let’s destruct our grade into its constituent parts. In Rocq we can do that with match