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
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 !
PS: I could write a big theorem saying that, but I’m looking for an automated way of doing it