Induction: Preuve par induction

La ligne suivante importe toutes les définitions du chapitre suivant.

Pour que ça marche, il faut compiler Basics.v en Basics.vo en utilisant coqc. (C'est la même chose que transformer un fichier .java en fichier .class, ou un .c en .o.) Voici deux façons de compiler votre code:

• CoqIDE:
  Ouvrir Basics.v. Dans le menu «Compile», clicker sur «Compile Buffer».
• Ligne de commande:
  Exécuter coqc Basics.v

Nommer les cas

Le fait qu'il n'y ait pas de commande explicite pour se déplacer d'une branche à l'autre d'un raisonnement par cas peut rendre les scripts de preuve bien difficiles à lire. Dans des preuves plus grosses, avec des raisonnements par cas imbriqués, il peut même être difficile de s'orienter en jouant la preuve avec Coq. (Imaginez-vous en train d'essayer de vous souvenir que les cinq premiers sous-buts font partie d'un raisonnement par cas intérieur et que les sept restant sont ce qui reste du raisonnement par cas extérieur...) Un usage discipliné de l'indentation et des commentaires peut aider, mais une meilleure solution est d'utiliser la tactique Case. Case n'est pas built in dans Coq : on doit le définir nous-mêmes. Il n'est pas nécessaire de comprendre comment ça marche -- vous pouvez simplement ignorer cette définition et passer à l'exemple qui suit. Elle utilise des possibilités de Coq que nous n'avons pas abordées -- la bibliothèque de chaînes de caractères (pour la syntaxe concrète des chaînes de caractères) et la commande Ltac, qui permet de définir des tactiques. Merci à Aaron Bohannon pour ce hack!

Voici un exemple d'utilisation de Case. Jouer la démonstration et observer les changements du contexte.

Case ne fait rien de difficile: elle ajoute simplement une chaîne de caractères qu'on choisit (étiquetée avec l'identifiant «Case») au contexte du but courant. Lorsque des sous-buts sont engendrés, cette chaîne de caractères reste présente dans leurs contextes. Lorsque le dernier de ces sous-buts est finalement démontré et que le but principal devient actif, cette chaîne de caractères disparaît du contexte, ce qui permet de voir facilement que le cas où on l'a introduite est fini. De plus, pour vérifier qu'on ne fait pas n'importe quoi, si on tente d'exécuter Case alors que la chaîne de caractères d'un précédent usage est encore dans le contexte, on obtient un message d'erreur clair. Pour les raisonnements par cas imbriqués (par exemple, quand on veut utiliser un destruct pour résoudre un but qui a lui-même été engendré par un destruct), on dispose d'une tactique SCase.

Exercice : 2 étoiles (andb_true_elim2)

Démontrer andb_true_elim2, en marquant les cas et sous-cas quand vous utilisez destruct.

☐ Il n'y a pas de règles figées quant au format des preuves en Coq -- en particulier, quand aller à la ligne et comment indenter les parties d'une preuve pour indiquer leur imbrication. Néanmoins, si on marque explicitement avec un Case en début de ligne tous les endroits où plusieurs sous-buts sont engendrés, alors la preuve sera lisible à peu près quels que soient les autres choix de typographie. C'est peut-être le bon moment pour mentionner un autre conseil (peut-être évident) sur la longueur des lignes. Les débutants ont tendance à être extrêmes, soit en n'utilisant qu'une ligne par tactique, soit en groupant chaque preuve sur une seule ligne. Le bon style est intermédiaire. En particulier, une convention raisonnable est de se limiter à des lignes de 80 caractères. Les lignes plus longues sont difficiles à lire et peuvent être gênantes à afficher et imprimer. De nombreux éditeurs savent forcer ce comportement.

Preuve par induction

On a démontré dans le chapitre précédent que 0 est neutre à gauche pour +, par un argument simple. Le fait qu'il soit aussi neutre à droite...

... ne se démontre pas si simplement. Appliquer reflexivity ne suffit pas: le n dans n + 0 est un entier arbitraire inconnu, donc le match dans la définition de + ne se simplifie pas.

Et raisonner par cas avec destruct n ne nous avance pas beaucoup: le cas où n=0 passe, mais dans le cas n = S n' pour un certain n', on reste bloqués exactement de la même manière. On pourrait utiliser destruct n' pour avancer d'encore un pas, mais comme n peut être arbitrairement grand, continuer comme ça ne nous mènera nulle part.

