Résumé:
J'ai implanté dans Coq une tactique permettant de générer le principe
d'induction correspondant à une fonction. Ce principe reproduit les
mêmes analyses de cas et récurrence que la fonction. Elle a été
utilisée sur des preuves du projet Certicarte dans lequel il est fait
un usage intensif de fonctions compliquées (26 cas...). Pour la pub
disons que le gain de taille des scripts va jusqu'à un facteur 10.
Pour l'instant ce travail est disponible sous la forme d'une tactique, mais à court terme il y aura aussi une commande du genre:
Functional Scheme find := f.
qui déclarera le principe automatiquement.
Pour ceux qui connaissent, ceci est très similaire à ce que Konrad Slind présente dans sa thèse, sauf qu'il s'agit de construire un terme de preuve pour ce principe.
Paradoxalement le travail s'en trouve plutôt facilité: pour générer le principe (sa preuve en fait) il suffit de prendre le corps de la fonction, de modifier quelques annotations de type, de remplacer les "bouts" des branches des cases par des obligations de preuve reprenant les mêmes appels récursifs que la fonction et le tour est joué (à l'aide de la tactique Refine).
Je présenterai cette tactique par une petite démo, suivi d'une courte explication plus précise des modifications permettant de passer de la fonction au principe d'induction. Je terminerai en proposant quelques améliorations possibles.
Retour au sommaire / Back to schedule