Ok, I finally found a solution to this which turns out to be already employed a lot in e.g. mathcomp: views.

Just for reference, define:

```
(** view of expressions either being some expression or a value *)
Inductive expr_view : expr -> Type :=
| expr_view_value : forall (v : value),
expr_view (Value v)
| expr_view_expr : forall (e : expr),
(forall v, e <> Value v) ->
expr_view e
.
#[local] Hint Constructors expr_view.
Lemma e_view e : expr_view e.
Proof. destruct e; econstructor; congruence. Qed.
```

Then, whenever I have a definition that somewhere somehow contains

```
match e with
| Value v => ...
| _ => ...
end
```

I patch the originial definition to

```
match e_view e with
| expr_view_value v1 => ...
| _ => ...
```

And this allows me to do the case analyses in the proofs without this insane state explosion where I'd get (at worst) >1000 goals. :)

Matthis Kruse has marked this topic as resolved.

Last updated: Jun 13 2024 at 21:01 UTC