Pour démontrer de tels résultats -- et en fait pour démontrer la plupart des résultats intéressants sur les entiers, les listes et les autres ensembles définis par induction -- on a besoin d'un principe de raisonnement plus puissant : l' induction. Rappelez-vous le principe de récurrence sur les entiers naturels: si P (n) est une proposition mentionnant un entier naturel n et si on veut montrer que P est vérifiée pour tous les entiers n, on peut raisonner comme ceci :

• montrer que P (0) est vérifiée ;
• montrer que, pour tout n', si P(n') est vérifiée, alors P (S n') aussi ;
• conclure que P(n) est vérifiée pour tout n.

En Coq, les étapes sont les mêmes, mais on procède à l'envers: on commence par le but (prouver P(n) pour tout n) et on le sépare (en appliquant la tactique induction) en deux sous-buts: d'abord montrer P(0), puis montrer P (n') -> P (S n'). Voici comment ça marche pour le théorème qu'on est en train d'essayer de démontrer:

Comme destruct, la tactique induction accepte une clause as... qui spécifie les noms des variables à introduire dans les sous-buts. Dans le premier cas, n est remplacé par 0 et le but devient 0+0=0, qui se prouve par simplification. Dans le second cas, n est remplacé par S n' et l'hypothèse n'+0 = n' est ajoutée au contexte (avec le nom IHn', parce que c'est l'Hypothèse d'Induction pour n'). Le but devient dans ce cas (S n') + 0 = S n', qui se simplifie en S (n' + 0) = S n', ce qui découle de l'hypothèse d'induction.

Exercice : 2 étoiles (basic_induction)

Démontrer les lemmes suivants par induction. Vous pouvez avoir besoin de résultats précédents.

☐

Exercice : 2 étoiles (double_plus)

Considérons la fonction suivante, qui double son argument :

Utiliser l'induction pour démontrer ce résultat simple sur double :

☐

Exercice : 1 étoile (destruct_induction)

Expliquer brièvement la différence entre les tactiques destruct et induction. ☐

Preuves imbriquées

En Coq, comme en mathématiques informelles, les grosses démonstrations sont en général divisées en une suite de théorèmes, les démonstrations suivantes faisant référence aux théorèmes précédents. De temps en temps, néanmoins, une démonstration peut utiliser un fait trop facile (ou trop particulier) pour mériter un nom global. Dans de tels cas, il est confortable de pouvoir simplement énoncer et démontrer le sous-théorème désiré à l'endroit où on l'utilise. La tactique assert permet de faire ça. Par exemple, notre démonstration précédente du théorème mult_0_plus fait référence à un théorème antérieur nommé plus_0_n. On pourrait aussi utiliser assert pour énoncer et démontrer plus_0_n sur place:

