Types inductifs

Ce chapitre décrit la théorie des types inductifs. Dans une première partie, nous nous intéressons aux définitions non récursives puis nous aborderons les définitions récursives. Dans ce document, pour simplifier les notations, les symboles ∀ et λ seront utilisés à la place des mots-clé de Coq forall et fun.

3.1 Généralités

3.1.1 Forme générale

Vocabulaire

Déclaration récursive

On dira que la déclaration est récursive si nom apparaît dans l’un des types d’argument de constructeur C_mⁿ. On dira qu’elle est non-récursive sinon.

3.1.2 Forme abstraite

Une déclaration inductive dans Coq introduit de nouveaux noms. Sur le plan théorique, il est parfois plus commode d’avoir une représentation abstraite des définitions inductives.

On ne garde alors que les éléments essentiels : l’arité A de la déclaration inductive et les types des constructeurs C_m. Dans le cas où il n’y a pas de paramètre, une notation possible pour la définition inductive est :

nom peut être vu comme un lieur dans la déclaration de l’inductif ce qui permet d’identifier des déclarations inductives isomorphes (même arité, même nombre de constructeurs avec les mêmes types d’argument).

Dans cette approche, si toutes les occurrences de nom dans les types d’arguments sont appliquées aux paramètres z₁,…,z_p alors les paramètres peuvent être vus comme des abstractions. On construit de nouveaux types de constructeur C′_k en remplaçant dans chaque type de constructeur C_k le terme (nom z₁… z_p) par le nouvel identificateur nom’ et on retrouve la définition inductive générale à l’aide des définitions suivantes.

Une déclaration inductive avec paramètres peut se voir comme une famille de définitions inductives.

3.2 Les déclarations non-récursives

Beaucoup des difficultés concernant les définitions inductives apparaissent déjà au niveau des définitions non-récursives que nous étudions en premier. Dans un premier temps, nous ne précisons pas la sorte de déclaration de la définition inductive. Nous considérons également des définitions inductives sans paramètres car ceux-ci ne jouent pas de rôle essentiel.

3.2.1 Les déclarations de base

Si on suppose que l’on a un Σ-type : Σ x:A.B avec deux projections : π₁ : Σ x:A.B → A et π₂ : (p:Σ x:A.B) B{x:=(π₁ p)} alors il est aisé de définir une somme n-aire :

