Le Coq’ Art (V8)

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 . . . . . . . . . . . . . . . . . . . . . . . . . . . ...