Le Coq’ Art (V8)

Informations

• Publié par: mtoledan
• Publié le: 11 octobre 2011
• Nombre de lectures: 49
• Langue: Français
• Poids de l'ouvrage: 2 Mo

Extrait

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 v