Defining and Reasoning About General Recursive Functions in Type Theory: a Practical Method

We propose a practical method for defining and proving properties of general (i.e., not necessarily structural) recursive functions in proof assistants based on type theory. The idea is to define the graph of the intended function as an inductive relation, and to prove that the relation actually represents a function, which is by construction the function that we are trying to define. Then, we generate induction principles for proving other arbitrary properties of the function. The approach has been experimented in the Coq proof assistant, but should work in like-minded proof asistants as well. It allows for functions with mutual recursive calls, nested recursive calls, and works also for the standard encoding of partial functions using total functions over a dependent type that restricts the original function's domain. We present simple examples and report on a larger case study (sets of integers represented as ordered lists of intervals) that we have conducted in the context of certified static analyses. \\ Nous proposons une approche pratique pour définir et prouver des propriétés de fonctions récursives générales (i.e., non nécessairement structurelles) dans des assistants de preuve basés sur la théorie des types. L'idée principale est de définir le graphe de la fonction en cours de définition comme une relation inductive, et de prouver que cette relation représente une fonction qui est, par construction, celle qu'on essaie de définir. Ensuite, nous définissons des principes d'induction qui permettent de prouver des propriétés quelconques sur la fonction. Nous avons expérimenté l'approche dans l'assistant de preuve Coq. Cependant, elle devrait fonctionner dans d'autres systèmes basés sur la théorie des types. L'approche permet de traiter des appels mutuellement récursifs et/ou imbriqués, ainsi que des fonctions partielles via le codage standard par des fonctions totales au type dépendant qui restreint le domaine de définition. Nous présentons des exemples simples ainsi qu'une étude de cas plus complexes (le codage d'ensembles d'entiers par des listes d'intervalles) que nous avons menée dans le contexte du développement d'analyses statiques certifiées