avec un constructeur de type ∀ (x₁:A₁)…(x_n:A_n),Σ (x₁:A₁;…;x_n:A_n) et n projections π_k:∀ p:Σ (x₁:A₁;…;x_n:A_n),(A_k{x₁,…,x_k−1:=(π₁ p),…, (π_k−1 p)}. On notera (a₁,…,a_n) l’élément de Σ (x₁:A₁;…;x_n:A_n) défini à l’aide du constructeur. Cette somme se définit par récurrence sur n. On pose Σ()≡ Un, Σ(x:A)≡ A, et Σ (x:A;x₁:A₁;…;x_n:A_n)≡ Σ x:A.Σ (x₁:A₁;…;x_n:A_n).

De même on peut définir une disjonction n-aire A₁+⋯ + A_n comme étant Zero si n=0, A₁ si n=1 et dans le cas n>1 A+A₁+⋯ A_n ≡ A + (A₁+⋯ A_n).

À partir de ces constructions de base, on peut trouver un équivalent à toute définition inductive non récursive. En reprenant les notations données en 3.1.1 et en introduisant la notation Σ A pour Σ (a₁:A₁;…;a_n:A_n) avec A≡ ∀ (a₁:A₁)…(a_n:A_n),s l’arité de la définition inductive :

Exemple 1 Le type des booléens est équivalent à Un+Un.

Opérateurs primitifs, vs schéma général

On peut choisir d’introduire dans un formalisme les constructions de base (c’est le cas d’un système comme NuPrl ou dans des présentations catégoriques) ou bien introduire un schéma général de définition inductive. Le second choix permet d’utiliser l’uniformité des principes d’introduction et d’élimination des différents opérateurs. Il permet également de représenter de manière concise des propriétés qui nécessiteraient une imbrication profonde de connecteurs. L’introduction ou l’élimination de ces propriétés peuvent alors se faire en une seule étape ce qui permet d’avoir des preuves plus directes. Par contre, la généralité du schéma complique les raisonnements par cas sur la forme des définitions inductives : on ne peut pas juste traiter les cas Zero, Un, Σ-type, somme disjointe et égalité, il faut raisonner sur la structure interne des définitions inductives et traiter de manière générale des suites finies de termes ou de types; cela introduit une lourdeur à la fois au niveau de la programmation et de la présentation théorique.

Exemple 2 On suppose donné un type U:Set et un prédicat P:U→Prop. On se propose de définir une relation dec portant sur un booléen b tel que (dec b) soit vérifié si b=true et ∀ x:U,(P x) est prouvable ou bien si b=false et ∃ x:U,¬(P x) est prouvable.

On peut bien sûr introduire dec comme :

λ (U:Set) (P:U→Prop) (b:bool) ⇒

((∀ x:U,(P x)) ∧ b=true) + ((∃ x:U,¬ (P x)) ∧ b=false)

Mais on peut également introduire une définition inductive avec U et P comme paramètres.

Inductive dec (U:Set) (P:U→Prop) : bool → Prop
    isTrue : (∀ x:U,(P x)) → (dec U P true)
 |  isFalse : ∀ x:U,~(P x) → (dec U P false).

3.2.2 Règles de formation et d’introduction

Une déclaration inductive va introduire de nouveaux objets dans la théorie. Dans un cadre de déduction naturelle, on va trouver des règles d’introduction (une par constructeur) et des règles d’élimination. Il faut ajouter une règle de bonne formation pour la définition elle-même.

Règle de formation

En reprenant les notations de 3.1.1, la règle de formation donne le typage de la définition inductive. La condition est que chaque type de constructeur soit bien formé dans un environnement comportant les paramètres :

Cette règle impose un lien entre la sorte de l’inductif et celles des types d’argument de constructeur dans le cas où la sorte s est prédicative.

Exemple 3 On peut introduire Σ X : Prop,X de type Prop qui représente la propriété ∃ X.X (quantification existentielle du second ordre). Par contre Σ X : Type_i,X représente le type des types non vides et sera bien typé de type Type_i+1. Finalement dans un système avec Set prédicatif, le type Σ X : Set,X est forcément de type Type alors qu’il peut être de type Set, si cette sorte est imprédicative.

Règle d’introduction

Il y a une règle d’introduction par constructeur (donc pas de règle d’introduction pour le type inductif sans constructeur), la précondition est juste la bonne formation des types de constructeurs.

3.2.3 Schémas d’élimination

Les règles d’introduction nous disent comment former des objets dans une définition inductive. Les règles d’élimination indiquent comment utiliser un objet x:(nom u₁… u_l). Il y a plusieurs manières d’exprimer cette propriété.

Le schéma d’élimination minimal

L’interprétation usuelle des définitions inductives est que les valeurs (objets clos normaux) dans une instance de la définition inductive sont exactement ceux formés à partir des constructeurs.

Donc si on a un objet x dans la définition inductive (nom u₁… u_l) et que l’on veut montrer une propriété C, il suffit de regarder les cas où x=(co_m x₁… x_{n_m}) avec x_i quelconque du type approprié. Il suffit donc de montrer pour chaque m :

Cependant faire intervenir des n-uplets et l’égalité qui ne sont pas des notions primitives paraît peu intuitif (il faudrait commencer par préciser les règles pour ces deux types inductifs). Pour éviter cela, on peut intégrer le raisonnement égalitaire dans le schéma d’élimination.

On suppose que l’on a une propriété P de type ∀ (a₁:A₁)… (a_l:A_l),(nom a₁… a_l)→ s′. Pour prouver ∀ (a₁:A₁)… (a_l:A_l),(x:(nom a₁… a_l))(P a₁… a_l x), il suffit de montrer pour chaque constructeur co_m, la propriété :

On obtient donc le schéma d’élimination suivant qui est paramétré par la sorte s′ de la propriété à prouver :

Réduction

Comme toute règle d’élimination, celle-ci se combine avec les règles d’introduction pour former une réduction. Si la fonction d’élimination est appliquée au m-ième constructeur alors elle se réduit en la m-ème branche instanciée par les arguments du constructeur. On vérifie que le type est préservé. Cette réduction est appelée la ι-réduction et s’écrit :

On remarque que cette construction est analogue à une déclaration par filtrage, dans laquelle on examine dans l’ordre les constructeurs et on n’a que des motifs de la forme (co_m x¹… x^n_m) avec co_m un constructeur et x^k une variable. On peut utiliser la notation :

Élimination non dépendante

Un cas particulier souvent utilisé de l’élimination est celui où le prédicat P ne dépend pas de l’objet éliminé. On parle alors d’élimination non-dépendante . La règle devient :

Codage imprédicatif

Les définitions inductives peuvent être vues comme de nouveaux objets ajoutés à la théorie, ou bien on peut essayer de les coder, c’est-à-dire, étant donné une théorie fixée, et une déclaration inductive de la forme 3.1.1, peut-on trouver des termes nom, co_m et Case qui ont les types appropriés et satisfont les règles de réduction.

Un des attraits des logiques d’ordre supérieur est qu’elles sont assez puissantes pour coder les définitions inductives. C’est d’ailleurs ce qui est fait dans les systèmes HOL, où les définitions inductives sont juste des packages plus ou moins puissants automatisant la définition de propriétés.

Dans le Calcul des Constructions Pures, il est possible de coder les définitions inductives. On introduit les définitions suivantes :

On vérifie que les objets introduits sont bien typés du type attendu sauf dans le cas du schéma d’élimination Case où le type est plus faible que celui que nous avons proposé précédemment. En effet on intègre dans le schéma le fait que dans chaque branche (a₁,…,a_l) est égal à (t_m¹,… t_m^l) mais pas le fait que x lui-même est égal à (co_m x¹… x^n_m). On appelle le schéma ainsi obtenu le schéma itératif. Dans le cas non récursif, ce schéma est le même que le schéma non-dépendant. On remarque également que le schéma d’élimination que nous avons codé a une sorte d’élimination qui est la même que la sorte de la définition inductive.

Cette représentation imprédicative a l’avantage de ne pas nécessiter d’extension de la théorie et donc de ne pas poser de problème théorique supplémentaire. Cependant, la faiblesse du schéma d’élimination fait que certaines propriétés logiquement très fortes et pourtant attendues ne sont pas prouvables.

On peut construire le type des booléens : bool:=∀ C:Set,C→ C → C avec true:=λ (C:Set)(t f:C) ⇒ t et false:=λ (C:Set) (t f:C)⇒ f mais il n’est pas possible de prouver true≠false et il n’est pas possible de montrer :

Il devient alors difficile de raisonner sur les booléens sauf à ajouter ces propriétés comme axiome. cependant, on perd alors la correspondance entre le calcul et le raisonnement.

Une autre difficulté du codage imprédicatif est qu’il y a plus de termes normaux clos dans le codage du type inductif que ceux construits à partir des constructeurs.

L’exemple le plus simple illustrant ce phénomène consiste à prendre le type inductif I des singletons avec un seul constructeur c:(Un→Un) → I. Le codage imprédicatif donne :

Il n’est pas difficile de construire un terme normal clos de type I qui ne peut s’écrire sous la forme (c f) avec f un terme normal clos de type Un→Un.

On distingue une classe de types appelés « types de données » qui correspondent à des codages de définitions inductives dans lesquelles tous les types d’arguments des constructeurs sont eux-mêmes récursivement des « types de données » (il est surtout essentiel qu’il n’y ait pas de quantification d’ordre supérieur en position négative). Pour les types de données, il est possible d’établir un théorème de représentation à savoir que tous les termes clos normaux sont β-équivalent à un constructeur appliqué à des arguments clos du bon type. Cependant, même pour les types de données, le schéma qui dit que les seuls objets dans le type sont ceux obtenus via les constructeurs n’est pas démontrable.

Définition de types par cas/Élimination forte

On appelle schéma d’élimination forte, le schéma d’élimination d’un inductif d’une sorte imprédicative (par exemple Prop mais aussi Set dans le calcul des constructions avec Set imprédicatif) vers des prédicats de sorte Type.

Si on reprend l’exemple des booléens, le schéma d’élimination forte a la forme suivante :

On peut en particulier instancier ce schéma avec P:=λ b:bool⇒ Prop, on obtient

En prenant pour f la propriété toujours vrai True et pour g la propriété toujours fausse False on obtient une propriété φ de type bool→ Prop telle que (φ true) est équivalent à True et (φ false) équivalent à False. Cette propriété P nous permet de réfuter le fait que true=false.

On peut également prendre P:=λ b:bool⇒ Set, f:=nat et g:=bool, on pourra alors définir un type ψ de type bool→ Set tel que (φ true) est équivalent à nat et (φ false) équivalent à false. Pour construire un objet dans ce type, il est encore nécessaire d’utiliser le schéma d’élimination de bool en prenant cette fois-ci P:=ψ, f:nat et g:bool. On a alors :

Ces fonctions sortent du cadre de ce qui peut être typé dans un langage à la ML, elles sont pourtant très utiles dans les techniques de preuve à base de réflexion pour interpréter les objets d’un type concret de proposition vers des propriétés Coq.

Nous verrons dans la partie 3.2.4 que l’élimination forte ne peut être autorisée pour tous les types inductifs sans risque de rendre le système incohérent.

Types dépendants

Les définitions inductives permettent de définir des familles de type I:∀ (a₁:A₁)…(a_n:A_n), s. Par exemple, on peut définir une relation neq sur les booléens par :

Il est étrangement plus complexe de construire une preuve de (neq b₁ b₂) ⇒ P lorsque b₁ et b₂ sont des termes et plus seulement des variables distinctes. C’est le cas par exemple si on veut montrer (neq true true) ⇒ ⊥ ou (b:bool)(neq b b) ⇒ ⊥.

En fait pour pouvoir utiliser le schéma d’élimination il faut pouvoir généraliser la propriété à montrer en : ∀ (x₁ x₂:bool),(neq x₁ x₂) ⇒ (Q x₁ x₂). puis l’appliquer à b₁ et b₂. Les exemples ci-dessus montrent qu’une généralisation naïve ne fonctionne pas en général. Une manière systématique de résoudre ce problème est de renforcer la propriété à prouver en :

puis d’utiliser l’élimination standard et de simplifier les égalités. Certaines correspondent à des hypothèses absurdes, d’autres vont donner lieu à des simplifications, on obtiendra de nouvelles égalités qui pourront être propagées.

Tactiques d’inversion

Le travail décrit ci-dessus est (partiellement) automatisé par les tactiques d’inversion. Cependant la preuve engendrée est loin d’être atomique. Il faut donc éviter autant que possible d’avoir recours aux schémas d’inversion. Pour cela, il est utile de mettre explicitement en paramètre tout argument qui n’est pas instancié dans les constructeurs (juste une variable liée). L’ordre dans lequel on réalise les éliminations, et des généralisations appropriées permettent parfois d’éviter l’utilisation de l’inversion. Finalement, il peut être utile d’engendrer des principes d’élimination ad-hoc pour certaines instances de définition inductive, ce qui permet d’éviter l’utilisation multiple de l’inversion.

Égalité

On note x=y le terme (eq x y). Le schéma d’élimination exprime que toute preuve de x=y est de la forme (refl x), il a la forme suivante :

Cette égalité permet de comparer deux objets du même type. Cependant, on est parfois amenés à devoir comparer des objets dans des types différents.

Une propriété attendue est ∀ l:(list 0), l=nil. Pour la montrer, en utilisant la généralisation pour l’inversion, on voudrait se ramener à montrer : ∀ (n:nat)(l:(list n)), n=0→ l=nil. Malheureusement, cette propriété ne peut être énoncée car la propriété l=nil est mal formée puisque l:(list n) et nil : (list 0) sont de type différents non convertibles. Le fait qu’il existe une preuve e de n=0 dans le contexte permet juste d’appliquer une transformation à l pour en faire un objet de type (list 0). Mais l’énoncé devient

On peut ensuite faire une preuve par cas sur l, cependant on se retrouve à devoir montrer :

On souhaiterait alors utiliser le fait que toute preuve de 0=0 est de la forme (refl 0), en remplaçant e par cette valeur, on doit montrer

En utilisant la ι réduction, on aboutit à la trivialité nil=nil. Malheureusement, le remplacement de e:0=0 par (refl 0) ne peut se faire. En effet, il faut utiliser le schéma d’élimination qui demande de généraliser le but sous la forme d’un prédicat de type ∀ y:nat, (0=y)→ Prop or les dépendances nous empêchent de généraliser comme on le souhaiterait :

Cette « pathologie » a été mise en évidence par Thierry Coquand. Thomas Streicher et Martin Hofmann [HS98] ont exhibé des modèles de la théorie des types, pour lesquels il y a des preuves de x=x qui ne sont pas convertibles à (refl x). Cependant, s’il existe une égalité décidable sur A (ce qui est le cas de tous les types de données usuels), alors cette propriété est démontrable mais la construction est complexe (l’idée originale est due à Michael Hedberg, elle a été codée dans LEGO par Thomas Kleymann et reprise dans Coq par Bruno Barras, cf le fichier theories/Logic/Eqdep_dec.v).

L’axiome K de Streicher

Thomas Streicher a proposé d’ajouter un principe d’élimination plus puissant pour l’égalité qui capture exactement que toute preuve de x=x est une preuve par réflexivité :

Il existe de nombreuses formes équivalentes de cet axiome. La théorie EqDep de Coq introduit un axiome qui dit que :

qui ne dit pas que e est égal à (refl x) mais qu’il se comporte calculatoirement de manière identique.

Égalité de John Major

C. McBride [McB99] a introduit une égalité qui permet de comparer deux objets dans des types quelconques. De manière inductive, cette égalité se définit par :

On peut facilement prouver que cette égalité est réflexive. symétrique et transitive en utilisant le schéma général des définitions inductives. Par contre, ce schéma impose une généralisation du but sous la forme d’un prédicat de type ∀ B:Set, B→ Prop, ce qui est en général malaisé.

C. McBride propose d’introduire un schéma d’élimination renforcé, analogue (et prouvablement équivalent) à l’axiome K de Streicher. Ce schéma d’élimination dit que si deux objets de même type sont égaux selon l’égalité de John Major, alors on peut remplacer l’un par l’autre (autrement dit, ils sont égaux au sens de l’égalité de Leibniz).

Cette égalité est commode car si on a n:nat et l:(list n) ainsi que n′:nat et l′:(list n′), on pourra simplement écrire (eq nat n nat n′) et (eq (list n) l (list n′) l′). Comme n et n′ sont du même type, on pourra remplacer n par n′ en particulier dans le type de l, ensuite l et l′ seront du même type (list n′) et on pourra remplacer l par l′. Cette égalité évite de passer par un codage de paires assez lourd.

3.2.4 Types inductifs et sortes

Nous n’avons pour l’instant pas préciser les sortes pour lesquelles l’élimination d’une définition inductive était possible.

Les types de données prédicatifs

Les types de données prédicatifs sont ceux pour lesquels les types des arguments des constructeurs sont dans la même sorte que l’inductif. C’est forcément le cas si le type inductif est dans Type ou bien dans Set dans le cas où cette sorte est aussi prédicative.

Les types de données imprédicatifs

Un type de données est imprédicatif s’il est défini dans Prop (ou aussi dans Set, si on se place dans la version de Coq avec Set imprédicatif) et si au moins un des types d’argument est dans la sorte Type. C’est le cas de la définition :

Si on autorisait, pour cette définition, une élimination forte alors on pourrait définir :

On vérifie de plus que (out (in P)) ≃ P. On a donc prop:Prop qui est isomorphe à Prop:Type ce qui introduit deux niveaux d’imprédicativité et donne un système incohérent.

Une possibilité est d’interdire les définitions imprédicatives, celles-ci peuvent être représentées par un codage à l’ordre supérieur. Dans Coq, de telles définitions sont autorisées, on peut utiliser le schéma d’élimination usuel sur la sorte imprédicative de la définition inductive par contre l’élimination forte (sur un prédicat dont la sorte est Type) ne peut pas leur être appliquée.

De telles définitions inductives sont utiles pour coder des existentielles du second ordre qui servent elle-même à coder des types abstraits : on sait qu’il existe un type avec certaines opérations sur ce type mais on ne peut pas accéder à l’implantation de ce type. Un exemple de telle utilisation est la définition nu dans contribs/Lyon/GFP.v qui code un plus grand point-fixe d’un opérateur monotone sur les types.

La distinction entre Prop et Set

Les sortes Prop et Set sont toutes les deux de type Type. Leur interprétation diffère vis-à-vis de l’extraction de programmes à partir de preuves. Un terme de preuve est dit logique s’il est de type P:Prop; le typage garantit qu’il ne servira pas de manière calculatoire pour construire un terme de preuve calculatoire de type S:Set. Ceci permet d’éliminer les termes de preuve logique qui sont toujours en position de code mort dans les termes calculatoires.

Si un type inductif est de type Prop alors on ne peut pas en général autoriser une élimination sur la sorte Set. En effet la règle d’élimination est :

Si x est logique, il doit disparaître à l’extraction, par contre si s′ est de type Set on doit être en mesure de fournir une réalisation de (P a₁… a_l x). On a beau pouvoir extraire chaque branche f_i, en l’absence de x, il est difficile de les combiner.

On aboutit à la règle suivante : un inductif de sorte Prop ne peut s’éliminer sur un prédicat de sorte Set. Il ne peut pas non plus s’éliminer sur un prédicat de sorte Type, car tout objet dans Set est également un objet de la sorte Type, donc l’élimination sur Type implique l’élimination sur Set.

De plus l’élimination sur Type permet de montrer qu’il existe une propriété A:Prop et a,b:A tel que a≠b est prouvable (par analogie avec la preuve de true≠false). Or du fait de notre interprétation non calculatoire des propositions logiques, supposer que toutes les preuves d’une même proposition logique sont égales est parfois utile. C’est également une propriété que l’on dérive à partir d’autres axiomes tel que celui de la logique classique ∀ A:Prop, A ∨ ¬ A ou de l’extensionnalité ∀ A B:Prop,(A ↔ B)→ A=B.

Les types singletons

Il existe deux cas particuliers d’inductif définis dans Prop pour lesquels l’élimination sur la sorte Set ne pose pas de difficulté. Il s’agit tout d’abord de la définition inductive vide. Dans une situation ou l’absurde est prouvable, n’importe quel objet est un programme correct par rapport à n’importe quelle définition inductive.

Le second cas est plus intéressant. Nous appelons type singleton, un type qui n’a qu’un constructeur dont tous les types d’arguments sont de type Prop. L’élimination ne comporte donc qu’une seule branche et on montre aisément que si la propriété est vérifiée alors le programme extrait de cette branche est correct par rapport à la propriété de la conclusion. L’extraction de la définition par cas est alors définie comme l’extraction de l’unique branche, l’élément sur lequel se fait le Case n’intervient donc pas dans le calcul. On peut montrer que pour de tels types, dès que l’on a l’élimination vers Set et que ces types sont prédicatifs, alors l’élimination vers Type peut également être simulée et est donc valide.

Les types conjonctions de propriétés logiques sont des types singletons, bien que définis dans Prop ils admettent une élimination pour toutes les sortes, il en est de même du prédicat d’égalité que nous avons défini plus haut.

La condition que tous les types d’arguments de constructeur sont de nature purement propositionnelle est essentielle. Un exemple de type à un seul constructeur qui ne vérifie pas cette condition est un type I avec un seul constructeur c avec un argument de type bool. La règle d’élimination :

Sur le plan calculatoire, la preuve x est essentielle pour décider l’instance de la branche à choisir (f true) ou bien (f false).

3.3 Les types inductifs récursifs

3.3.1 Exemples

La définition inductive récursive de base est bien entendu celle des entiers :

À peine plus compliquée est celle des listes, qui peut être paramétrée par le type des éléments :

On construit aisément sur le même modèle le type des arbres ou de manière plus générale de toute structure de terme algébrique.

Un exemple un peu plus sophistiqué est celui des notations ordinales (du second ordre). Il se construit comme le type des entiers, mais on ajoute un constructeur de limite qui correspond à un branchement infini paramétré par des entiers. Cette structure infinie se représente de manière finie par une fonction des entiers vers les ordinaux.

En suivant le même modèle, on peut définir un type générique d’arbre où les branchements sont indicés par un premier type de données A (il y a autant de type de branchements possibles que d’éléments dans A) et où l’arité de chaque branchement est donnée par un type B qui dépend de l’indice du branchement : Ce type a été initialement introduit par Per Martin-Löf et est traditionnellement écrit W. Il se définit en Coq par :

Ce type est suffisant pour coder les autres définitions inductives. Par exemple, pour représenter les entiers, on remarque qu’il nous faut deux types de branchement (l’un pour 0 qui est d’arité nulle et l’autre pour S qui est d’arité un). Il suffit donc de prendre A ≡ bool et B définie par (B true) ≡ False et (B false) ≡ True. On pose alors : nat≡ (W A B) On peut alors introduire 0 ≡ (node true λ t:False⇒ Case(nat,t)) et S ≡ λ n:nat⇒ (node false λ t:True⇒ n) dont on vérifie qu’ils ont le bon type.

Un autre type récursif intéressant est la définition d’un élément bien fondé x:A pour une relation R:A→ A → Prop. On dit que x est bien fondé si tous les éléments en relation avec x sont eux-mêmes bien fondés. Cela s’écrit :

3.3.2 Condition de positivité

Positivité large

Un type inductif qui comporterait une occurrence récursive négative, permet de construire des objets qui bouclent sans utiliser de récursivité. Supposons que l’on puisse définir :

et que l’élimination sur la sorte Set soit permise. Ce type est habité puisqu’il contient au moins le terme (lam [x:L]x) On peut également définir :

On vérifie alors que le terme (app δ δ) se réduit en une étape de ι réduction vers lui-même et donc que ce terme n’est pas normalisable.

Cet exemple peut être aisément codé en ML. Par contre, il explique pourquoi les définitions inductives doivent imposer une condition de positivité.

Une définition inductive I est positive si les seules occurrences de I dans des types d’arguments de constructeur se font de manière positive, c’est-à-dire à la gauche d’un nombre pair (éventuellement nul) de produits avec la définition suivante : Dans le terme ∀ x:A,B, le terme B est à gauche de 0 produit, un sous-terme C de B qui est à gauche de n produits dans B est également à gauche de n produits dans ∀ x:A,B. Le terme A est à gauche d’un produit dans ∀ x:A,B et un sous-terme C de A qui est à gauche de n produits dans A est également à gauche de n+1 produits dans ∀ x:A,B.

Un type d’argument C qui dépend de I de manière positive satisfait une condition de monotonicité, c’est-à-dire que si I ⊆ J (autrement dit s’il existe un terme de type ∀ (a₁:A₁)…(a_l:A_l), (I a₁… a_l) → (J a₁… a_l)) alors on peut construire un terme de type C→ C{I:=J}. Cette condition de monotonicité suffit à garantir l’existence d’un plus petit point fixe qui peut être codé de manière imprédicative.

Par contre, cette positivité au sens large ne convient pas lorsqu’il s’agit de définir un type inductif au niveau prédicatif Type. Th. Coquand [CPM90] a montré que accepter la définition inductive suivante conduisait à un paradoxe :

En effet, pour tout Y, il existe une application ψ de Y dans Y→Prop qui à y:Y associe le prédicat λ y′⇒ y=y′. On en déduit une application φ de X→Prop dans X qui à P de type X→Prop associe (in λ P′. P=P′). On vérifie que φ est une injection : φ(P)=φ(P′) → P=P′. Il suffit alors de considérer le prédicat P₀ = λ x. ∃ P,φ(P)=x ∧ ¬ (P x) et de prendre x₀=φ(P₀). On vérifie alors aisément que (P₀ x₀) est equivalent à ¬(P₀ x₀) d’où une incohérence.

Positivité stricte

Les définitions inductives de Coq ne permettent pas de la positivité large (c’est-à-dire une occurrence de la définition inductive à la gauche d’au moins un produit).

Le schéma général est que si la définition inductive I apparaît dans un type d’argument d’un constructeur alors ce type d’argument à la forme :

On vérifiera que toutes les définitions inductives données en exemple satisfont cette condition de positivité.

Récursivité emboîtée

La positivité stricte n’interdit pas a priori que l’argument récursif se trouve comme paramètre d’une autre définition inductive. De fait, si un type de constructeur de la définition inductive I a pour type (A * I) → I ou A*I est la définition inductive pour le produit de A et de I alors, I est équivalente à une définition J où le type de constructeur serait A → J → J et donc strictement positif. De même si le constructeur est (A + I) → I alors on peut le remplacer par deux constructeurs strictement positifs de type A → J et J → J. Cela fonctionne même si la définition imbriquée est récursive, il faut alors définir deux types mutuellement récursifs. Si le type de constructeur est (list I) → I on remplace I par une définition J définie de manière mutuellement récursive avec L qui représente (list I). Le constructeur de type (list I) → I devient un constructeur de type L → J, les constructeurs de L sont ceux de (list I) soit nil_L : L et cons_L : J → L → L.

Cette transformation nous montre qu’il est possible d’autoriser une occurrence récursive de l’inductif I comme paramètre d’une autre définition inductive J. Cependant certaines conditions doivent être vérifiée. L’occurrence de I doit apparaître strictement positivement en position de paramètre de la définition inductive J, et ce paramètre doit lui-même apparaître strictement positivement dans les types d’arguments de J. On peut donc avoir un type de constructeur de I de la forme (list (A+I)) → I par contre si on introduit

Alors définir un inductif I dont un type de constructeur est (neg I) → I est non valide.

3.3.3 Schéma d’élimination récursif primitif

Supposons que l’on définisse un inductif récursif qui vérifie la condition de stricte positivité sans imbrication. Alors le schéma d’élimination peut être renforcé pour prendre en compte le fait que la propriété que l’on cherche à montrer est récursivement satisfaite pour les sous-termes du type approprié.

On peut donc renforcer le schéma d’élimination en prenant sa forme récursive :

Si C est un type d’argument récursif strictement positif et sans imbrication alors il est de la forme :

On voit que ce schéma d’élimination est plus général que le schéma non récursif préalablement introduit. Il implique en particulier que l’ordre structurel sur le type inductif est bien fondé. Nos objets dans le type inductif ne représentent que des structures qui peuvent être infinies mais dont toutes les branches récursives sont finies.

Les schémas d’élimination récursive sont engendrés automatiquement par Coq au moment de la définition inductive. Dans le cas d’une définition de sorte Prop, le schéma déclaré correspond à une élimination non dépendante. Les schémas dépendants peuvent être introduits à l’aide de la commande de vernaculaire Scheme.

Dans le cas de définition inductive imbriquée, la forme du schéma d’élimination récursive n’est pas aussi simple à formuler. Coq ne fournit pas de facilité pour les introduire, c’est à l’utilisateur de concevoir un schéma adapté et de le démontrer à l’aide de l’élimination récursive et des constructions par point fixe que nous allons maintenant introduire.

3.3.4 Condition de garde

Le schéma d’élimination récursive était proposé par P. Martin-Löf comme la construction d’élimination de base des définitions inductives. Il permet de capturer la notion de fonctionnelle définie de manière primitive récursive ainsi que la notion de preuve par récurrence structurelle.

Cependant, Th. Coquand a suggéré une approche alternative, où comme dans les langages de programmation fonctionnelle, les notions primitives sont l’élimination non récursive (qui correspond à l’analyse par cas) et les définitions par point fixe. Évidemment, on ne peut autoriser n’importe quel point fixe sous peine de construire des termes non normalisables et d’aboutir à une incohérence. Une condition syntaxique de garde permet d’accepter les définitions qui suivent un schéma primitif récursif et de préserver la terminaison.

Pour cela, une fonction f peut être définie par point fixe si un de ses arguments x a pour type une définition inductive et si dans le corps de f tous les appels récursifs à f se font avec en place de x un terme t que l’on reconnaît syntaxiquement comme étant plus petit que x.

La règle principale pour être structurellement plus petit que x est d’apparaître dans une branche d’un Case sur x et d’être l’un des sous-termes de x. Mais cette définition peut être étendue. Par exemple un Case est reconnu plus petit que x si chacune de ses branches est plus petite que x (en particulier s’il n’y a aucune branche dans le cas de l’élimination d’une condition absurde). De même être plus petit est une opération transitive.

dans lequel f est une variable liée et n est un entier positif ou nul. La règle de typage est :

La règle de réduction est également gardée par la condition que l’argument de décroissance commence par un constructeur. Ceci permet d’éviter de poursuivre la réduction du point fixe à l’intérieur du terme ce qui violerait la terminaison forte.

On définit aisément à l’aide du point fixe la fonction qui calcule le minimum de deux entiers :

L’exigence que l’argument de décroissance soit de type inductif est essentielle. En effet, du fait de la présence d’imprédicativité, on peut construire des types pour lesquels certains sous-arbres sont plus « grands » que l’objet initial. Ainsi si on introduit un type I avec un constructeur (non-récursif) c de type (∀ A:Set,A→ A)→ I. On introduit l’objet t ≡ λ (A:Set)(x:A)⇒ x de type ∀ A:Set, A→ A. L’objet (c t) est de type I. Soit une fonction f de type I→I définie par

On pourrait penser que l’appel récursif qui se fait sur un sous-terme x de (c x) est bien fondé. Ce n’est pas le cas. En effet (f (c t)) se réduit en (f (t I (c t))) qui se réduit en (f (c t)) et donc se terme ne se normalise pas.

3.3.5 Récurrence structurelle versus récurrence bien fondée

La définition primitive par point fixe permet de capturer certaines fonctions récursives mais évidemment toutes les fonctions ne suivent pas ce critère de décroissance structurel. Un exemple classique est la fonction quicksort sur les listes qui s’appelle récursivement sur deux sous-listes qui sont de longueur plus petite. Évidemment, on sait ramener cette décroissance à un point-fixe structurel sur un argument supplémentaire représentant la longueur de la liste. Mais on voudrait également pouvoir justifier la définition par point fixe, en utilisant uniquement un argument de bonne fondation de la relation avoir une longueur strictement plus petite.

On suppose que l’on dispose d’une fonction split : A→ list → list × list qui sépare une liste l suivant un pivot a en deux listes l₁ et l₂ telle que la longueur de l_i est inférieure ou égale à la longueur de l. On notera |l| la longueur de l, qui vérifie les propriétés :

On peut alors définir une fonction de tri quick : ∀ (l:list)(n:nat),|l|≤ n → list de manière structurelle sur n. La définition de quick suit le schéma suivant :

Avec h₀, h₁ et h₂ des preuves de ⊥, |l₁|≤ n et |l₂|≤ n. Pour obtenir une fonction de tri de type list→ list il suffit de prendre une valeur initiale de n égale à la longueur de l. Cependant, d’un point de vue calculatoire, l’argument entier n qui a été ajouté apparaît superflu.

L’alternative consiste à utiliser une preuve du fait que la relation R≡ λ l,m:list⇒ |l|<|m| est bien fondée.

Le programme se construit alors comme un terme quickwf de type :
∀ l:list,(wf list R l) → list. Cette preuve suit le schéma suivant :

Avec h₁ et h₂ des preuves de (wf list R l₁) et (wf list R l₂) qui sont structurellement plus petites que h. Ces preuves sont construites de la manière suivante. Il est possible de définir wf_inv de type ∀ (A:Set)(R:A→ A→ Prop)(x:A), wf A R x → ∀ y:A, R y x→ wf A R y par :

On remarque que (wf_inv A R x H) est structurellement plus petit que H car obtenu en prenant un sous-terme structurel de H.

Pour obtenir une fonction de type list→list il suffit d’utiliser une preuve que R est bien fondée, c’est-à-dire d’une preuve de ∀ l:list, (wf list R l).

L’avantage de cette définition est que la propriété wf peut être définie dans la sorte Prop. Donc le comportement calculatoire de la fonction quickwf à l’extraction est le comportement attendu. Par contre, il est compliqué de réduire la fonction quickwf dans Coq car cette réduction ne peut avoir lieu que si la preuve h de (wf list R l) commence par un constructeur. Pour raisonner sur de telles fonctions, il est préférable d’établir des équations de point fixe. Cependant ces équations ne sont pas immédiates à établir. Ce problème a été étudié en détail dans la thèse de Antonia Baala [Bal02]. Des théorèmes dans la bibliothèque Init/Wf permettent de faciliter les constructions de fonctions par point fixe.

3.3.6 Définitions mutuellement inductives

Coq accepte de manière primitive les définitions mutuellement récursives. En fait de telles définitions peuvent simplement être codées en faisant de la définition inductive une famille de définitions inductives. On introduit un type A qui fait la somme disjointe des arités des différentes définitions inductives. Les définitions mutuellement inductives I_k seront remplacées par une famille inductive d’arité A → s dans laquelle s est la sorte des définitions inductives. On remplace dans les types de constructeur chaque mention à une des définitions mutuellement inductives (I_k a₁… a_l) par la référence à l’instance appropriée de I, c’est-à-dire (I (in_k a₁… a_l)). Le schéma d’élimination mutuellement récursif des définitions I_k peut également se déduire du schéma général pour I.

Exemple 4

Inductive arbre (A:Set) : Set :=
  | node : A → (foret A) → (arbre A)
with foret (A:Set) : Set :=
  | vide : (foret A)
  | add : (arbre A) → (foret A) → (foret A).

est équivalent à

Inductive arbre_foret (A:Set) : bool → Set :=
  | node : A → (arbre_foret A false) → (arbre_foret A true)
  | vide : (arbre_foret A false)
  | add : (arbre_foret A true) → (arbre_foret A false) 
          → (arbre_foret A false).
Definition arbre (A:Set) := arbre_foret A true.
Definition foret (A:Set) := arbre_foret A false.

Dans le cas de définitions mutuellement récursives, Coq engendre automatiquement un principe d’élimination récursive pour chaque type qui ne tient pas compte des appels aux autres inductifs de la famille. Par contre la commande Scheme permet d’engendrer automatiquement les schémas d’élimination mutuellement récursifs dans le cas de positivité non imbriquée. Ces schémas peuvent ensuite être utilisés par la tactique

en instanciant de manière appropriée les propriétés à montrer pour les types auxiliaires.

Dans le cas de l’exemple des arbres et des forêts, la commande Inductive introduit en particulier le schéma suivant qui n’utilise pas la structure récursive de foret :

Pour définir arbre_foret_ind qui permet de prouver une propriété P sur les arbres en utilisant une propriété Q sur les forêts prouvée de manière mutuellement récursive, on utilise :

3.4 Extensions

Les définitions inductives du Calcul des Constructions Inductives permettent une représentation directe des types de données concrets et des relations inductives définies comme les plus petites propriétés satisfaisant un ensemble de conditions de stabilité.

Cependant, cette notion est insuffisante pour représenter certaines structures qui apparaissent naturellement dans les développements mathématiques et informatiques.

3.4.1 Structures infinies

Il s’agit en particulier des structures potentiellement infinies comme les streams (suites infinies), les séries mathématiques ou les expressions de processus. Il est possible d’utiliser des fonctions pour représenter de tels objets mais on aimerait une représentation plus proche de la structure concrète de ces objets. Les définitions co-inductives ont une structure duale des définitions inductives. Elles ont été ajoutées au Calcul des Constructions Inductives et intégrées à Coq par Eduardo Giménez. L’approche suivie avait été suggérée par Th. Coquand. Les définitions co-inductives admettent comme schéma d’élimination la définition par cas et comme règle d’introduction, en complément des constructeurs, des définitions par point fixe.

3.4.2 Structures quotients

Les définitions (co)-inductives sont des structures libres, il est donc possible de prouver que deux constructeurs d’un type inductif dans Set ou Type ont des images disjointes. Supposer qu’une équation entre constructeurs est satisfaite conduit à une théorie inconsistante. Pourtant les structures quotients sont très utilisées (représentation des rationnels, des réels ou des lambda-termes). Plusieurs solutions ont été proposées pour ajouter des types quotients à une théorie des types, en particulier par R. Backhouse, M. Hofmann, S. Boutin, G. Barthe et plus récemment par P. Courtieu. A part NuPrl, les assistants de preuve ne proposent pas de type inductif quotient. C’est à l’utilisateur de gérer à la main une égalité ad-hoc et des conditions de compatibilité.

3.4.3 Réductions généralisées

Les types inductifs de Coq permettent de définir aisément une addition sur les entiers qui vérifie les axiomes de Peano 0+x=x et (S y)+x=(S (x+y)) comme des règles de conversion. Par contre la propriété x+0=x ou l’associativité de l’addition sont prouvables mais ne sont pas des conversions et doivent donc être traités manuellement alors que les systèmes de réécriture savent parfaitement traiter ses égalités de manière automatique. Pour pallier cette difficulté, on étudie depuis quelques années des systèmes qui combinent la réécriture et le lambda-calcul typé. Une difficulté est de garantir la confluence et terminaison du système résultant. Pour cela, il faut bien entendu restreindre la forme des réécritures applicables. Les travaux récents de F. Blanqui dans la lignée de ceux de J.-P. Jouannaud et M. Okada proposent un cadre qui capture un très large sous-ensemble des définitions inductives de Coq et permet de définir des fonctions par des systèmes de réécriture vérifiant un certain schéma. De manière alternative, J.-P. Jouannaud, A. Rubio et D. Walukiewicz-Chrząszcz proposent un ordre RPO applicable aux termes du Calcul des Constructions qui garantit la préservation par ajout de règles de réécriture.

Cours 3 Types inductifs