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.