Le Coq’ Art (V8)

Publié par

Le Coq’ Art (V8)Yves Bertot, Pierre Castéran26 janvier 20112Table des matières1 Préface 112 Un bref tour d’horizon 232.1 Expressions, types et fonctions . . . . . . . . . . . . . . . . . . . 242.2 Propositions et preuves . . . . . . . . . . . . . . . . . . . . . . . 252.3 Propositions et types . . . . . . . . . . . . . . . . . . . . . . . . . 262.4 Spécifications complexes et programmes certifiés . . . . . . . . . 272.5 L’exemple du tri . . . . . . . . . . . . . . . . . . . . . . . . . . . 272.5.1 Définitions inductives . . . . . . . . . . . . . . . . . . . . 282.5.2 La relation «avoir les mêmes éléments» . . . . . . . . . . 282.5.3 La spécification du tri . . . . . . . . . . . . . . . . . . . . 292.5.4 Une fonction auxiliaire . . . . . . . . . . . . . . . . . . . . 292.5.5 Le tri proprement dit . . . . . . . . . . . . . . . . . . . . 302.6 Apprendre Coq . . . . . . . . . . . . . . . . . . . . . . . . . . . . 312.7 Contenu de l’ouvrage . . . . . . . . . . . . . . . . . . . . . . . . . 322.8 Conventions lexicales . . . . . . . . . . . . . . . . . . . . . . . . . 343 Types et expressions 373.1 Premiers pas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 383.1.1 Termes, expressions, types, etc. . . . . . . . . . . . . . . . 383.1.2 Notion de portée . . . . . . . . . . . . . . . . . . . . . . . 383.1.3 Contrôle de type . . . . . . . . . . . . . . . . . . . . . . . 403.2 Les règles du jeu . . . . . . . . . . . . . . . . . . . . . . . . . . . ...
Publié le : mardi 11 octobre 2011
Lecture(s) : 49
Nombre de pages : 512
Voir plus Voir moins
Le Coq’ Art (V8) Yves Bertot, Pierre Castéran 26 janvier 2011 2 Table des matières 1 Préface 11 2 Un bref tour d’horizon 23 2.1 Expressions, types et fonctions . . . . . . . . . . . . . . . . . . . 24 2.2 Propositions et preuves . . . . . . . . . . . . . . . . . . . . . . . 25 2.3 Propositions et types . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.4 Spécifications complexes et programmes certifiés . . . . . . . . . 27 2.5 L’exemple du tri . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.5.1 Définitions inductives . . . . . . . . . . . . . . . . . . . . 28 2.5.2 La relation «avoir les mêmes éléments» . . . . . . . . . . 28 2.5.3 La spécification du tri . . . . . . . . . . . . . . . . . . . . 29 2.5.4 Une fonction auxiliaire . . . . . . . . . . . . . . . . . . . . 29 2.5.5 Le tri proprement dit . . . . . . . . . . . . . . . . . . . . 30 2.6 Apprendre Coq . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2.7 Contenu de l’ouvrage . . . . . . . . . . . . . . . . . . . . . . . . . 32 2.8 Conventions lexicales . . . . . . . . . . . . . . . . . . . . . . . . . 34 3 Types et expressions 37 3.1 Premiers pas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 3.1.1 Termes, expressions, types, etc. . . . . . . . . . . . . . . . 38 3.1.2 Notion de portée . . . . . . . . . . . . . . . . . . . . . . . 38 3.1.3 Contrôle de type . . . . . . . . . . . . . . . . . . . . . . . 40 3.2 Les règles du jeu . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.2.1 Types simples . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.2.2 Identificateurs, environnements, contextes, etc. . . . . . . 43 3.2.3 Les expressions et leur type . . . . . . . . . . . . . . . . . 45 3.2.4 Occurrences libres et liées; α-conversion . . . . . . . . . . 51 3.3 Déclarations et définitions . . . . . . . . . . . . . . . . . . . . . . 52 3.3.1 Déclarations et définitions globales . . . . . . . . . . . . . 53 3.3.2 Sections et variables locales . . . . . . . . . . . . . . . . . 54 3.4 Un peu de calcul . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 3.4.1 Substitution . . . . . . . . . . . . . . . . . . . . . . . . . . 58 3.4.2 Règles de conversion . . . . . . . . . . . . . . . . . . . . . 58 3.4.3 Notations . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 3 4 TABLE DES MATIÈRES 3.4.4 Propriétés abstraites de la réduction . . . . . . . . . . . . 60 3.5 Types, sortes et univers . . . . . . . . . . . . . . . . . . . . . . . 61 3.5.1 La sorte Set . . . . . . . . . . . . . . . . . . . . . . . . . 61 3.5.2 Les univers . . . . . . . . . . . . . . . . . . . . . . . . . . 62 3.5.3 Définitions et déclarations de spécifications . . . . . . . . 64 3.6 De la spécification à la réalisation . . . . . . . . . . . . . . . . . . 65 4 Propositions et preuves 69 4.1 La logique minimale propositionnelle . . . . . . . . . . . . . . . . 71 4.1.1 Le monde des propositions et des preuves . . . . . . . . . 71 4.1.2 Buts et tactiques . . . . . . . . . . . . . . . . . . . . . . . 73 4.1.3 Un premier exemple . . . . . . . . . . . . . . . . . . . . . 74 4.2 Règles de typage et tactiques . . . . . . . . . . . . . . . . . . . . 77 4.2.1 Règles de construction des propositions . . . . . . . . . . 77 4.2.2 Règles d’inférence et tactiques . . . . . . . . . . . . . . . 78 4.3 Structure d’une preuve interactive . . . . . . . . . . . . . . . . . 83 4.3.1 Activation du système de gestion de buts . . . . . . . . . 83 4.3.2 Étape courante d’une preuve interactive . . . . . . . . . . 84 4.3.3 Hésitations . . . . . . . . . . . . . . . . . . . . . . . . . . 84 4.3.4 Fin normale d’un développement . . . . . . . . . . . . . . 84 4.4 La non pertinence des preuves . . . . . . . . . . . . . . . . . . . . 85 4.4.1 Theorem versus Definition . . . . . . . . . . . . . . . . . 86 4.4.2 Des tactiques pour construire des programmes? . . . . . . 86 4.5 Utilisation de sections . . . . . . . . . . . . . . . . . . . . . . . . 87 4.6 Composition de tactiques . . . . . . . . . . . . . . . . . . . . . . 88 4.7 Quelques problèmes de maintenance . . . . . . . . . . . . . . . . 93 4.8 Problèmes de complétude . . . . . . . . . . . . . . . . . . . . . . 94 4.8.1 Un jeu de tactiques suffisant . . . . . . . . . . . . . . . . 94 4.8.2 Des propositions impossibles à montrer . . . . . . . . . . 95 4.9 Autres tactiques . . . . . . . . . . . . . . . . . . . . . . . . . . . 95 4.9.1 Les tactiques cut et assert . . . . . . . . . . . . . . . . . 97 4.9.2 Tactiques et automatismes . . . . . . . . . . . . . . . . . 98 4.10 Un nouveau type d’abstractions . . . . . . . . . . . . . . . . . . . 99 5 Le produit dépendant 101 5.1 Éloge de la dépendance . . . . . . . . . . . . . . . . . . . . . . . 102 5.1.1 De nouveaux types flèches . . . . . . . . . . . . . . . . . . 102 5.1.2 Les liaisons nécessaires . . . . . . . . . . . . . . . . . . . . 107 5.1.3 Une nouvelle construction . . . . . . . . . . . . . . . . . . 107 5.2 Règles de typage associées au produit dépendant . . . . . . . . . 109 5.2.1 Règle d’application . . . . . . . . . . . . . . . . . . . . . . 109 5.2.2 Règle d’abstraction . . . . . . . . . . . . . . . . . . . . . . 113 5.2.3 Inférence de type . . . . . . . . . . . . . . . . . . . . . . . 114 5.2.4 Règle de conversion . . . . . . . . . . . . . . . . . . . . . 118 5.2.5 Produit dépendant et ordre de convertibilité . . . . . . . . 118 5.3 * Puissance d’expression du produit dépendant . . . . . . . . . . 119 TABLE DES MATIÈRES 5 5.3.1 Règle de formation du produit dépendant . . . . . . . . . 119 5.3.2 Types dépendants . . . . . . . . . . . . . . . . . . . . . . 121 5.3.3 Le polymorphisme . . . . . . . . . . . . . . . . . . . . . . 122 5.3.4 L’égalité en Coq . . . . . . . . . . . . . . . . . . . . . . . 126 5.3.5 Types d’ordre supérieur . . . . . . . . . . . . . . . . . . . 128 6 Logique de tous les jours 133 6.1 Pratique du produit dépendant . . . . . . . . . . . . . . . . . . . 133 6.1.1 exact et assumption . . . . . . . . . . . . . . . . . . . . 133 6.1.2 La tactique intro . . . . . . . . . . . . . . . . . . . . . . 134 6.1.3 La tactique apply . . . . . . . . . . . . . . . . . . . . . . 136 6.1.4 La tactique unfold . . . . . . . . . . . . . . . . . . . . . . 143 6.2 Connecteurs logiques . . . . . . . . . . . . . . . . . . . . . . . . . 145 6.2.1 Règles d’introduction et d’élimination . . . . . . . . . . . 145 6.2.2 Elimination du faux . . . . . . . . . . . . . . . . . . . . . 146 6.2.3 Négation . . . . . . . . . . . . . . . . . . . . . . . . . . . 147 6.2.4 Conjonction et disjonction . . . . . . . . . . . . . . . . . . 149 6.2.5 À propos de repeat . . . . . . . . . . . . . . . . . . . . . 151 6.2.6 La quantification existentielle . . . . . . . . . . . . . . . . 152 6.3 L’égalité et la réécriture . . . . . . . . . . . . . . . . . . . . . . . 153 6.3.1 Introduction de l’égalité . . . . . . . . . . . . . . . . . . . 153 6.3.2 Tactiques de réécriture . . . . . . . . . . . . . . . . . . . . 154 6.3.3 La tactique pattern . . . . . . . . . . . . . . . . . . . . . 155 6.3.4 * Réécritures conditionnelles . . . . . . . . . . . . . . . . 156 6.3.5 Recherche de théorèmes pour la réécriture . . . . . . . . . 158 6.3.6 Autres tactiques liées à l’égalité . . . . . . . . . . . . . . . 158 6.4 Tableau récapitulatif des tactiques . . . . . . . . . . . . . . . . . 158 6.5 *** Définitions imprédicatives . . . . . . . . . . . . . . . . . . . . 158 6.5.1 Avertissement . . . . . . . . . . . . . . . . . . . . . . . . . 158 6.5.2 Le Vrai et le Faux . . . . . . . . . . . . . . . . . . . . . . 159 6.5.3 Une curiosité : l’égalité de Leibniz . . . . . . . . . . . . . 160 6.5.4 Quelques autres connecteurs logiques et quantificateurs . 162 7 Structures de données inductives 165 7.1 Types sans récursion . . . . . . . . . . . . . . . . . . . . . . . . . 165 7.1.1 Types énumérés . . . . . . . . . . . . . . . . . . . . . . . 166 7.1.2 Raisonnements et calculs simples . . . . . . . . . . . . . . 167 7.1.3 La tactique elim . . . . . . . . . . . . . . . . . . . . . . . 169 7.1.4 Construction de filtrage . . . . . . . . . . . . . . . . . . . 170 7.1.5 Types enregistrements . . . . . . . . . . . . . . . . . . . . 174 7.1.6 Types enregistrements avec variantes . . . . . . . . . . . . 175 7.2 Preuves par cas . . . . . . . . . . . . . . . . . . . . . . . . . . . . 176 7.2.1 La tactique case . . . . . . . . . . . . . . . . . . . . . . . 176 7.2.2 Égalités contradictoires . . . . . . . . . . . . . . . . . . . 179 7.2.3 ** Les dessous de discriminate . . . . . . . . . . . . . . 180 7.2.4 Constructeurs injectifs . . . . . . . . . . . . . . . . . . . . 181 6 TABLE DES MATIÈRES 7.2.5 ** Les dessous d’injection . . . . . . . . . . . . . . . . . 182 7.2.6 Types inductifs et égalités . . . . . . . . . . . . . . . . . . 184 7.2.7 * Conseils dans l’utilisation de la tactique case . . . . . . 185 7.3 Types avec récursion . . . . . . . . . . . . . . . . . . . . . . . . . 188 7.3.1 Le type des entiers naturels . . . . . . . . . . . . . . . . . 189 7.3.2 Démonstration par récurrence sur les nombres naturels . . 190 7.3.3 Programmation récursive . . . . . . . . . . . . . . . . . . 192 7.3.4 Variations dans les constructeurs . . . . . . . . . . . . . . 195 7.3.5 ** Constructeurs prenant des fonctions en arguments . . . 198 7.3.6 Raisonnement sur les fonctions récursives . . . . . . . . . 200 7.3.7 Fonctions récursives anonymes (fix) . . . . . . . . . . . . 202 7.4 Types polymorphes . . . . . . . . . . . . . . . . . . . . . . . . . . 203 7.4.1 Le type des listes polymorphes . . . . . . . . . . . . . . . 204 7.4.2 Le type option . . . . . . . . . . . . . . . . . . . . . . . . 206 7.4.3 Le type des couples. . . . . . . . . . . . . . . . . . . . . . 208 7.4.4 Le type des sommes disjointes . . . . . . . . . . . . . . . . 209 7.5 * Types inductifs dépendants . . . . . . . . . . . . . . . . . . . . 210 7.5.1 Paramètres du premier ordre . . . . . . . . . . . . . . . . 210 7.5.2 Constructeurs à type dépendant variable . . . . . . . . . . 210 7.6 * Types vides . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 213 7.6.1 Types vides non dépendants . . . . . . . . . . . . . . . . . 213 7.6.2 Dépendance et types vides . . . . . . . . . . . . . . . . . . 214 8 Tactiques et automatisation 217 8.1 Les tactiques des types inductifs . . . . . . . . . . . . . . . . . . 217 8.1.1 Traitement par cas et récursion . . . . . . . . . . . . . . . 218 8.1.2 Conversions . . . . . . . . . . . . . . . . . . . . . . . . . . 219 8.2 Les tactiques auto et eauto . . . . . . . . . . . . . . . . . . . . . 221 8.2.1 Bases de tactiques : Hints . . . . . . . . . . . . . . . . . . 221 8.2.2 * La tactique eauto . . . . . . . . . . . . . . . . . . . . . 225 8.3 Les tactiques numériques . . . . . . . . . . . . . . . . . . . . . . 225 8.3.1 La tactique ring . . . . . . . . . . . . . . . . . . . . . . . 226 8.3.2 La tactique omega . . . . . . . . . . . . . . . . . . . . . . 227 8.3.3 La tactique field . . . . . . . . . . . . . . . . . . . . . . 229 8.3.4 La tactique fourier . . . . . . . . . . . . . . . . . . . . . 229 8.4 Décision pour la logique propositionnelle . . . . . . . . . . . . . . 230 8.5 ** Le langage de définition de tactiques . . . . . . . . . . . . . . 231 8.5.1 Liaison de paramètres . . . . . . . . . . . . . . . . . . . . 231 8.5.2 Constructions de filtrage . . . . . . . . . . . . . . . . . . . 232 8.5.3 Interactions avec la réduction . . . . . . . . . . . . . . . . 239 9 Prédicats inductifs 241 9.1 Quelques propriétés inductives . . . . . . . . . . . . . . . . . . . 242 9.1.1 Quelques exemples . . . . . . . . . . . . . . . . . . . . . . 242 9.1.2 Propriétés inductives et programmation logique . . . . . . 243 9.1.3 Conseils pour les définitions inductives . . . . . . . . . . . 244 TABLE DES MATIÈRES 7 9.1.4 L’exemple des listes triées . . . . . . . . . . . . . . . . . . 245 9.2 Propriétés inductives et connecteurs logiques . . . . . . . . . . . 248 9.2.1 Représentation de la vérité . . . . . . . . . . . . . . . . . 249 9.2.2 Représentation de la contradiction . . . . . . . . . . . . . 249 9.2.3 Représentation de la conjonction . . . . . . . . . . . . . . 249 9.2.4 Représentation de la disjonction . . . . . . . . . . . . . . 250 9.2.5 Représentation de la quantification existentielle . . . . . . 250 9.2.6 Représentation inductive de l’égalité . . . . . . . . . . . . 251 9.2.7 *** Égalité dépendante . . . . . . . . . . . . . . . . . . . 251 9.2.8 Pourquoi un principe de récurrence exotique? . . . . . . . 255 9.3 Raisonnement sur les propriétés inductives . . . . . . . . . . . . . 256 9.3.1 Variantes structurées de intros . . . . . . . . . . . . . . 256 9.3.2 Les tactiques constructor . . . . . . . . . . . . . . . . . 257 9.3.3 * Récurrence sur les prédicats inductifs . . . . . . . . . . 257 9.3.4 * Récurrence sur le . . . . . . . . . . . . . . . . . . . . . 260 9.4 * Relations inductives et fonctions . . . . . . . . . . . . . . . . . 264 9.4.1 Représentation de la fonction factorielle . . . . . . . . . . 264 9.4.2 ** Représentation de la sémantique d’un langage . . . . . 269 9.4.3 ** Une démonstration en sémantique . . . . . . . . . . . . 271 9.5 * Comportements élaborés de la tactique elim . . . . . . . . . . 275 9.5.1 Instancier les arguments . . . . . . . . . . . . . . . . . . . 275 9.5.2 Inversion . . . . . . . . . . . . . . . . . . . . . . . . . . . 276 10 * Les fonctions et leur spécification 281 10.1 Types inductifs pour les spécifications . . . . . . . . . . . . . . . 282 10.1.1 Type « sous-ensemble » . . . . . . . . . . . . . . . . . . . 282 10.1.2 Type sous-ensemble emboîté . . . . . . . . . . . . . . . . 284 10.1.3 Somme disjointe certifiée . . . . . . . . . . . . . . . . . . 285 10.1.4 Somme disjointe hybride . . . . . . . . . . . . . . . . . . . 286 10.2 Spécifications fortes . . . . . . . . . . . . . . . . . . . . . . . . . 287 10.2.1 Fonctions bien spécifiées . . . . . . . . . . . . . . . . . . . 287 10.2.2 Construction de fonctions par preuves . . . . . . . . . . . 288 10.2.3 Fonctions partielles par précondition . . . . . . . . . . . . 288 10.2.4 ** Complexité des démonstrations de préconditions . . . . 289 10.2.5 ** Renforcement des spécifications . . . . . . . . . . . . . 290 10.2.6 *** Renforcement minimal de spécification. . . . . . . . . 292 10.2.7 La tactique refine . . . . . . . . . . . . . . . . . . . . . . 296 10.3 Variations sur la récursion structurelle . . . . . . . . . . . . . . . 297 10.3.1 Fonctions récursives structurelles à pas multiple . . . . . . 298 10.3.2 Simplification du pas . . . . . . . . . . . . . . . . . . . . . 302 10.3.3 Fonctions récursives à plusieurs arguments . . . . . . . . . 303 10.4 ** Division binaire . . . . . . . . . . . . . . . . . . . . . . . . . . 308 10.4.1 Division faiblement spécifiée . . . . . . . . . . . . . . . . . 308 10.4.2 Division bien spécifiée . . . . . . . . . . . . . . . . . . . . 313 8 TABLE DES MATIÈRES 11 * Extraction et programmes impératifs 319 11.1 Vers les langages fonctionnels . . . . . . . . . . . . . . . . . . . . 319 11.1.1 Le mécanisme d’extraction . . . . . . . . . . . . . . . . . 320 11.1.2 La dualité Prop/Set et l’extraction . . . . . . . . . . . . . 328 11.1.3 Production effective de code OCAML . . . . . . . . . . . 330 11.2 ** Description de programmes impératifs . . . . . . . . . . . . . 331 11.2.1 L’outil Why . . . . . . . . . . . . . . . . . . . . . . . . . . 331 11.2.2 *** Les dessous de l’outil Why . . . . . . . . . . . . . . . 334 12 * Étude de cas 343 12.1 Les arbres binaires de recherche . . . . . . . . . . . . . . . . . . . 343 12.1.1 Les arbres de recherche en Coq . . . . . . . . . . . . . . . 343 12.2 Spécification des programmes . . . . . . . . . . . . . . . . . . . . 347 12.2.1 Test d’occurrence . . . . . . . . . . . . . . . . . . . . . . . 347 12.2.2 Programme d’insertion . . . . . . . . . . . . . . . . . . . . 348 12.2.3 Programme de destruction . . . . . . . . . . . . . . . . . . 348 12.3 Lemmes préliminaires . . . . . . . . . . . . . . . . . . . . . . . . 349 12.4 Vers la réalisation. . . . . . . . . . . . . . . . . . . . . . . . . . . 350 12.4.1 Réalisation du test d’occurrence . . . . . . . . . . . . . . 350 12.4.2 Insertion . . . . . . . . . . . . . . . . . . . . . . . . . . . . 353 12.4.3 ** Destruction . . . . . . . . . . . . . . . . . . . . . . . . 356 12.5 Améliorations possibles . . . . . . . . . . . . . . . . . . . . . . . 357 12.6 Un autre exemple . . . . . . . . . . . . . . . . . . . . . . . . . . . 358 13 * Le système de modules 361 13.1 Signatures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 362 13.2 Modules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 364 13.2.1 Étapes de la construction d’un module . . . . . . . . . . . 364 13.2.2 Exemple : la notion de clef . . . . . . . . . . . . . . . . . 365 13.2.3 Modules paramétriques (foncteurs) . . . . . . . . . . . . . 368 13.3 Une théorie : les relations d’ordre décidables . . . . . . . . . . . . 370 13.3.1 Enrichissement d’une théorie par foncteur . . . . . . . . . 371 13.3.2 Le produit lexicographique vu comme foncteur . . . . . . 373 13.4 Développement d’un module : les dictionnaires . . . . . . . . . . 375 13.4.1 Implémentations enrichies . . . . . . . . . . . . . . . . . . 376 13.4.2 Construction de dictionnaires par application de foncteurs 376 13.4.3 Une implémentation triviale . . . . . . . . . . . . . . . . . 376 13.4.4 Une implémentation efficace . . . . . . . . . . . . . . . . . 378 13.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 382 14 ** Objets et preuves infinis 383 14.1 Types co-inductifs . . . . . . . . . . . . . . . . . . . . . . . . . . 383 14.1.1 La commande CoInductive . . . . . . . . . . . . . . . . . 383 14.1.2 Spécificité des types co-inductifs . . . . . . . . . . . . . . 384 14.1.3 Listes infinies (Flots) . . . . . . . . . . . . . . . . . . . . . 385 14.1.4 Listes paresseuses. . . . . . . . . . . . . . . . . . . . . . . 385 TABLE DES MATIÈRES 9 14.1.5 Arbres finis ou infinis . . . . . . . . . . . . . . . . . . . . 386 14.2 Technologie des types co-inductifs. . . . . . . . . . . . . . . . . . 386 14.2.1 Construction d’objets finis . . . . . . . . . . . . . . . . . . 386 14.2.2 Décomposition selon les constructeurs . . . . . . . . . . . 387 14.3 Construction d’objets infinis . . . . . . . . . . . . . . . . . . . . . 387 14.3.1 Tentatives infructueuses . . . . . . . . . . . . . . . . . . . 388 14.3.2 La commande CoFixpoint . . . . . . . . . . . . . . . . . 388 14.3.3 Quelques constructions par co-point-fixe . . . . . . . . . . 391 14.3.4 Exemples de définitions mal formées . . . . . . . . . . . . 393 14.4 Techniques de dépliage . . . . . . . . . . . . . . . . . . . . . . . . 394 14.4.1 Décomposition systématique . . . . . . . . . . . . . . . . 395 14.4.2 Simplification et décomposition . . . . . . . . . . . . . . . 396 14.4.3 Utilisation des lemmes de décomposition . . . . . . . . . . 397 14.5 Prédicats inductifs sur un type co-inductif . . . . . . . . . . . . . 398 14.5.1 Le prédicat «être un flot fini» . . . . . . . . . . . . . . . 399 14.6 Propriétés co-inductives . . . . . . . . . . . . . . . . . . . . . . . 400 14.6.1 Le prédicat «être infini» . . . . . . . . . . . . . . . . . . 400 14.6.2 Construction de preuves infinies . . . . . . . . . . . . . . 400 14.6.3 Manque de respect de la garde . . . . . . . . . . . . . . . 402 14.6.4 Techniques d’élimination . . . . . . . . . . . . . . . . . . . 404 14.7 L’égalité extensionnelle (bisimilarité) . . . . . . . . . . . . . . . . 406 14.7.1 Le problème . . . . . . . . . . . . . . . . . . . . . . . . . . 406 14.7.2 Le prédicat bisimilar . . . . . . . . . . . . . . . . . . . . 406 14.7.3 Quelques résultats intéressants . . . . . . . . . . . . . . . 408 14.8 Le principe de Park . . . . . . . . . . . . . . . . . . . . . . . . . 409 14.9 LTL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 410 14.10Exemple d’étude : systèmes de transitions . . . . . . . . . . . . . 413 14.10.1Définitions . . . . . . . . . . . . . . . . . . . . . . . . . . 413 14.11Exploration des types co-inductifs . . . . . . . . . . . . . . . . . 414 15 ** Fondements des types inductifs 417 15.1 Règles de bonne formation . . . . . . . . . . . . . . . . . . . . . . 417 15.1.1 Le type inductif lui-même . . . . . . . . . . . . . . . . . . 417 15.1.2 Formation des constructeurs. . . . . . . . . . . . . . . . . 419 15.1.3 Comment se construit le principe de récurrence . . . . . . 421 15.1.4 Typage des récurseurs . . . . . . . . . . . . . . . . . . . . 424 15.1.5 Principes de récurrence des propriétés inductives . . . . . 431 15.1.6 La commande Scheme . . . . . . . . . . . . . . . . . . . . 433 15.2 *** Filtrage et récursion sur des preuves . . . . . . . . . . . . . . 434 15.2.1 Restriction sur le filtrage . . . . . . . . . . . . . . . . . . 434 15.2.2 Relâchement de la restriction . . . . . . . . . . . . . . . . 436 15.2.3 Récursion . . . . . . . . . . . . . . . . . . . . . . . . . . . 437 15.2.4 Élimination forte . . . . . . . . . . . . . . . . . . . . . . . 439 15.3 Types mutuellement inductifs . . . . . . . . . . . . . . . . . . . . 441 15.3.1 Arbres et forêts . . . . . . . . . . . . . . . . . . . . . . . . 441 15.3.2 Démonstration par récurrence mutuelle . . . . . . . . . . 443 10 TABLE DES MATIÈRES 15.3.3 *** Arbres et listes d’arbres . . . . . . . . . . . . . . . . . 445 16 * Récursivité générale 449 16.1 Récursion bornée . . . . . . . . . . . . . . . . . . . . . . . . . . . 450 16.2 ** Fonctions récursives bien fondées . . . . . . . . . . . . . . . . 453 16.2.1 Relations bien fondées . . . . . . . . . . . . . . . . . . . . 453 16.2.2 Preuves d’accessibilité . . . . . . . . . . . . . . . . . . . . 454 16.2.3 Construction de relations bien fondées . . . . . . . . . . . 455 16.2.4 Récursion bien fondée . . . . . . . . . . . . . . . . . . . . 456 16.2.5 Le récurseur well_founded_induction . . . . . . . . . . 456 16.2.6 Division euclidienne bien fondée . . . . . . . . . . . . . . 458 16.2.7 Récursion imbriquée . . . . . . . . . . . . . . . . . . . . . 461 16.3 ** Récursion générale par itération . . . . . . . . . . . . . . . . . 463 16.3.1 Fonctionnelle associée à une fonction récursive . . . . . . 463 16.3.2 Construction de la fonction cherchée . . . . . . . . . . . . 467 16.3.3 Démonstration de l’équation de point fixe . . . . . . . . . 467 16.3.4 Utilisation de l’équation de point fixe . . . . . . . . . . . 469 16.3.5 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . 469 16.4 *** Récursion sur un prédicat ad-hoc . . . . . . . . . . . . . . . . 470 17 * Démonstration par réflexion 477 17.1 Présentation générale . . . . . . . . . . . . . . . . . . . . . . . . . 477 17.2 Démonstrations par calcul direct . . . . . . . . . . . . . . . . . . 479 17.3 ** Démonstrations par calcul algébrique . . . . . . . . . . . . . . 482 17.3.1 Démonstrations modulo associativité . . . . . . . . . . . . 483 17.3.2 Abstraire sur le type et l’opérateur . . . . . . . . . . . . . 486 17.3.3 *** Tri de variables pour la commutativité . . . . . . . . . 489 17.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 492 Annexes 495 Tri par insertion : le code . . . . . . . . . . . . . . . . . . . . . . . . . 495 Index 499 Coq et bibliothèques . . . . . . . . . . . . . . . . . . . . . . . . . . . . 500 Exemples du livre . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 504 Les annotations de niveau : *, **, et *** apparaissant dans cette table des matières sont expliquées page 32.
Soyez le premier à déposer un commentaire !

17/1000 caractères maximum.