Stream: Coq users

Topic: ✔ Simplify case analysis: combine similar cases into one

view this post on Zulip Matthis Kruse (Aug 05 2023 at 09:49):

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

view this post on Zulip Notification Bot (Aug 05 2023 at 09:49):

Matthis Kruse has marked this topic as resolved.

Last updated: Oct 08 2024 at 15:02 UTC