Tactics for pattern matching?

Using Coq
1

Hello,

Is there a way to tell Coq to rewrite a goal/hypothesis of the form

f (match e with p1 => e1 | ... | pn => en end)

by

match e with p1 => f e1 | ... | pn => f en end

?

Similarly, is there a way to get Coq to rewrite

match e with p1 | ... | pn => e' end

simply by

e'

?

When reasoning with functions defined using Fixpoint which contain nested pattern matching, I find myself doing a lot of destruct e in order to achieve the same effect, which is tedious and repetitive.

Any additional advice on reasoning about match ... with is welcome. Thanks!

Cheers,
Nicolás

2

Hey, sadly I don’t think there is, but I would be happy to be proven wrong!
I was personally in a very similar situation when working on a project and here is what I ended up writing: ssprove/pkg_user_util.v at 95fb84d7d653b6b67f307b18e89480ea64577718 · SSProve/ssprove · GitHub

I create a fresh evar and replace the subterm with it, and then I apply a tactic which traverses the term and does the destruct e you suggested, except, it does it only when proving the equality! This means that in the end you will still have a goal with match e with ... end.

If you don’t have to go under binders, then you don’t need something as complicated as I have.

Regarding

match e with p1 | ... | pn => e' end

another option might be to try to avoid this situation, for instance by using views when defining functions. As explained in the Equations’s examples: Examples.views

3

Thanks for the reply @TheoWinterhalter ! I will give it a look. Out of curiosity, do you know if it would be possible to implement these kinds of rewritings as a custom tactic in an OCaml plugin?

Cheers!
Nicolás

4

I have never written such plugins, but it might be easier than in Ltac1. Other people will know better than me.