How to simplify single-branch match expressions?

Using Coq
1

I’m working my way through the software foundations book on my own, and I’ve gotten caught on the lower_grade_lowers exercise in Basics. Specifically, I’m struggling with one sub-expression that coq refuses to simplify:

match l with
  | A | _ => Grade l Natural
end

I don’t see why this expression would not simplify to simply Grade l Natural, at which point the solution becomes obvious. The only way I can see to proceed is to destruct l, but the problem’s hint specifically says that this should not be needed.

Is there any way to force this expression to simplify?

This problem was also phrased on stack exchange (functional programming - Force Coq to simplify unfalsifiable pattern matches - Stack Overflow), but I’m posting it here because it looks like no one ever responded to it.

Edit: I’ve discovered that changing the definition of the lower_grade function to use a different casing approach allows this simplification to happen, but I don’t understand why that would be required. The match expression shown above should just trivially reduce to Grade l Natural if it’s gotten that far.

3

No. There is no such rule in the logic of Coq. Just because one is able to prove that an expression reduces to another one does not mean that it always reduces to the other one. Indeed, the proof might be depending on a specific hypothesis and might no hold in the general case. (In your case, it is also true in the general case, but that is not easy to characterize.)

4

Well in general I would agree, but this just seems to be a bug in coq’s simplification logic. I’m checking with the coq team to see what they think: Single-branch match expressions not being properly simplified. · Issue #18912 · coq/coq · GitHub