Lists
Require Export Induction.
Module NatList.
Paires d'entiers
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 y ⇒ x
end.
Definition snd (p : natprod) : nat :=
match p with
| pair x y ⇒ y
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.
(snd p, fst p) = swap_pair p.
Proof.
(* FILL IN HERE *) Admitted.
Theorem fst_swap_is_snd : ∀(p : natprod),
fst (swap_pair p) = snd p.
Proof.
(* FILL IN HERE *) Admitted.
fst (swap_pair p) = snd p.
Proof.
(* FILL IN HERE *) Admitted.
☐
Listes de nombres
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,
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.
Notation "x + y" := (plus x y)
(at level 50, left associativity).
(at level 50, left associativity).
Fixpoint repeat (n count : nat) : natlist :=
match count with
| O ⇒ nil
| S count' ⇒ n :: (repeat n count')
end.
La fonction length calcule la longueur d'une liste.
Fixpoint length (l:natlist) : nat :=
match l with
| nil ⇒ O
| h :: t ⇒ S (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
| nil ⇒ l2
| h :: t ⇒ h :: (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
| nil ⇒ default
| h :: t ⇒ h
end.
Definition tail (l:natlist) : natlist :=
match l with
| nil ⇒ nil
| h :: t ⇒ t
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)
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.
☐
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.)
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.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
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
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
Induction sur les listes
- 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.
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.
Voici un exemple similaire à faire ensemble en classe:
- 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 den :: ((l1' ++ l2) ++ l3) = n :: (l1' ++ (l2 ++ l3)),qui est immédiat par hypothèse d'induction. ☐
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 :: t ⇒ h :: (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
| nil ⇒ nil
| h :: t ⇒ snoc (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.
Théorème: Pour toute liste l, length (rev l) = length l.
Démonstration: Par induction sur l.
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
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.
- 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 montrerlength (snoc (n' :: l') n) = S (length (n' :: l')).Par définition de length et snoc, ceci est une conséquence deS (length (snoc l' n)) = S (S (length l')),qui est immédiat par hypothèse d'induction. ☐
- 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 montrerlength (rev (n :: l')) = length (n :: l').Par définition de rev, ceci est une conséquence delength (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. ☐
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. ☐
SearchAbout
(* 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 *)
☐
Cet exercice admet une solution simple et une plus dure.
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.
(* FILL IN HERE *)
☐
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
| true ⇒ a
| false ⇒ index_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
| nil ⇒ None
| a :: l' ⇒ match beq_nat n O with
| true ⇒ Some a
| false ⇒ index (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
| nil ⇒ None
| 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'
| None ⇒ d
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
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
| empty ⇒ None
| record k v d' ⇒ if (beq_nat key k)
then (Some v)
else (find key d')
end.
Theorem dictionary_invariant1' : ∀(d : dictionary) (k v: nat),
(find k (insert k v d)) = Some v.
Proof.
(* FILL IN HERE *) Admitted.
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) $ *)