La lecture en ligne est gratuite
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres
Télécharger Lire

Le Coq’ Art (V8)

512 pages
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 . . . . . . . . . . . . . . . . . . . . . . . . . . . ...
Voir plus Voir moins

Vous aimerez aussi

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.
Un pour Un
Permettre à tous d'accéder à la lecture
Pour chaque accès à la bibliothèque, YouScribe donne un accès à une personne dans le besoin