Lists

Listes: travail avec des données structurées


Require Export Induction.

Module NatList.

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:

Inductive natprod : Type :=
  pair : nat nat natprod.

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:

Check (pair 3 5).

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

Definition fst (p : natprod) : nat :=
  match p with
  | pair x yx
  end.
Definition snd (p : natprod) : nat :=
  match p with
  | pair x yy
  end.

Eval simpl in (fst (pair 3 5)).
(* ===> 3 *)

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.

Notation "( x , y )" := (pair x y).

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):

Eval simpl in (fst (3,5)).

Definition fst' (p : natprod) : nat :=
  match p with
  | (x,y) ⇒ x
  end.
Definition snd' (p : natprod) : nat :=
  match p with
  | (x,y) ⇒ y
  end.

Definition swap_pair (p : natprod) : natprod :=
  match p with
  | (x,y) ⇒ (y,x)
  end.

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):

Theorem surjective_pairing' : (n m : nat),
  (n,m) = (fst (n,m), snd (n,m)).
Proof.
  reflexivity. Qed.

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

Theorem surjective_pairing_stuck : (p : natprod),
  p = (fst p, snd p).
Proof.
  simpl. (* Ne simplifie rien du tout! *)
Abort.

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.

Theorem surjective_pairing : (p : natprod),
  p = (fst p, snd p).
Proof.
  intros p. destruct p as (n,m). simpl. reflexivity. Qed.

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.

Exercise: 1 star (snd_fst_is_swap)

Theorem snd_fst_is_swap : (p : natprod),
  (snd p, fst p) = swap_pair p.
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 1 star, optional (fst_swap_is_snd)

Theorem fst_swap_is_snd : (p : natprod),
  fst (swap_pair p) = snd p.
Proof.
  (* FILL IN HERE *) Admitted.

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

Inductive natlist : Type :=
  | nil : natlist
  | cons : nat natlist natlist.

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

Definition mylist := cons 1 (cons 2 (cons 3 nil)).

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

Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..).

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:

Definition mylist1 := 1 :: (2 :: (3 :: nil)).
Definition mylist2 := 1 :: 2 :: 3 :: nil.
Definition mylist3 := [1,2,3].

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.

Fixpoint repeat (n count : nat) : natlist :=
  match count with
  | Onil
  | S count'n :: (repeat n count')
  end.

La fonction length calcule la longueur d'une liste.

Fixpoint length (l:natlist) : nat :=
  match l with
  | nilO
  | h :: tS (length t)
  end.

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

Fixpoint app (l1 l2 : natlist) : natlist :=
  match l1 with
  | nill2
  | h :: th :: (app t l2)
  end.

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

Notation "x ++ y" := (app x y)
                     (right associativity, at level 60).

Example test_app1: [1,2,3] ++ [4,5] = [1,2,3,4,5].
Proof. reflexivity. Qed.
Example test_app2: nil ++ [4,5] = [4,5].
Proof. reflexivity. Qed.
Example test_app3: [1,2,3] ++ nil = [1,2,3].
Proof. reflexivity. Qed.

Definition hd (default:nat) (l:natlist) : nat :=
  match l with
  | nildefault
  | h :: th
  end.

Definition tail (l:natlist) : natlist :=
  match l with
  | nilnil
  | h :: tt
  end.

Example test_hd1: hd 0 [1,2,3] = 1.
Proof. reflexivity. Qed.
Example test_hd2: hd 0 [] = 0.
Proof. reflexivity. Qed.
Example test_tail: tail [1,2,3] = [2,3].
Proof. reflexivity. Qed.

