1

I'm working through Software Foundations on my own and am stuck on the final bullet for lower_grade_lowers. My theorem follows the hint pretty well until that final case which is obviously the crux of the problem but I'm not posting the example as it's used for homework assignments. My problem is the case with the sub-goal:

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

grade_comparison is a definition that returns the inductive

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

Using lower_grade_F_Minus as suggested in the help comments and then simplifying, I get a proposition which seems like it should be easy to prove. Either

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

or simplified

Eq = Lt -> Eq = Lt

Given the premise of the conditional is always false, it seems trivial to prove this statement, but from searching online for how to actually write this out in tactics, it sounds like this can only be covered by intuitionistic propositional calculus which hasn't been covered at this point in the text so it seems like my approach is getting ahead of the text and I missed something.

Is there a simpler way to show that a proposition with a false premise is always true using only intros, destruct, simpl, rewrite and reflexivity which were the only tactics covered so far?

PeterTN
  • 21
  • 3

2 Answers2

1

Naturally as soon as I post this question, I reread prior examples and was overthinking the problem. A simple rewrite using the hypothesis is all that's needed to turn the implication into a trivial equality and the grader accepts the solution.

PeterTN
  • 21
  • 3
  • As it’s currently written, your answer is unclear. Please [edit] to add additional details that will help others understand how this addresses the question asked. You can find more information on how to write good answers [in the help center](/help/how-to-answer). – Community Aug 27 '23 at 14:34
1

If assumption belongs to the set of allowed tactics in this exercise, the script intro H; assumption or intro H; exact H works fine.

Pierre Castéran
  • 791
  • 4
  • 5
  • `assumption` did not belong and exact hadn't been introduced yet. I believe `rewrite` using `H` was the intended tactic as in the solution for `plus_id_example`. – PeterTN Aug 24 '23 at 19:15