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? :)

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