From 6424326014a5bf08290c7661e7212cd924e03371 Mon Sep 17 00:00:00 2001 From: Mysaa Date: Thu, 23 Sep 2021 10:04:09 +0200 Subject: [PATCH] =?UTF-8?q?Ajout=20du=20d=C3=A9but=20du=20DM?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- dm1-AVRILLON.v | 214 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 214 insertions(+) create mode 100644 dm1-AVRILLON.v diff --git a/dm1-AVRILLON.v b/dm1-AVRILLON.v new file mode 100644 index 0000000..617fd97 --- /dev/null +++ b/dm1-AVRILLON.v @@ -0,0 +1,214 @@ + +(* L3 IF, 2021-2022, cours Théorie de la Programmation, DM 1. + À rendre en déposant le fichier nommé DM1-nomdefamille.v sur le portail des études + pour le 7 octobre à 23h59 au plus tard. + + À faire seul(e). Vous pouvez solliciter les chargés de TP, H. Déprés et E. Hazard, + ou D. Hirschkoff sur discord (ou par mail) si vous avez des questions. + + +On s’intéresse ici à une représentation d’une liste à l’aide de deux listes. +Pour simplifier, on ne considérera que des listes d’entiers naturels (list nat) en Coq. + + +L’intuition est que l’on “pointe” un endroit dans la liste (entre deux entiers), +avec d’un côté ce qui est avant, et de l’autre ce qui est après. +On convient que le couple (l1,l2) représente la liste commençant par la liste l1 +à l’envers, suivie de la liste l2. Par exemple, le couple ([2;4], [5]) représente +la liste [4;2;5], le pointeur étant entre le 2 et le 5. +Les couples ([2], [4;5]), ([], [2;4;5]) et ([5;4;2],[]) représentent également la même liste. +Ce fichier sert de trame à votre devoir : il s’agit de le renvoyer rempli. + +Dans les solutions que vous proposez, il faut s’astreindre à ne pas parcourir inutilement +les listes, avec l’idée qu’ajouter un élément à une liste (opérateur ::) a un coût, +et déconstruire une liste (récupérer la tête et la queue de la liste, si celle-ci n’est pas +vide) a également un coût. +Comme évoqué ci-dessus, une liste d’entiers peut avoir plusieurs représentations équivalentes. +Lorsqu’on a le choix, on privilégiera la représentation avec “un maximum d’éléments +à droite” (intuitivement parce que la liste de droite est celle qui est à l’endroit), +mais on ne va pas s’amuser à parcourir des bouts de liste uniquement pour en faire +basculer certains à droite. +*) + +(************************************************************************************) + +(* Nous faisons appel à la librairie sur les listes. + Commencez par lire la documentation sur cette librairie, certains des + résultats qui y sont prouvés pourront vous être utiles : + https://coq.inria.fr/library/Coq.Lists.List.html +*) +Require Export List. + + +(* On introduit des incantations récupérées du livre "Software Foundations", + de B. Pierce et al., pour utiliser les notations habituelles avec les crochets *) +Notation "x :: l" := (cons x l) + (at level 60, right associativity). +Notation "[ ]" := nil. +Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..). + + +(* La représentation des listes sur laquelle on travaille pour ce DM : *) +Definition dl : Set := (list nat)*(list nat). + +Definition sizetwo := fun d : dl => length (fst d) + length (snd d). + + +(* Des listes de nat aux dl *) +Definition init : (list nat)-> dl := fun l => ([],l). + + +(* Des dl aux listes de nat. + Définissez t2o "directement", sans faire appel à + des fonctions définies dans la librairie List. *) +Fixpoint t2o (l1 l2: list nat) := match l1 with + | [] => l2 + | e::s => t2o s (e::l2) +end. + + +(* Utilisez t2o pour définir la fonction suivante, qui est l'"inverse" + de init. *) +Definition two2one : dl -> list nat := fun ll => + match ll with + | (l1,l2) => t2o l1 l2 + end. + + + + +(*******************************************************************************) + +Require Export Arith. (* pour connaître des lemmes ci-dessous *) + +(* On introduit la fonction suivante *) +Fixpoint compare_lists l1 l2 := + match l1,l2 with +| nil,nil => true +| x::xs, y::ys => if Nat.eq_dec x y then compare_lists xs ys else false +| _,_ => false end. + +(* La fonction compare_lists fait un if-then-else, en se servant de Nat.eq_dec : *) +Check Nat.eq_dec. +(* Nat.eq_dec + : forall n m : nat, {n = m} + {n <> m} *) +(* La notation { .. } + { .. } correspond à une "disjonction dans Set", sur + laquelle on peut faire un if-then-else. Cette notation s'appuie sur le type + sumbool de Coq. + Vous pouvez par exemple utiliser la commande *) +Search sumbool lt. +(* pour voir l'ensemble des lemmes que connaît Coq faisant intervenir lt et sumbool. *) + + + + + +(* transitivité *) +(* Pour prouver ce lemme, vous pouvez utiliser une seule induction, et pas mal + de "destruct". À noter que destruct peut être utilisé sur une liste, mais on + peut aussi faire destruct (Nat.eq_dec k k'), où k et k' sont des nat. *) +Lemma compare_lists_t : forall l1 l2 l3, + compare_lists l1 l2 = true -> compare_lists l2 l3 = true -> + compare_lists l1 l3 = true. +[...] +Qed. + + +(* symétrie *) +Lemma compare_lists_s : forall l1 l2, + compare_lists l1 l2 = true -> compare_lists l2 l1 = true. +[...] +Qed. + +(* reflexivité *) +Lemma compare_lists_r : forall l, compare_lists l l = true. +[...] + + + +Definition compare_dl : dl -> dl -> bool := + fun d1 d2 => compare_lists (two2one d1) (two2one d2). + + +(* Sans surprise, le calcul qui est effectué par compare_lists en renvoyant + un bool correspond à l'égalité sur les list nat : c'est prouvé par les deux + lemmes suivants. *) +Lemma compare_bool_Prop : forall l1 l2, compare_lists l1 l2 = true -> l1=l2. +[...] +Qed. + + +Lemma compare_Prop_bool : forall l1 l2, l1=l2 -> compare_lists l1 l2 = true. +[...] +Qed. + + +(* Définissez une fonction qui calcule le retournement d'une liste. *) +Definition rev2 : dl -> dl := [...]. + +[...] + +(* Pour prouver le lemme suivant, vous pouvez introduire des lemmes + intermédiaires, et aussi vous appuyer sur la librairie List de Coq + (n'oubliez pas que ++ est une notation pour la fonction app). *) +Lemma rev2_two2one : forall d, + compare_lists (List.rev (two2one d)) (two2one (rev2 d))=true. +[...] +Qed. + + + +(* Retirer un élément d'une liste *) + +(* +Définir une fonction rid : dl -> nat -> dl, qui retire un élément d'une liste +s'il le trouve, et renvoie la liste inchangée sinon. +Si l'élément apparaît plusieurs fois dans la liste, on n'en retire qu'une seule copie. + +Veillez à prendre en compte les recommandations ci-dessus à propos du fait que l'on +évite de parcourir inutilement des bouts de liste, et que l'on préfère que +"ça penche à droite" plutôt qu'à gauche. +*) + +[...] + + +(* +Définir une fonction rid_sorted : dl -> nat -> dl, qui fait comme rid2, à ceci près +que l'on suppose que la liste passée en argument (et représentée avec un dl) est triée.*) + +[...] + + + +(* Relation inductive entre listes. *) + +(* Définir une relation inductive dont l'intention est qu'elle coïncide avec compare_dl. + Il n'est pas autorisé de faire appel à des fonctions définies ci-dessus dans la + définition de same. *) +Inductive same : dl -> dl -> Prop := [...]. +[...] + + + +(* On prouve ensuite que compare_dl et same coïncident. *) + + +Theorem same_compare : + forall d1 d2, same d1 d2 -> compare_dl d1 d2 = true. +[...] +Qed. + + + +[...] + + + +Theorem compare_same : + forall d1 d2, compare_dl d1 d2 = true -> same d1 d2. +[...] +Qed. + + +(* fin du DM ***************************************************************)