The Coq mailing list

[Blaudeau Clément <clement.blaudeau AT polytechnique.edu>]

Hi Everyone,
I'm currently working to prove results on a fonction that uses several 
levels of nested pattern matching and it generates *a lot* of trivial 
subgoals, to the point that every proof takes several minutes to go through.

##### High level view of the problem

I have an inductive type with ~ 50 constructors, and nested pattern 
matching on lists of that type. The nested pattern matching is 
translated into several levels of normal pattern matching with one case 
that is interesting and 49 useless cases. To build proofs on my 
function, I would like to be able to extract easily the interesting 
cases, and quickly drop all useless cases. Is there automated ways of 
doing that ? Just destruct the match expressions and using `congruence` 
is too slow.

##### More details

I have a function  `is_valid : A -> bool`, and I want to prove results 
of the form `is_valid a = true -> P`, where `A` is an inductive type of 
the form
```Coq
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
```Coq
| 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 for any property P, but I'm 
looking for an automated way of doing it

--
Clément Blaudeau
clement.blaudeau AT polytechnique.edu

--
Clément Blaudeau
0646116755
clement.blaudeau AT polytechnique.edu