215 lines
6.8 KiB
Coq
215 lines
6.8 KiB
Coq
|
||
(* 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 ***************************************************************)
|