Listes : travail avec des données structurées

Paires d'entiers

Dans une définition de type avec Inductive, chaque constructeur peut prendre un nombre arbitraire d'arguments -- aucun (comme avec true et O), un (comme avec S), ou plus d'un, comme avec cette définition :

On peut comprendre cette déclaration comme: «il y a un seul moyen de construire une paire d'entiers : appliquer le constructeur pair à deux arguments de type nat». On peut construire un élément de natprod comme ceci :

Voici deux définitions de fonctions simples pour extraire la première et la seconde composante d'une paire. (Les définitions illustrent aussi le raisonnement par cas pour des constructeurs à deux arguments.)

Puisque les paires sont utilisées souvent, il est utile de pouvoir les écrire avec la notation mathématique standard (x,y) plutôt que pair x y. On peut demander à Coq de permettre cela par une déclaration Notation.

La nouvelle notation fonctionne aussi bien dans les expressions que dans les raisonnements par cas (en fait, on l'a déjà utilisée dans le chapitre précédent -- cette notation fait partie de la bibliothèque standard) :

Essayons de démontrer quelques résultats simples sur les paires. Si nous énonçons les lemmes de manière adéquate (et un peu bizarre), on peut les démontrer par réflexivité (et la simplification qui va automatiquement avec) :

Observons que reflexivity ne suffit pas si on énonce le résultat plus naturellement :

Ne simplifie rien du tout !

Il nous faut exposer la structure de p pour que simpl puisse raisonner par cas dans fst et snd. On fait ceci avec destruct. Observons que, contrairement au cas des nats (les éléments de type nat), destruct ne génère pas ici de sous-but supplémentaire. La raison en est que les natprods ne peuvent être construits que d'une seule manière.

Observons aussi au passage que Coq nous permet d'utiliser la notation introduite pour les paires dans le filtre «as...» qui nomme les variables introduites.

Exercice : 1 étoile (snd_fst_is_swap)

☐

Exercice : 1 étoile (fst_swap_is_snd)

☐

Listes de nombres

En généralisant légèrement la définition des paires, on peut décrire le type des listes d'entiers en disant: «une liste est soit la liste vide, soit une paire d'un entier et d'une autre liste».

Par exemple, voici une liste à trois éléments :

Comme pour les paires, il est plus confortable de noter les listes de manière plus proche de la programmation. Les deux déclarations suivantes permettent d'utiliser, pour construire des listes, :: comme un opérateur cons infixe et les crochets comme une notation «extrafixe».

Il n'est pas nécessaire de comprendre ces déclarations dans le détail, mais voici plus de détails pour le lecteur intéressé. L'annotation right associativity indique à Coq comment parenthéser les expressions comprenant plusieurs occurrences de ::. Ainsi, par exemple, les trois déclarations suivantes dénotent exactement la même chose:

L'annotation at level 60 dit à Coq comment parenthéser des expressions comprenant à la fois :: et un autre opérateur infixe. Par exemple, on a défini de la même manière une notation infixe pour + au niveau 50, Notation "x + y" := (plus x y) (at level 50, left associativity). L'opérateur + sera prioritaire devant ::, de sorte que 1 + 2 :: [3] sera compris, comme prévu, comme (1 + 2) :: [3], plutôt que 1 + (2 :: [3]). (Au passage, notons que des expressions telles que «1 + 2 :: [3]» peuvent paraître étranges quand on les lit dans un fichier .v. Les crochets intérieurs, autour de 3, indiquent une liste, alors que les crochets extérieurs, qui sont invisibles dans l'affichage HTML, ont pour rôle d'indiquer à l'outil «coqdoc» que la partie entre crochets doit être affichée comme du code Coq plutôt que comme du texte.) Les deuxième et troisième déclarations Notation ci-dessus introduisent la notation avec crochets standard pour les listes; le membre droit de la troisième illustre la syntaxe de Coq pour déclarer des notations n-aires et les traduires en suites imbriquées de constructeurs binaires. Un certains nombres de fonctions sont très utiles pour manipuler des listes. Par exemple, la fonction repeat attend deux entiers n et count et renvoie une liste de longueur count où chaque élément est n.

La fonction length calcule la longueur d'une liste.

La fonction app («append», i.e., «ajouter à la fin») concatène deux listes.

En fait, on va beaucoup utiliser app dans ce qui suit; il sera donc confortable d'avoir une notation infixe.

Exercice : 2 étoiles (list_funs)

Compléter les définitions de nonzeros, oddmembers et countoddmembers ci-dessous. Jeter un oeil aux tests pour comprendre ce que doivent faire ces fonctions.

☐

Exercice : 3 étoiles (alternate)

Compléter la définition de alternate, qui "zippe" deux listes en une, en prenant les éléments alternativement dans la première et la seconde liste. Voir les tests ci-dessous pour des exemples. Note : une façon naturelle et élégante d'écrire alternate va échouer à satisfaire la contrainte de Coq imposant que toute définition Fixpoint doit "terminer trivialement". Si vous vous trouvez dans ce cas, cherchez une solution légèrement plus verbeuse qui considère les éléments des deux listes en même temps. (Une solution possible demande la définition d'un nouveau type de paires, mais ce n'est pas la seule façon de faire).

☐

Sacs par les listes

Un bag (ou multiset, pour «multi-ensemble») est une sorte d'ensemble, où les éléments peuvent apparaître plusieurs fois. Une implantation raisonnable des sacs consiste à représenter un sac d'entiers comme une liste.

Exercice : 3 étoiles (bag_functions)

Compléter les définitions suivantes des fonctions count, sum, add et member pour les sacs.

Toutes ces démonstrations peuvent se faire par reflexivity.

La somme (sum) de multi-ensembles est similaire à l'union d'ensembles : sum a b contient les éléments de a et de b. (Les mathématiciens ont tendance à définir l'union de multi-ensemble un peu différemment, ce qui nous pousse à utiliser un autre nom.) Pour la somme, nous vous fournissons un type qui ne nomme pas explicitement les arguments. De plus, il utilise le mot-clef Definition plutôt que Fixpoint, donc même si les arguments étaient nommés, vous ne pourriez pas les utiliser récursivement. Nous posons la question de cette manière pour vous encourager à vous demander si sum peut se définir autrement -- éventuellement en utilisant des fonctions définies précédemment.

☐

Exercice : 3 étoiles, (bag_more_functions)

Voilà d'autres fonctions sur les sacs pour vous exercer.

☐

Exercice : 3 étoiles (bag_theorem)

Énoncer un théorème non trivial sur les sacs concernant les fonctions count et add, puis le démontrer. Bien sûr, puisque cet exercice est très ouvert, il se peut que la démonstration de votre théorème requière des techniques non encore apprises. N'hésitez pas à demander de l'aide si vous êtes coincé!

☐

Raisonner sur les listes

Comme avec les entiers, certains résultats simples sur les listes se démontrent entièrement par simplification. Par exemple, la simplification effectuée par reflexivity suffit pour ce théorème...

... parce que le [] est substitué dans la définition de app de sorte que le match peut choisir le bon cas. De même, comme avec les entiers, il peut être utile de raisonner par cas sur les formes possibles (vide ou pas) d'une liste inconnue.

Ici, le cas nil fonctionne parce que nous avons choisi de définir tail nil = nil. Observons que l'annotation as de la tactique destruct introduit ici deux noms, n et l', parce que le constructeur de listes cons attend deux arguments (la tête et la queue de la liste qu'il construit). Néanmoins, les résultats intéressants sur les listes requièrent souvent des démonstrations par induction.

Micro-Sermon

Se contenter de lire les exemples de démonstrations ne vous mènera pas loin! Il est très important de toutes les travailler en détail avec Coq, en réfléchissant pour comprendre ce que chaque étape de la démonstration fait réellement. Sans cela, il est plus ou moins garanti que les exercices ci-dessous ne feront pas sens pour vous.

Induction sur les listes

Les démonstrations par induction sur les types de données comme natlist vous sont peut-être un peu moins familières que celles par récurrence standard sur les entiers, mais l'idée de base est tout aussi simple. Chaque déclaration Inductive définit un ensemble de valeurs construites à partir des constructeurs correspondants : un booléen peut être soit true, soit false; un entier peut être soit O, soit S appliqué à un entier; une liste peut être soit nil, soit cons appliqué à un entier et une liste. De plus, appliquer certains constructeurs à d'autres est la seule forme possible que peuvent prendre les éléments d'un ensemble défini inductivement: soit un nombre est 0, soit c'est S appliqué à un entier plus petit; une liste est soit nil, soit cons appliqué à un entier et une liste plus petite; etc... Ainsi, si on pense à une proposition P mentionnant une liste l et qu'on veut démontrer que P est vérifiée pour toutes les listes, on peut raisonner comme ceci:

• D'abord, montrer que P est vérifiée pour l lorsque l est nil.
• Ensuite, montrer que P est vérifiée pour l lorsque l est de la forme cons n l', pour un entier n et une liste l' plus petite que l, vérifiant elle-même P.

Puisque les listes ne peuvent être construites qu'à partir de listes plus petites, on finit par atteindre nil et les deux points ci-dessus suffisent à établir que P est vérifiée pour toute liste l. Voici un exemple concret:

Encore une fois, cette démonstration Coq n'est pas particulièrement éclairante en tant que document écrit statique -- elle est plus facile à lire en la parcourant dans une session Coq interactive, dans laquelle on voit le but et le contexte courants à chaque étape, mais cet état n'est pas visible dans la partie écrite de la démonstration Coq. Ainsi, une démonstration en langue naturelle -- écrite pour des lecteurs humains -- devra ajouter des «panneaux de signalisation»; en particulier, le lecteur s'orientera plus facilement si on lui rappelle explicitement l'hypothèse d'induction dans le second cas. Théorème: Pour toutes listes l1, l2 et l3, (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3). Démonstration: Par induction sur l1.

• D'abord, supposons l1 = []. On doit montrer (☐ ++ l2) ++ l3 = ☐ ++ (l2 ++ l3), qui découle directement de la définition de ++.
• Supposons ensuite l1 = n::l1' et (l1' ++ l2) ++ l3 = l1' ++ (l2 ++ l3) (l'hypothèse d'induction). On doit montrer ((n :: l1') ++ l2) ++ l3 = (n :: l1') ++ (l2 ++ l3).

]] Par définition de ++, ceci est une conséquence de n :: ((l1' ++ l2) ++ l3) = n :: (l1' ++ (l2 ++ l3)), qui est immédiat par hypothèse d'induction. ☐ Voici un exemple similaire à faire ensemble en classe:

Voyons maintenant un exemple un peu plus difficile de démonstration inductive sur les listes. Définissons une fonction «cons à droite», snoc, comme ceci :

et utilisons-la pour définir une fonction rev de renversement de listes, comme ceci :

Prouvons maintenant d'autres théorèmes sur les listes utilisant nos nouvelles fonctions snoc et rev. Un résultat moins évident que les démonstrations inductives vues jusqu'ici est que renverser une liste ne change pas sa longueur. Notre premier essai bloque dans le cas successeur ...

On va donc démontrer l'équation sur snoc qui nous manquait, comme un résultat intermédiaire.

On peut maintenant achever la démonstration originale.

Pour comparer, voici des démonstrations informelles de ces deux théorèmes : Théorème : pour tout entier n et toute liste l, length (snoc l n) = S (length l). Démonstration : par induction sur l.

• D'abord, supposons l = []. On doit montrer length (snoc ☐ n) = S (length ☐), qui découle directement des définitions de length et snoc.
• Ensuite, supposons l = n'::l' et length (snoc l' n) = S (length l'). On doit montrer length (snoc (n' :: l') n) = S (length (n' :: l')). Par définition de length et snoc, ceci est une conséquence de S (length (snoc l' n)) = S (S (length l')),

]] qui est immédiat par hypothèse d'induction. ☐ Théorème : pour toute liste l, length (rev l) = length l. Démonstration : par induction sur l.

