, Une petite moitié de ce travail est constituée de manipulations élémentaires de formules sur les naturels. Il y a d'une part les petits lemmes de la bibliothèque et quelques lemmes locaux ne formalisant que des calculs numériques simples, d'autre part les nombreuses occurrences de tactiques comme
, Bien sûr ce n'est pas toujours simple et l'utilisateur comprend bien qu'il y a plusieurs façons d'unifier (S (S (S (plus t dt)))) avec (plus t' dt'), mais il aimerait avoir une façon plus commode de dire qu'il veut t':=(S (S t)) et dt':=(S dt) que d'appeler plusieurs règles de réécriture de plus et S. Le confort serait d'avoir un "apply" lié à un solveur d'équations (un peu ce qui existe dans PROLOG III de PrologIA) qui traduirait les unifications en contraintes, résoudrait celles qu'il saurait résoudre et placerait les autres en buts à prouver. Par contre, Coq permet une mise au point très fine de la preuve, Le but de ces manipulations est généralement de faire coïncider une expression paramètre du but avec l'expression correspondante de l'hypothèse ou du lemme que l'on veut appliquer
, ? l a vérification de tous les cas sans risque d'erreurs, dans la preuve du firing squad, il suffit de penser au nombre de fois que les tables de transitions ont été utilisées
, ? l a validation de modifications en cours de développement avec un minimum de travail lorsqu'une modification est faite sur un point déjà écrit, il suffit de repasser toutes les preuves postérieures à ce point pour savoir lesquelles sont concernées et vérifier ainsi sans risque d'oubli, que la suite du développement est encore valide
, Avec en plus, l'avantage de trouver sur le réseau la démonstration complète, de pouvoir la vérifier (reviewers), la comprendre et la réutiliser, Enfin, j'ai acquis la conviction que les logiciels d'aide à la preuve tels que Coq ont un champ d'utilisation comme langage universel de spécification de problème et d'écriture de preuves. Verra-t-on un jour fleurir les démonstrations "à la Coq" dans les papiers de mathématiques discrètes et d'informatique théorique comme on a vu fleurir les algorithmes
, Même en utilisant des noms mnémotechniques et des écritures les plus standardisées possibles, il est fréquent de rechercher le nom ou l'énoncé d'un lemme. L'outil "search" est certes parfois pratique, mais s'avère souvent trop rudimentaire. Un outil plus puissant serait apprécié
, Pourquoi choisir un assistant de preuves? Le fait d'avoir à suggérer des tactiques à Coq jusqu'à l'aboutissement de la preuve apparaît de prime abord comme un point faible par rapport aux véritables démonstrations automatiques. Après usage, la conclusion est plutôt inverse
, Mais l'usage habile de lemmes, ou la simple utilisation du couper-coller permet de ne pas répéter cette opération trop souvent. Par contre, le fait de rester le maître du processus de démonstration prend tout son intérêt dans l'échec. Une tentative de démontrer un lemme inexact ne peut aboutir, mais au fur et à mesure que les tactiques sont essayées, le point dur apparaît de plus en plus clairement permettant à l'utilisateur non seulement de se persuader de la fausseté de l'assertion mais en plus d'en percevoir la raison. L'utilisateur reçoit alors des informations précieuses pour poursuivre sa démonstration en modifiant son raisonnement. On note le confort qu'il y a eu dans cette longue preuve à laisser gérer toutes les petites conditions de longueur des figures par Coq. De même, les transitions, une fois écrites sont pratiquement oubliées, Certes, il est souvent fastidieux d'expliquer à Coq comment on démontre quelque chose qui nous semble facile, et la tentation est forte de ne pas trouver Coq bien intelligent
, Il faut bien se persuader que Coq ne peut servir à trouver une démonstration. Par contre, l'expressivité de son langage permet facilement d'écrire la preuve dès que l'idée de la démonstration est claire. D'une certaine façon, on peut dire que la preuve est à la démonstration ce que le programme est à l'algorithme : une formalisation rigoureuse
, Il y a d'ailleurs une grande similitude de méthodologie entre l'écriture d'une grosse preuve et celle d'un grand programme. Il faut commencer par une analyse rigoureuse, structurer sa preuve, éviter les noms passepartout et utiliser au contraire des dénominations précises, éviter les longues preuves et découper autant que faire se peut en petits lemmes
, Sequential machines, Selected Papers, pp.213-214, 1964.
, A six-state minimal time solution to the firing squad synchronization problem, Theoretical Computer Science, vol.50, pp.183-238, 1987.
, The Coq Proof Assistant Reference Manual, Version 5, vol.10
URL : https://hal.archives-ouvertes.fr/inria-00069994