软件基础基础 - 定理 lower_grade_lowers 需要证明蕴涵 Eq = Lt -> Eq = Lt

Question

我正在独自完成软件基础，并且陷入了lower_grade_lowers的最后一个项目。我的定理很好地遵循了提示，直到最终的情况，这显然是问题的症结所在，但我不会发布示例，因为它用于家庭作业。我的问题是子目标的情况：

grade_comparison (Grade F Minus) (Grade F Minus) = Lt ->
grade_comparison (lower_grade (Grade F Minus)) (Grade F Minus) = Lt

grade_comparison 是返回归纳法的定义

Inductive comparison : Set :=
  | Eq : comparison        (* "equal" *)
  | Lt : comparison        (* "less than" *)
  | Gt : comparison.       (* "greater than" *)

按照帮助注释中的建议使用 lower_grade_F_Minus 然后进行简化，我得到一个似乎应该很容易证明的命题。要么

grade_comparison (Grade F Minus) (Grade F Minus) = Lt ->
grade_comparison (Grade F Minus) (Grade F Minus) = Lt

或简化

Eq = Lt -> Eq = Lt

鉴于条件条件的前提总是假的，证明这个命题似乎微不足道，但是从网上搜索如何在策略中实际写出这个命题来看，这听起来只能用直觉命题演算来覆盖，而直觉命题演算还没有被证明。文本中的这一点已涵盖，所以看起来我的方法超出了文本，我错过了一些东西。

有没有一种更简单的方法来证明一个前提错误的命题总是正确的，仅使用介绍、解构、简化、重写和反身性（这是迄今为止所涵盖的唯一策略）？

Answer 1

自然地，当我发布这个问题时，我会重新阅读之前的示例并过度思考这个问题。只需使用假设进行简单重写即可将蕴涵转化为微不足道的等式，并且评分者会接受该解决方案。