La tactique assert introduit deux sous-buts. Le premier est l'assertion elle-même ; en la préfixant par H:, on nomme l'assertion H. (Observons qu'on pourrait aussi utiliser as, comme plus haut avec destruct et induction, c'est-à-dire assert (0+n=n) as H. Observons aussi qu'on marque la démonstration de l'assertion avec un Case, à la fois pour la lisibilité et pour pouvoir, lors de l'utilisation interactive de Coq, détecter facilement qu'on a fini de prouver l'assertion en observant que la chaîne de caractères "Proof of assertion" disparaît du contexte.) Le second but est le même qu'avant l'appel à assert, sauf que, dans le contexte, on a l'hypothèse H que 0+n=n. C'est-à-dire que assert engendre un sous-but où on doit prouver l'assertion et un autre où on peut utiliser l'assertion pour avancer dans ce qu'on était en train d'essayer de démontrer. En fait, assert va se révéler bien pratique dans de nombreuses situations. Par exemple, supposons qu'on veuille démontrer que (n + m) + (p + q) = (m + n) + (p + q). La seule différence entre les deux membres de l'égalité est que les arguments m et n de premier + interne sont échangés. On devrait donc pouvoir utiliser la commutativité de l'addition (plus_comm) pour récrire l'un en l'autre. Sauf que la tactique rewrite est un peu idiote quant au lieu où elle est censée récrire. Il y a trois usages de + ici et invoquer rewrite -> plus_comm ne modifie en fait que le plus externe.

On voudrait juste échanger n + m contre m + n... et plus_comm devrait marcher !

Ne marche pas... Coq récrit le mauvais +!

Pour appliquer plus_comm à l'endroit désiré, on peut introduire un lemme local disant que n + m = m + n (pour nos m et n particuliers), qu'on démontre en utilisant plus_comm, puis utiliser ce lemme pour effectuer la récriture souhaitée.

Exercice : 4 étoiles (mult_comm)

Utiliser assert pour démontrer ce théorème. Vous ne devriez pas avoir besoin d'induction.

Démontrer maintenant la commutativité de la multiplication. (Vous devrez probablement définir et démontrer un théorème auxiliaire.) Vous pourriez trouver plus_swap bien pratique.

☐

Exercice : 2 étoiles (evenb_n__oddb_Sn)

Démontrer le résultat facile suivant :

☐

Encore des exercices

Exercice : 3 étoiles

Prendre une feuille. Pour chacun des théorèmes suivants, commencer par réfléchir à (a) s'il se démontre par simplification et récriture, (b) s'il a aussi besoin d'un raisonnement par cas (destruct), ou (c) s'il a aussi besoin d'une induction. Écrire votre prédiction. Compléter ensuite la démonstration. (Il n'y a pas vraiment besoin de faire le coup de la feuille ; c'est juste pour vous encourager à réfléchir avant de hacker !)

☐

Exercice : 2 étoiles (beq_nat_refl)

☐

Exercice : 2 étoiles (plus_swap')

La tactique replace permet de spécifier un sous-terme particulier à récrire et en quoi on veut le récrire. Plus précisément, replace (t) with (u) remplaces (toutes les copies de) l'expression t dans le but par l'expression u, puis engendre t=u comme nouveau sous-but. Ceci est souvent utile quand un simple rewrite agit sur la mauvaise partie du but. Utiliser la tactique replace pour démontrer plus_swap', comme pour plus_swap mais sans avoir besoin de assert (n + m = m + n).

☐

Exercice : 3 étoiles (binary_commute)

Rappelez-vous les fonctions increment et binary-to-unary écrites pour l'exercice binary dans le chapitre Basics. Démontrer que ces fonctions commutent -- c'est-à-dire qu'incrémenter un entier binaire puis le convertir en unaire donne le même résultat que le convertir d'abord en unaire puis de l'incrémenter. (Avant de commencer à travailler sur cet exercice, vous êtes priés de copier les définitions de votre solution à l'exercice binary ici. Si vous souhaitez modifier vos définitions originales pour faciliter la démonstration, n'hésitez pas.)

☐

Exercice : 5 étoiles, avancé (binary_inverse)

Cet exercice poursuit l'exercice précédent sur les entiers binaires. Vous aurez besoin des définitions et théorèmes du précédent pour faire celui-ci. (a) D'abord, écrire une fonction pour convertir les entiers unaires en binaire. Démontrer ensuite que, en partant d'un entier unaire arbitraire, le convertir en binaire puis le reconvertir en unaire donne bien l'entier de départ. (b) On pourrait naturellement penser que ça marche aussi dans l'autre sens: partant d'un entier binaire, le convertir en unaire puis le reconvertir en binaire donne l'entier de départ. Mais c'est faux ! Expliquer le problème. (c) Définir une fonction normalize des entiers binaires dans eux-mêmes telle que pour tout entier binaire b, convertir b en unaire puis reconvertir le résultat en binaire donne (normalize b). Le démontrer. À nouveau, n'hésitez pas à modifier vos définitions précédentes si ça aide.

☐

Contenu avancé

Preuve formelle / informelle

«Les preuves informelles sont des algorithmes; les preuves formelles sont des programmes.» La question de ce qu'est précisément une «démonstration» d'un résultat mathématique a intrigué les philosophes pendant des millénaires. Une définition rapide et brutale pourrait néanmoins être: une démonstration d'une proposition mathématique P est un texte écrit (ou lu) qui transmet au lecteur ou à l'auditeur la certitude que P est vraie. C'est-à-dire qu'une démonstration est un acte de communication. Bon, mais les actes de communication peuvent impliquer plusieurs sortes de lecteurs. Par exemple, le «lecteur» peut être un programme comme Coq, auquel cas la «certitude» transmise est une simple vérification mathématique que P peut se déduire d'un certain ensemble de règles formelles de logique et la démonstration est une recette qui guide le programme dans cette vérification. De telles recettes sont des preuves formelles. Alternativement, le lecteur peut être un humain, auquel cas la preuve sera écrite en français, ou dans une autre langue, et donc forcément informelle. Ici, les critères de succès sont moins clairs. Une démonstration est «bonne» si elle amène le lecteur à croire P. Mais la même démonstration peut être lue par des lecteurs très différents, dont certains peuvent être convaincus par une formulation particulière du raisonnement, alors que d'autres ne le sont pas. Tel lecteur peut être particulièrement pédant ou inexpérimenté ; le seul moyen de le convaincre sera de détailler le raisonnement à l'extrême. Mais tel autre lecteur, plus familier avec la discipline, pourra crouler sous tous ces détails et perdre le fil de la démonstration. Tout ce qu'un tel lecteur attendra est qu'on lui explique les idées principales, parce qu'il lui sera plus facile de retrouver le reste par lui-même. Au final, il n'y a pas de standard universel, parce qu'aucune formulation de démonstration informelle ne peut à coup sûr convaincre tous les lecteurs imaginables. En pratique, toutefois, les mathématiciens ont développé un ensemble de conventions et d'idiomes assez riche pour parler d'objets mathématiques complexes, qui, au sein d'une certaine communauté, rend la communication relativement fiable. Les conventions de cette forme stylisée de communication donnent un standard plutôt clair pour juger les bonnes et les mauvaises démonstrations. Comme nous utilisons Coq dans ce cours, nous allons travailler essentiellement avec des démonstrations formelles. Mais cela ne signifie pas qu'on peut ignorer les démonstrations informelles ! Les démonstrations formelles sont utiles pour plusieurs raisons, mais certainement pas pour communiquer entre humains. Par exemple, voici une démonstration que l'addition est associative :

Coq est tout-à-fait satisfait de cette démonstration. Pour un humain, toutefois, il est difficile d'en retirer quoi que ce soit. Quelqu'un de familier avec Coq peut sans doute lire les tactiques l'une après l'autre et deviner l'état du contexte et de la pile de buts à chaque endroit, mais si la démonstration était ne serait-ce qu'un tout petit peu plus compliquée, ça deviendrait presque impossible. Au lieu de ça, un mathématicien pourrait l'écrire comme ceci :

• Théorème : pour tous n, m et p, n + (m + p) = (n + m) + p.
  Démonstration : par induction sur n.
  • D'abord, supposons n = 0. On doit montrer 0 + (m + p) = (0 + m) + p. Cela découle directement de la définition de +.
  • Ensuite, supposons n = S n' et n' + (m + p) = (n' + m) + p. On doit montrer (S n') + (m + p) = ((S n') + m) + p. Par définition de +, ceci est une conséquence de S (n' + (m + p)) = S ((n' + m) + p), qui est immédiat par hypothèse d'induction. ☐

La forme globale de la démonstration est en gros semblable. Ce n'est pas une coïncidence : Coq est conçu pour que sa tactique induction engendre les mêmes sous-buts, dans le même ordre, que les étapes qu'un mathématicien écrirait. Cependant, il y a des différences significatives dans le niveau de détail : la démonstration formelle est beaucoup plus explicite par certains côtés (par exemple, l'utilisation de reflexivity) mais beaucoup moins par d'autres (en particulier, l'«état» de la preuve à chaque endroit du script Coq est entièrement implicite, alors que la démonstration informelle en rappelle des bouts au lecteur plusieurs fois). Voici une démonstration formelle montrant plus clairement la structure :

Exercice : 2 étoiles, avancé (plus_comm_informal)

Traduire votre solution à plus_comm en une démonstration informelle. Thèorème: l'addition est commutative. Démonstration: ☐

Exercice : 2 étoiles (beq_nat_refl_informal)

Écrire une démonstration informelle du théorème suivant, en utilisant la démonstration informelle de plus_assoc comme modèle. Ne pas se contenter de paraphraser les tactiques Coq ! Théorème: true = beq_nat n n pour tout n. Démonstration: ☐