Stream: Coq users

Topic: Rewrite a match


view this post on Zulip 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 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? :)

view this post on Zulip 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