I'm running through logic foundations and during the lower_grade_lowers
exercise, Coq is behaving in a way that I wouldn't expect.
I have the following goal:
grade_comparison match l with
| A | _ => Grade l Natural
end (Grade l Plus) = Lt
This, to me, feels like it should simplify: the | A | _ => ...
branch is not falsifiable, and I would expect Coq to simplify the whole thing to:
grade_comparison (Grade l Natural) (Grade l Plus) = Lt
This does not happen, and I do not understand why...
Grade l Natural
is guarded behind a match; did you try runningdestruct l.
at this point?