• D'abord, supposons l = []. On doit montrer length (rev ☐) = length ☐, qui est une conséquence directe des définitions de length et rev.
• Ensuite, supposons l = n::l' ent length (rev l') = length l'. On doit montrer length (rev (n :: l')) = length (n :: l'). Par définition de rev, ceci est une conséquence de length (snoc (rev l') n) = S (length l') qui, par le lemme précédent, revient à S (length (rev l')) = S (length l'). Ceci est immédiat par hypothèse d'induction. ☐

Bien sûr, ces démonstrations sont écrites dans un style alambiqué et pédant. Après quelques démonstrations dans ce style, on trouvera sans doute plus facile de donner moins de détails (puisqu'on peut facilement les retrouver mentalement ou sur brouillon si nécessaire), en se contentant de mettre en avant les étapes non-triviales. En style compressé, la démonstration ci-dessus pourrait ressembler à ça : Théorème : pour toute liste l, length (rev l) = length l. Démonstration : d'abord, observons que length (snoc l n) = S (length l) pour tout l, ce qui se démontre facilement par induction sur l. Le résultat principal découle ensuite d'une autre induction facile sur l, utilisant, dans le cas où l = n' :: l', l'observation ci-dessus, associée à l'hypothèse d'induction. ☐ Le choix du style doit dépendre du degré de familiarité du lecteur avec le genre de démonstrations en question et les techniques utilisées. Le style plus pédant sera ici utilisé par défaut.

SearchAbout

Nous avons vu que les démonstrations peuvent utiliser des théorèmes prouvés précédemment, grâce à la tactique rewrite. Nous verrons plus tard d'autres manières d'utiliser des théorèmes précédents. Mais pour faire référence à un théorème, il faut connaître son nom. Or, il semble difficile de se rappeler les noms de tous les théorèmes qu'on peut éventuellement vouloir utiliser un jour ! Il est même souvent difficile de se rappeler quels théorèmes on a prouvé, beaucoup plus que leurs noms. La commande Coq SearchAbout est très utile pour résoudre ce problème. Taper SearchAbout bidule affiche une liste de tous les théorèmes concernant bidule. Par exemple, essayez de décommenter la ligne suivante pour obtenir une liste de théorèmes déjà prouvés sur rev :

Gardez SearchAbout en tête lors des exercices suivants et dans le reste du cours; cela peut vous faire gagner beaucoup de temps ! De plus, si vous utilisez ProofGeneral, vous pouvez exécuter SearchAbout en tapant C-c C-a C-a. Coller le résultat dans votre buffer se fait en tapant C-c C-;.

Exercices sur les listes, partie 1

Exercice : 3 étoiles (list_exercises)

Un peu d'entraînement avec les listes.

L'exercice suivant admet une solution courte. Si vous vous trouvez empêtré, revenez en arrière et essayez de faire plus simple.

Un exercice sur votre implantation de nonzeros :

☐

Exercices sur les listes, partie 2

Exercice : 2 étoiles (list_design)

Exercice de conception :

• Énoncer un théorème non-trivial mentionnant cons (::), snoc et app (++).
• Le démontrer.

☐

Exercice : 3 étoiles, avancé (bag_proofs)

Voici deux petits théorèmes sur vos définitions sur les sacs dans le problème précédent.

Le résultat suivant sur ble_nat pourrait vous servir dans la démonstration d'après.

☐

Exercice : 3 étoiles (bag_count_sum)

Énoncer un théorème non-trivial sur les sacs mentionnant les fonctions count et sum, puis le démontrer.

☐

Exercice : 4 étoiles, avancé (rev_injective)

Démontrer que la fonction rev est injective, c'est-à-dire : forall (l1 l2 : natlist), rev l1 = rev l2 -> l1 = l2. Cet exercice admet une solution simple et une autre plus difficile.

☐

Options

On considère maintenant une autre définition de type qui sert beaucoup en programmation :

Il est standard d'utiliser natoption comme un moyen d'écrire des fonctions renvoyant des «codes d'erreur». Par exemple, supposons qu'on veuille écrire une fonction renvoyant le nème élément d'une liste. Si on lui donne le type nat -> natlist -> nat, alors on devra renvoyer un entier même lorsque la liste sera trop courte!

Si on lui donne plutôt le type nat -> natlist -> natoption, alors on peut renvoyer None quand la liste est trop courte et Some a quand elle est assez longue et contient a comme nème élément.

Cet exemple est aussi l'occasion de présenter une nouvelle petite construction de Coq: les expressions conditionnelles ...

Les conditionnelles de Coq sont exactement comme dans les autres langages, avec une petite généralisation. Comme le type booléen n'est pas built in, Coq accepte en fait les conditionnelles sur n'importe quel type inductif à deux constructeurs. La condition est considérée comme vraie si elle s'évalue en le premier constructeur et comme fausse sinon. La fonction ci-dessous extrait le nat d'une natoption et renvoie un défaut fourni en argument dans le cas None.

Exercice : 2 étoiles (hd_opt)

Dans la même veine, modifier la fonction hd précédente pour qu'on n'ait pas à lui passer une valeur par défaut pour le cas nil.

☐

Exercice : 1 étoile (option_elim_hd)

Cet exercice relie votre nouvelle fonction hd_opt à l'ancienne hd.

☐

Exercice : 2 étoiles (beq_natlist)

Compléter la définition de beq_natlist, qui teste l'égalité de listes d'entiers. Démontrer que beq_natlist l l renvoie true pour toute liste l.

☐

Dictionnaires

Voici une dernière illustration de la construction de structures de données fondamentales en Coq, la déclaration d'un type de données dictionary simple, utilisant les entiers à la fois comme clefs et comme valeurs à stocker. (C'est-à-dire qu'un dictionnaire représente une fonction finie des entiers vers les entiers.)

Cette déclaration peut se comprendre comme: «il y a deux moyens de construire un dictionary : soit en utilisant le constructeur empty pour représenter un dictionnaire vide, soit en appliquant le constructeur record à une clef, une valeur et un dictionary existant pour construire un dictionary avec une association clef-valeur de plus».

Voici une fonction find qui parcourt un dictionary en recherchant une clef donnée. Elle renvoie None si la clef n'est pas trouvée et Some val si la clef est associée à la valeur val dans le dictionnaire. Si la même clef est associée à plusieurs valeurs, find renvoie la première qu'elle trouve.

Exercice : 1 étoile (dictionary_invariant1)

Compléter la démonstration suivante.

☐

Exercice : 1 étoile (dictionary_invariant2)

Compléter la démonstration suivante.

☐