Software Foundations：如何从grade中提取letter实现grade_comparison

你尝试的记录式访问（.(l)/.(letter)）无法生效，是因为用Inductive定义的构造子不会自动生成投影函数——只有Record类型才会默认生成这类访问器。无需定义额外的get_letter函数，直接通过模式匹配就能提取grade中的letter参数。

直接在模式匹配中提取letter实现grade_comparison #

假设letter_comparison的类型为letter -> letter -> comparison（比如返回Ordering或自定义的比较结果类型），你可以这样实现grade_comparison：

(* 补全基础类型定义示例 *)
Inductive letter : Type := A | B | C | D | F.
Inductive modifier : Type := Plus | Minus | Neutral.

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

(* 假设已存在的letter_comparison函数 *)
Definition letter_comparison (l1 l2 : letter) : comparison :=
  match l1, l2 with
  | A, A => Eq | A, _ => Gt
  | B, A => Gt | B, B => Eq | B, _ => Gt
  | C, A | C, B => Gt | C, C => Eq | C, _ => Lt
  | D, A | D, B | D, C => Gt | D, D => Eq | D, F => Lt
  | F, F => Eq | F, _ => Lt
  end.

(* 核心实现：直接解构grade提取letter *)
Definition grade_comparison (g1 g2 : grade) : comparison :=
  match g1, g2 with
  | Grade l1 _, Grade l2 _ => letter_comparison l1 l2
  end.

临时提取单个grade的letter（无需定义函数） #

如果只是在Compute中临时提取某个grade的letter，可以用匿名模式匹配：

Compute letter_comparison
  (match Grade C Plus with Grade l _ => l end)
  (match Grade B Plus with Grade l _ => l end).

这种方式直接通过模式匹配解构Grade构造子，一步拿到内部的letter参数，完全不需要额外定义get_letter函数，符合练习要求的分情况分析逻辑。

内容的提问来源于stack exchange，提问作者user21829651