Simplify proofs with neested pattern matching

Using Coq
1

Hi Everyone,
I’m currently working to prove results on a fonction is_valid : A -> bool of the form is_valid a = true -> % some property, where A is an inductive type of the form

Inductive A := | N : B -> (list A) -> A . % N is the only constructor

And B is also an inductive type with around 50 constructors.
The problem is that, in the is_valid function, I have nested pattern matching (on the list) like

| N b1 (N b2 [])::(N b3 [])::_ -> (f b1 b2 b3) % some property computed using b1 b2 b3

generates huge patterns, because the internal translation of nested patterns is to create several levels of patterns. As my type B has 50 constructors, each level of pattern matching generates a lot of subgoals and slows down the proofs.

Is there a simple way to say that if is_valid a = true then all the possible cases are only the ones of the main pattern matching, without having to break all sub-levels of matching using congruence everywhere ? Just doing an unfold of the is_valid function takes ~2 min on my computer. The dream would be that is_valid a = true -> P could be split into the few subgoals of the form (f b1 b2 b3) -> P

Thank you for your help !
Clément

PS: I could write a big theorem saying that, but I’m looking for an automated way of doing it

2

Would it work for you to define is_valid as an inductive type? You can have that as an alternative, or if you need a function then you can prove them equivalent once.
Also, are you using Program to define is_valid? Program makes definition even larger than they’d be, unless you use Unset Program Cases first.

If you’d matching only on the list, you shouldn’t get splits over the constructors of b. Are b1 b2 and b3 variables or constructors of b?

Because 2 minutes for an unfold sounds really bad. OTOH, I might use simpl rather than calling unfold, that’s probably faster.