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

Question

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.

Answer 1

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.

Answer 2

I am struggling with this function as well, but Ana Borges's answer above demonstrated that you can parametrise constructors in the pattern-matching clause:

match g with Grade x _ => x end.

We can use this knowledge to solve the task without resorting to anything but pattern-matching:

Definition grade_comparison (g1 g2 : grade) : comparison :=
  match g1, g2 with
  | Grade l1 m1, Grade l2 m2 => 
    match (letter_comparison l1 l2) with
    | Eq => modifier_comparison m1 m2
    | not_eq => not_eq
    end 
  end.

This definition passes the examples right after the task just well. I still don't quite understand what "3 possibilities" mean though, so maybe this solution is not an intended one.