# Simplify proofs with neested pattern matching

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

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.