Exercise: 2 stars (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.

Fixpoint nonzeros (l:natlist) : natlist :=
  (* FILL IN HERE *) admit.

Example test_nonzeros: nonzeros [0,1,0,2,3,0,0] = [1,2,3].
 (* FILL IN HERE *) Admitted.

Fixpoint oddmembers (l:natlist) : natlist :=
  (* FILL IN HERE *) admit.

Example test_oddmembers: oddmembers [0,1,0,2,3,0,0] = [1,3].
 (* FILL IN HERE *) Admitted.

Fixpoint countoddmembers (l:natlist) : nat :=
  (* FILL IN HERE *) admit.

Example test_countoddmembers1: countoddmembers [1,0,3,1,4,5] = 4.
 (* FILL IN HERE *) Admitted.
Example test_countoddmembers2: countoddmembers [0,2,4] = 0.
 (* FILL IN HERE *) Admitted.
Example test_countoddmembers3: countoddmembers nil = 0.
 (* FILL IN HERE *) Admitted.

Exercise: 3 stars, advanced (alternate)

Complete the definition of alternate, which "zips up" two lists into one, alternating between elements taken from the first list and elements from the second. See the tests below for more specific examples.
Note: one natural and elegant way of writing alternate will fail to satisfy Coq's requirement that all Fixpoint definitions be "obviously terminating." If you find yourself in this rut, look for a slightly more verbose solution that considers elements of both lists at the same time. (One possible solution requires defining a new kind of pairs, but this is not the only way.)

Fixpoint alternate (l1 l2 : natlist) : natlist :=
  (* FILL IN HERE *) admit.

Example test_alternate1: alternate [1,2,3] [4,5,6] = [1,4,2,5,3,6].
 (* FILL IN HERE *) Admitted.
Example test_alternate2: alternate [1] [4,5,6] = [1,4,5,6].
 (* FILL IN HERE *) Admitted.
Example test_alternate3: alternate [1,2,3] [4] = [1,4,2,3].
 (* FILL IN HERE *) Admitted.
Example test_alternate4: alternate [] [20,30] = [20,30].
 (* FILL IN HERE *) Admitted.

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.

Definition bag := natlist.

Exercise: 3 stars (bag_functions)

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

Fixpoint count (v:nat) (s:bag) : nat :=
  (* FILL IN HERE *) admit.

Toutes ces démonstrations peuvent se faire par reflexivity.

Example test_count1: count 1 [1,2,3,1,4,1] = 3.
 (* FILL IN HERE *) Admitted.
Example test_count2: count 6 [1,2,3,1,4,1] = 0.
 (* FILL IN HERE *) Admitted.

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.

Definition sum : bag bag bag :=
  (* FILL IN HERE *) admit.

Example test_sum1: count 1 (sum [1,2,3] [1,4,1]) = 3.
 (* FILL IN HERE *) Admitted.

Definition add (v:nat) (s:bag) : bag :=
  (* FILL IN HERE *) admit.

Example test_add1: count 1 (add 1 [1,4,1]) = 3.
 (* FILL IN HERE *) Admitted.
Example test_add2: count 5 (add 1 [1,4,1]) = 0.
 (* FILL IN HERE *) Admitted.

Definition member (v:nat) (s:bag) : bool :=
  (* FILL IN HERE *) admit.

Example test_member1: member 1 [1,4,1] = true.
 (* FILL IN HERE *) Admitted.
Example test_member2: member 2 [1,4,1] = false.
 (* FILL IN HERE *) Admitted.

Exercise: 3 stars, optional (bag_more_functions)

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

Fixpoint remove_one (v:nat) (s:bag) : bag :=
  (* Appliquer remove_one à un sac ne contenant pas l'entier à enlever, on renvoie le sac sans le modifier. *)
  (* FILL IN HERE *) admit.

Example test_remove_one1: count 5 (remove_one 5 [2,1,5,4,1]) = 0.
 (* FILL IN HERE *) Admitted.
Example test_remove_one2: count 5 (remove_one 5 [2,1,4,1]) = 0.
 (* FILL IN HERE *) Admitted.
Example test_remove_one3: count 4 (remove_one 5 [2,1,4,5,1,4]) = 2.
 (* FILL IN HERE *) Admitted.
Example test_remove_one4:
  count 5 (remove_one 5 [2,1,5,4,5,1,4]) = 1.
 (* FILL IN HERE *) Admitted.

Fixpoint remove_all (v:nat) (s:bag) : bag :=
  (* FILL IN HERE *) admit.

Example test_remove_all1: count 5 (remove_all 5 [2,1,5,4,1]) = 0.
 (* FILL IN HERE *) Admitted.
Example test_remove_all2: count 5 (remove_all 5 [2,1,4,1]) = 0.
 (* FILL IN HERE *) Admitted.
Example test_remove_all3: count 4 (remove_all 5 [2,1,4,5,1,4]) = 2.
 (* FILL IN HERE *) Admitted.
Example test_remove_all4: count 5 (remove_all 5 [2,1,5,4,5,1,4,5,1,4]) = 0.
 (* FILL IN HERE *) Admitted.

Fixpoint subset (s1:bag) (s2:bag) : bool :=
  (* FILL IN HERE *) admit.

Example test_subset1: subset [1,2] [2,1,4,1] = true.
 (* FILL IN HERE *) Admitted.
Example test_subset2: subset [1,2,2] [2,1,4,1] = false.
 (* FILL IN HERE *) Admitted.

Exercise: 3 stars (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é!

(* FILL IN HERE *)

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

Theorem nil_app : l:natlist,
  [] ++ l = l.
Proof. reflexivity. Qed.

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

Theorem tl_length_pred : l:natlist,
  pred (length l) = length (tail l).
Proof.
  intros l. destruct l as [| n l'].
  Case "l = nil".
    reflexivity.
  Case "l = cons n l'".
    reflexivity. Qed.

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:

Theorem app_ass : l1 l2 l3 : natlist,
  (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof.
  intros l1 l2 l3. induction l1 as [| n l1'].
  Case "l1 = nil".
    reflexivity.
  Case "l1 = cons n l1'".
    simpl. rewrite IHl1'. reflexivity. Qed.

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:

Theorem app_length : l1 l2 : natlist,
  length (l1 ++ l2) = (length l1) + (length l2).
Proof.
  (* WORKED IN CLASS *)
  intros l1 l2. induction l1 as [| n l1'].
  Case "l1 = nil".
    reflexivity.
  Case "l1 = cons".
    simpl. rewrite IHl1'. reflexivity. Qed.

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

Fixpoint snoc (l:natlist) (v:nat) : natlist :=
  match l with
  | nil ⇒ [v]
  | h :: th :: (snoc t v)
  end.

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

Fixpoint rev (l:natlist) : natlist :=
  match l with
  | nilnil
  | h :: tsnoc (rev t) h
  end.

Example test_rev1: rev [1,2,3] = [3,2,1].
Proof. reflexivity. Qed.
Example test_rev2: rev nil = nil.
Proof. reflexivity. Qed.

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

Theorem rev_length_firsttry : l : natlist,
  length (rev l) = length l.
Proof.
  intros l. induction l as [| n l'].
  Case "l = []".
    reflexivity.
  Case "l = n :: l'".
    (* C'est le cas difficile. Commençons comme d'habitude par simplifier. *)
    simpl.
    (* On dirait bien qu'on est coincés: le but est une égalité sur
    snoc, mais on n'a aucune équation sur snoc, ni dans le
    contexte ni dans l'environnement global!

    Nous pouvons avancer un peu en utilisant l'hypothèse d'induction
    pour récrire le but... *)

    rewrite IHl'.
    (* ... mais ensuite on est vraiment bloqués. *)
Abort.

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

Theorem length_snoc : n : nat, l : natlist,
  length (snoc l n) = S (length l).
Proof.
  intros n l. induction l as [| n' l'].
  Case "l = nil".
    reflexivity.
  Case "l = cons n' l'".
    simpl. rewrite IHl'. reflexivity. Qed.

On peut maintenant achever la démonstration originale.

Theorem rev_length : l : natlist,
  length (rev l) = length l.
Proof.
  intros l. induction l as [| n l'].
  Case "l = nil".
    reflexivity.
  Case "l = cons".
    simpl. rewrite length_snoc.
    rewrite IHl'. reflexivity. Qed.

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 lectorat 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:

(* SearchAbout 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-;.

Exercises sur les listes, partie 1

Exercise: 3 stars (list_exercises)

Un peu d'entraînement avec les listes.

Theorem app_nil_end : l : natlist,
  l ++ [] = l.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem rev_involutive : l : natlist,
  rev (rev l) = l.
Proof.
  (* FILL IN HERE *) Admitted.

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

Theorem app_ass4 : l1 l2 l3 l4 : natlist,
  l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem snoc_append : (l:natlist) (n:nat),
  snoc l n = l ++ [n].
Proof.
  (* FILL IN HERE *) Admitted.

Theorem distr_rev : l1 l2 : natlist,
  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
Proof.
  (* FILL IN HERE *) Admitted.

Un exercice sur votre implantation de nonzeros:

Lemma nonzeros_app : l1 l2 : natlist,
  nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
Proof.
  (* FILL IN HERE *) Admitted.

Exercices sur les listes, partie 2

Exercise: 2 stars (list_design)

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

(* FILL IN HERE *)

Exercise: 3 stars, advanced (bag_proofs)

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

Theorem count_member_nonzero : (s : bag),
  ble_nat 1 (count 1 (1 :: s)) = true.
Proof.
  (* FILL IN HERE *) Admitted.

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

Theorem ble_n_Sn : n,
  ble_nat n (S n) = true.
Proof.
  intros n. induction n as [| n'].
  Case "0".
    simpl. reflexivity.
  Case "S n'".
    simpl. rewrite IHn'. reflexivity. Qed.

Theorem remove_decreases_count: (s : bag),
  ble_nat (count 0 (remove_one 0 s)) (count 0 s) = true.
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 3 stars, optional (bag_count_sum)

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

(* FILL IN HERE *)

Exercise: 4 stars, advanced (rev_injective)

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

(* FILL IN HERE *)

Options

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

Inductive natoption : Type :=
  | Some : nat natoption
  | None : natoption.

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!

Fixpoint index_bad (n:nat) (l:natlist) : nat :=
  match l with
  | nil ⇒ 42 (* arbitraire! *)
  | a :: l'match beq_nat n O with
               | truea
               | falseindex_bad (pred n) l'
               end
  end.

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.

Fixpoint index (n:nat) (l:natlist) : natoption :=
  match l with
  | nilNone
  | a :: l'match beq_nat n O with
               | trueSome a
               | falseindex (pred n) l'
               end
  end.

Example test_index1 : index 0 [4,5,6,7] = Some 4.
Proof. reflexivity. Qed.
Example test_index2 : index 3 [4,5,6,7] = Some 7.
Proof. reflexivity. Qed.
Example test_index3 : index 10 [4,5,6,7] = None.
Proof. reflexivity. Qed.

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

Fixpoint index' (n:nat) (l:natlist) : natoption :=
  match l with
  | nilNone
  | a :: l'if beq_nat n O then Some a else index' (pred n) l'
  end.

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.

Definition option_elim (d : nat) (o : natoption) : nat :=
  match o with
  | Some n'n'
  | Noned
  end.

Exercise: 2 stars (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.

Definition hd_opt (l : natlist) : natoption :=
  (* FILL IN HERE *) admit.

Example test_hd_opt1 : hd_opt [] = None.
 (* FILL IN HERE *) Admitted.

Example test_hd_opt2 : hd_opt [1] = Some 1.
 (* FILL IN HERE *) Admitted.

Example test_hd_opt3 : hd_opt [5,6] = Some 5.
 (* FILL IN HERE *) Admitted.

Exercise: 1 star, optional (option_elim_hd)

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

Theorem option_elim_hd : (l:natlist) (default:nat),
  hd default l = option_elim default (hd_opt l).
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 2 stars (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.

Fixpoint beq_natlist (l1 l2 : natlist) : bool :=
  (* FILL IN HERE *) admit.

Example test_beq_natlist1 : (beq_natlist nil nil = true).
 (* FILL IN HERE *) Admitted.
Example test_beq_natlist2 : beq_natlist [1,2,3] [1,2,3] = true.
 (* FILL IN HERE *) Admitted.
Example test_beq_natlist3 : beq_natlist [1,2,3] [1,2,4] = false.
 (* FILL IN HERE *) Admitted.

Theorem beq_natlist_refl : l:natlist,
  true = beq_natlist l l.
Proof.
  (* FILL IN HERE *) Admitted.

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

Module Dictionary.

Inductive dictionary : Type :=
  | empty : dictionary
  | record : nat nat dictionary dictionary.

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

Definition insert (key value : nat) (d : dictionary) : dictionary :=
  (record key value d).

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.

Fixpoint find (key : nat) (d : dictionary) : natoption :=
  match d with
  | emptyNone
  | record k v d'if (beq_nat key k)
                       then (Some v)
                       else (find key d')
  end.

Exercise: 1 star (dictionary_invariant1)

Compléter la démonstration suivante.

Theorem dictionary_invariant1' : (d : dictionary) (k v: nat),
  (find k (insert k v d)) = Some v.
Proof.
 (* FILL IN HERE *) Admitted.

Exercise: 1 star (dictionary_invariant2)

Compléter la démonstration suivante.

Theorem dictionary_invariant2' : (d : dictionary) (m n o: nat),
  (beq_nat m n) = false (find m d) = (find m (insert n o d)).
Proof.
 (* FILL IN HERE *) Admitted.

End Dictionary.

End NatList.

(* $Date: 2013-03-09 03:28:08 +0100 (Sat, 09 Mar 2013) $ *)