## Stream: Coq users

### Topic: Rewrite a match

#### Matthis Kruse (Aug 03 2023 at 06:38):

I'm wondering about an ergonomic and efficient way to reduce the following goal:

``````match e with
| Value v => Some a(v)
| _ => Some(b e)
end = Some c
``````

The list of assumptions contains a proof that `e` is not a value, i.e., `forall v, e <> Value v`.
What I want the goal to change to is:

``````Some(b e) = Some c
``````

Previously, I resolved this the obvious way: `destruct e` and contradict. Unfortunately, this generates `n` goals, where `n` is the number of shapes an expression can have without being classified as a value.
This has led to rather serious performance issues due to nested matches where I get at worst `n³` goals.
So, I want to somehow rewrite this but so far, without luck.
I tried with a lemma like:

``````Lemma getrid_of_matchval { A : Type } (P : A -> Prop) e (a b : A) :
~ is_value e ->
P b ->
P(match e with
| Value _ => a
| _ => b
end)
.
``````

And then `change` my goal to `(fun x => ...) (match e with ... end)`, trying to apply `getrid_of_matchval`.
But, Coq fails to unify.

What's the trick? :)

#### Matthis Kruse (Aug 03 2023 at 07:05):

I managed to at least get the rewrite through by patching the definition of `getrid_of_matchval` and by rewriting the goal even further, i.e., match arms also need to be of the form `(fun x => ...) e`
The updated version of `getrid_of_matchval` looks as follows:

``````Lemma getrid_of_matchval { A : Type } (P : A -> Prop) (e : expr) (a : value -> A) (b : expr -> A) :
~ is_val e ->
P(b e) ->
P(match e with
| Value v => a v
| _ => b e
end)
.
``````

So, now, my question is more about ergonomics instead of efficiency, given I found a solution that works. But, I'd still appreciate pointers to (semi-)automate rewriting the goal, not having to write out the `change` explicitly would be nice

Last updated: Jun 22 2024 at 16:02 UTC