578 lines
14 KiB
Coq
578 lines
14 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. *)
|
||
|
||
Lemma compare_lists_cons_nil : forall (a: nat) (l: list nat), compare_lists (a::l) [] = false.
|
||
intros.
|
||
simpl.
|
||
reflexivity.
|
||
Qed.
|
||
|
||
Lemma compare_lists_cons_nil_r : forall (a: nat) (l: list nat), compare_lists [] (a::l) = false.
|
||
intros.
|
||
simpl.
|
||
reflexivity.
|
||
Qed.
|
||
|
||
|
||
Lemma compare_lists_nil : forall (l: list nat), compare_lists l [] = true -> l=[].
|
||
induction l.
|
||
simpl.
|
||
trivial.
|
||
intro HH.
|
||
rewrite (compare_lists_cons_nil a l) in HH.
|
||
inversion HH.
|
||
Qed.
|
||
|
||
Lemma compare_lists_nil_r : forall (l: list nat), compare_lists [] l = true -> l=[].
|
||
induction l.
|
||
simpl.
|
||
trivial.
|
||
intro HH.
|
||
rewrite (compare_lists_cons_nil_r a l) in HH.
|
||
inversion HH.
|
||
Qed.
|
||
|
||
Check IF_then_else.
|
||
Check (Nat.eq_dec 0 1).
|
||
Check sumbool.
|
||
|
||
Lemma compare_lists_ind : forall l l' a b,
|
||
(compare_lists (a::l) (b::l')) = true -> ((a=b) /\ (compare_lists l l')=true).
|
||
intros.
|
||
unfold compare_lists in H; fold compare_lists in H.
|
||
destruct (Nat.eq_dec a b).
|
||
split.
|
||
assumption.
|
||
assumption.
|
||
inversion H.
|
||
Qed.
|
||
|
||
Lemma compare_lists_tt : forall l' l l'',
|
||
compare_lists l l' = true -> compare_lists l' l'' = true ->
|
||
compare_lists l l'' = true.
|
||
induction l' as [ | b lb ].
|
||
intros.
|
||
apply (compare_lists_nil l) in H.
|
||
apply (compare_lists_nil_r l'') in H0.
|
||
rewrite H.
|
||
rewrite H0.
|
||
simpl.
|
||
reflexivity.
|
||
intro.
|
||
|
||
case l as [ | a la].
|
||
intros.
|
||
rewrite compare_lists_cons_nil_r in H.
|
||
inversion H.
|
||
|
||
case l'' as [ | c lc ].
|
||
intros.
|
||
inversion H0.
|
||
|
||
intros H1 H2.
|
||
|
||
apply compare_lists_ind in H1.
|
||
apply compare_lists_ind in H2.
|
||
destruct H1.
|
||
destruct H2.
|
||
subst a c.
|
||
|
||
simpl.
|
||
|
||
destruct (Nat.eq_dec b b).
|
||
apply IHlb.
|
||
assumption.
|
||
assumption.
|
||
destruct n.
|
||
reflexivity.
|
||
Qed.
|
||
|
||
Lemma compare_lists_t : forall l1 l2 l3,
|
||
compare_lists l1 l2 = true -> compare_lists l2 l3 = true ->
|
||
compare_lists l1 l3 = true.
|
||
intros.
|
||
apply (compare_lists_tt l2 l1 l3).
|
||
assumption.
|
||
assumption.
|
||
Qed.
|
||
|
||
|
||
|
||
(* symétrie *)
|
||
Lemma compare_lists_s : forall l1 l2,
|
||
compare_lists l1 l2 = true -> compare_lists l2 l1 = true.
|
||
induction l1.
|
||
intros.
|
||
apply compare_lists_nil_r in H.
|
||
rewrite H.
|
||
simpl.
|
||
reflexivity.
|
||
|
||
induction l2.
|
||
intro HH.
|
||
rewrite compare_lists_cons_nil in HH.
|
||
inversion HH.
|
||
|
||
intro H.
|
||
apply compare_lists_ind in H.
|
||
destruct H.
|
||
subst a0.
|
||
|
||
destruct (Nat.eq_dec a a).
|
||
simpl.
|
||
destruct (Nat.eq_dec a a).
|
||
apply IHl1.
|
||
assumption.
|
||
apply n in e.
|
||
inversion e.
|
||
|
||
contradiction.
|
||
Qed.
|
||
|
||
(* reflexivité *)
|
||
Lemma compare_lists_r : forall l, compare_lists l l = true.
|
||
induction l.
|
||
simpl. reflexivity.
|
||
simpl. destruct (Nat.eq_dec a a).
|
||
assumption.
|
||
contradiction.
|
||
Qed.
|
||
|
||
|
||
|
||
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.
|
||
induction l1.
|
||
intro l2.
|
||
case l2.
|
||
simpl. reflexivity.
|
||
intros.
|
||
rewrite compare_lists_cons_nil_r in H.
|
||
inversion H.
|
||
|
||
induction l2.
|
||
intro HH.
|
||
rewrite compare_lists_cons_nil in HH.
|
||
inversion HH.
|
||
|
||
intro H.
|
||
apply compare_lists_ind in H.
|
||
destruct H.
|
||
subst a0.
|
||
apply IHl1 in H0.
|
||
subst l2.
|
||
reflexivity.
|
||
Qed.
|
||
|
||
|
||
Lemma compare_Prop_bool : forall l1 l2, l1=l2 -> compare_lists l1 l2 = true.
|
||
induction l1.
|
||
intros.
|
||
subst l2.
|
||
simpl. reflexivity.
|
||
|
||
induction l2.
|
||
intro H. inversion H.
|
||
|
||
intros.
|
||
inversion H.
|
||
apply IHl1 in H2.
|
||
subst a0.
|
||
simpl.
|
||
|
||
destruct (Nat.eq_dec a a).
|
||
apply compare_lists_r.
|
||
contradiction.
|
||
Qed.
|
||
|
||
|
||
(* Définissez une fonction qui calcule le retournement d'une liste. *)
|
||
Definition rev2 : dl -> dl := fun dd => match dd with
|
||
| (lg, ld) => (ld,lg)
|
||
end.
|
||
|
||
Lemma petit_cons : forall (a:nat) (l:list nat), (a::l) = ([a] ++ l).
|
||
intros.
|
||
simpl.
|
||
reflexivity.
|
||
Qed.
|
||
|
||
Lemma dl_def : forall lg ld, (t2o lg ld) = (List.rev lg ++ ld).
|
||
induction lg.
|
||
simpl. reflexivity.
|
||
simpl. intro ld.
|
||
rewrite IHlg.
|
||
rewrite app_ass.
|
||
rewrite petit_cons.
|
||
reflexivity.
|
||
Qed.
|
||
|
||
Lemma rev2_two2one_ll : forall lg ld,
|
||
compare_lists (List.rev (t2o lg ld)) (two2one (rev2 ((lg,ld))))=true.
|
||
simpl.
|
||
induction lg.
|
||
simpl.
|
||
induction ld.
|
||
simpl. reflexivity.
|
||
simpl. rewrite dl_def. apply compare_lists_r.
|
||
|
||
induction ld.
|
||
simpl.
|
||
rewrite dl_def.
|
||
apply (compare_Prop_bool (rev (rev lg ++ [a])) (a::lg)).
|
||
cut ([a] = rev [a]).
|
||
intro H.
|
||
rewrite H.
|
||
rewrite distr_rev.
|
||
rewrite rev_involutive.
|
||
rewrite rev_involutive.
|
||
simpl. reflexivity.
|
||
simpl. reflexivity.
|
||
|
||
apply compare_Prop_bool.
|
||
apply compare_bool_Prop in IHld.
|
||
|
||
rewrite dl_def.
|
||
rewrite dl_def.
|
||
rewrite dl_def in IHld.
|
||
rewrite dl_def in IHld.
|
||
|
||
rewrite <- (rev_involutive (a0::ld)).
|
||
rewrite distr_rev.
|
||
rewrite rev_involutive.
|
||
rewrite rev_involutive.
|
||
|
||
rewrite <- (rev_involutive ld) in IHld.
|
||
rewrite <- (distr_rev (rev ld) (a::lg)) in IHld.
|
||
rewrite rev_involutive in IHld.
|
||
rewrite rev_involutive in IHld.
|
||
reflexivity.
|
||
Qed.
|
||
|
||
|
||
(* 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.
|
||
|
||
induction d as [ lg ld ].
|
||
apply rev2_two2one_ll.
|
||
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.
|
||
*)
|
||
Fixpoint ridelle l n := match l with
|
||
| nil => (nil, false)
|
||
| e::s => if Nat.eq_dec n e then (s, true) else
|
||
match (ridelle s n) with
|
||
| (ss, b) => (e::ss, b)
|
||
end
|
||
end.
|
||
|
||
Definition rid ll n := match ll with
|
||
| (lg, ld) => match (ridelle lg n) with
|
||
| (sg, b) => if Bool.bool_dec b true then (sg,ld) else
|
||
match (ridelle ld n) with
|
||
| (sd, bb) => (sg,sd)
|
||
end
|
||
end
|
||
end.
|
||
|
||
Definition fst (ll: list nat * bool) := match ll with
|
||
| (lg, ld) => lg
|
||
end.
|
||
|
||
|
||
(*
|
||
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.*)
|
||
|
||
Definition rid_sorted ll n := match ll with
|
||
| (lg, ld) => match lg with
|
||
| nil => (nil, fst (ridelle ld n))
|
||
| e::s => if Bool.bool_dec (e<?n) true then (lg, fst (ridelle ld n)) else (fst (ridelle lg n), ld)
|
||
end
|
||
end.
|
||
|
||
|
||
|
||
|
||
(* 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 :=
|
||
| same_nil : forall l, same ([],l) ([],l)
|
||
| same_decale : forall lg ld a dd, same (lg,a::ld) dd -> same (a::lg, ld) dd
|
||
| same_s : forall ld lg lg', ld<>[] -> same (ld, lg) ([], lg') -> same ([], lg') (ld, lg).
|
||
|
||
Lemma cons_toi_meme : forall (l:list nat) (a:nat), l=(a::l) -> False.
|
||
intros.
|
||
induction l.
|
||
inversion H.
|
||
inversion H.
|
||
subst.
|
||
apply IHl in H2.
|
||
apply H2.
|
||
Qed.
|
||
|
||
Lemma same_decale_r : forall lg ld a dd, same (a::lg, ld) dd -> same (lg, a::ld) dd.
|
||
Proof.
|
||
intros.
|
||
inversion H. (* On fait les trois cas de same *)
|
||
subst. assumption.
|
||
Qed.
|
||
|
||
Lemma same_right_shift : forall lg ld dd, same (lg,ld) dd <-> same ([], t2o lg ld) dd.
|
||
Proof.
|
||
induction lg.
|
||
|
||
(* Initialisation *)
|
||
simpl.
|
||
reflexivity.
|
||
|
||
(* Héredité *)
|
||
intros ld dd.
|
||
simpl t2o.
|
||
split.
|
||
(* Une induction *)
|
||
intro H.
|
||
apply IHlg.
|
||
apply same_decale_r in H.
|
||
assumption.
|
||
intro H.
|
||
apply IHlg in H.
|
||
apply same_decale.
|
||
assumption.
|
||
Qed.
|
||
|
||
Lemma same_s_r : forall dd lg', same ([], lg') dd -> same dd ([], lg').
|
||
induction dd as [lg ld].
|
||
intro lg'.
|
||
intro H.
|
||
inversion H.
|
||
subst. assumption.
|
||
subst. assumption.
|
||
Qed.
|
||
|
||
Lemma same_nil_first : forall ld ld', same ([], ld) ([], ld') -> ld=ld'.
|
||
intros.
|
||
inversion H.
|
||
reflexivity.
|
||
subst.
|
||
exfalso.
|
||
apply H3.
|
||
reflexivity.
|
||
Qed.
|
||
|
||
Theorem same_compare :
|
||
forall d1 d2, same d1 d2 -> compare_dl d1 d2 = true.
|
||
|
||
intros.
|
||
induction d1 as [lg ld].
|
||
induction d2 as [lg' ld'].
|
||
|
||
cut (t2o lg ld=t2o lg' ld').
|
||
intro.
|
||
unfold compare_dl.
|
||
simpl.
|
||
rewrite <-H0.
|
||
apply compare_lists_r.
|
||
|
||
apply same_right_shift in H.
|
||
apply same_s_r in H.
|
||
apply same_right_shift in H.
|
||
inversion H.
|
||
reflexivity.
|
||
subst.
|
||
apply same_nil_first in H4.
|
||
assumption.
|
||
Qed.
|
||
|
||
Lemma list_empty_dec :
|
||
forall (l: list nat), (l = nil) \/ (exists a s, l = a::s).
|
||
intro l.
|
||
case l.
|
||
left. reflexivity.
|
||
right. exists n. exists l0. reflexivity.
|
||
Qed.
|
||
|
||
Lemma two2one_decale :
|
||
forall a lg ld, two2one (a :: lg, ld) = two2one (lg, a::ld).
|
||
intros.
|
||
simpl.
|
||
reflexivity.
|
||
Qed.
|
||
|
||
Lemma compare_same_deca1 :
|
||
forall lg ld ld',
|
||
two2one (lg, ld) = two2one ([], ld') -> same (lg, ld) ([], ld').
|
||
|
||
induction lg.
|
||
|
||
intros.
|
||
simpl in H. subst. apply same_nil.
|
||
|
||
intros.
|
||
apply same_decale.
|
||
rewrite two2one_decale in H.
|
||
apply IHlg in H.
|
||
assumption.
|
||
Qed.
|
||
|
||
Lemma compare_same_deca2 :
|
||
forall lg ld lg' ld',
|
||
two2one (lg, ld) = two2one (lg', ld') -> same (lg, ld) (lg', ld').
|
||
induction lg.
|
||
|
||
intros.
|
||
simpl in H. subst.
|
||
case lg'.
|
||
simpl. apply same_nil.
|
||
intros.
|
||
apply same_s.
|
||
intro H. inversion H.
|
||
apply compare_same_deca1.
|
||
simpl. reflexivity.
|
||
|
||
intros.
|
||
apply same_decale.
|
||
apply IHlg.
|
||
rewrite <- two2one_decale. assumption.
|
||
Qed.
|
||
|
||
Theorem compare_same :
|
||
forall d1 d2, compare_dl d1 d2 = true -> same d1 d2.
|
||
Proof.
|
||
intros.
|
||
induction d1 as [lg ld].
|
||
induction d2 as [lg' ld'].
|
||
unfold compare_dl in H.
|
||
apply compare_bool_Prop in H.
|
||
|
||
apply compare_same_deca2.
|
||
assumption.
|
||
Qed.
|
||
|
||
|
||
(* fin du DM ***************************************************************)
|