coqlogical-foundations

Software Foundations Basics Exercise - How do I access letter from grade?


I am working through Software Foundations by myself and am trying the exercises, but I am stuck on the exercise for writing the function grade_comparison.

 Definition grade_comparison (g1 g2 : grade) : comparison
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

The definition of the type grade is given by

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

and we are given a function letter_comparison which takes two letters and returns if they are equal, or if one is greater or less than the other.

I want to apply the letter_comparison function to the letter portion of the two given grades since the instructions say to "do case analysis on the result of a suitable call to letter_comparison to end up with just 3 possibilities."

However, I am not sure how to call letter comparison correctly.

I have tried treating Grade as a record type,

(letter_comparison (Grade A Plus).(l) (Grade C Plus).(l))
(letter_comparison (Grade A Plus).(letter) (Grade C Plus).(letter))

but nothing I have tried so far compiles.

I can write a separate function that returns the letter from a grade

Definition get_letter (g : grade) : letter :=
    match g with 
    | Grade A _ => A
    | Grade B _ => B
    | Grade C _ => C
    | Grade D _ => D
    | Grade F _ => F
    end.

Compute ((letter_comparison (get_letter (Grade C Plus)) (get_letter (Grade B Plus)))).

However, I think there is a way to do this without having to define this function.


Solution

  • I also don't know of an alternative way to get the letter from the grade other than a simplified get_letter:

    Definition get_letter (g : grade) :=
      match g with Grade x _ => x end.
    

    I think this is more or less standard. For example, the pair type is defined similarly to grade and the way we obtain the first or second elements of the pair is through dedicated functions, fst and snd in this case.