Les définitions de fonction par filtrage de motifs permettent de définir des fonctions de manière claire et concise. Dans les assistants preuves basés sur la Théorie des Types, elles permettent également d'effectuer des raisonnements par cas et par induction.
Cependant, la précision apportée au typage par les types dépendants rend certains cas inutiles dans des définitions par filtrage de motifs. La détection de ces cas inutiles est indécidable et le système Coq oblige l'utilisateur à présenter un traitement pour chacun des motifs, ce qui peut encombrer les preuves et les programmes par du code inutile.
Nous présentons une méthode permettant de détecter et de réfuter certains cas inutiles en sur-approximant des ensembles de termes habitant des types inductifs ou des contextes.