# How to simplify single-branch match expressions?

**URL:** <https://discourse.rocq-prover.org/t/how-to-simplify-single-branch-match-expressions/2243>\
**Category:** Using Rocq\
**Tags:** software-foundations\
**Created:** [April 6, 2024, 2:11pm UTC](https://discourse.rocq-prover.org/t/how-to-simplify-single-branch-match-expressions/2243 "2024-04-06T14:11:19Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![dragazo](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/dragazo/32/954_2.png) [@dragazo](https://discourse.rocq-prover.org/u/dragazo)\
**Post date:** [April 6, 2024, 2:11pm UTC](https://discourse.rocq-prover.org/t/how-to-simplify-single-branch-match-expressions/2243/1 "2024-04-06T14:11:19Z")

</div>

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:

```auto
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](https://stackoverflow.com/questions/76916890/force-coq-to-simplify-unfalsifiable-pattern-matches)), 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.

---

<div class="post-metadata">

**Author:** ![silene](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/silene/32/485_2.png) [@silene](https://discourse.rocq-prover.org/u/silene)\
**Post date:** [April 7, 2024, 4:06am UTC](https://discourse.rocq-prover.org/t/how-to-simplify-single-branch-match-expressions/2243/3 "2024-04-07T04:06:43Z")

</div>

> [@dragazo](#):
>
> Is there any way to force this expression to simplify?

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.)

---

<div class="post-metadata">

**Author:** ![dragazo](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/dragazo/32/954_2.png) [@dragazo](https://discourse.rocq-prover.org/u/dragazo)\
**Post date:** [April 8, 2024, 3:17pm UTC](https://discourse.rocq-prover.org/t/how-to-simplify-single-branch-match-expressions/2243/4 "2024-04-08T15:17:09Z")

</div>

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](https://github.com/coq/coq/issues/18912)