diff --git a/dm1-AVRILLON.v b/dm1-AVRILLON.v index 8a9e49f..aabcee3 100644 --- a/dm1-AVRILLON.v +++ b/dm1-AVRILLON.v @@ -414,16 +414,16 @@ 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 : same ([],[]) ([],[]) - | same_decale : forall lg ld a dd, same (a::lg,ld) dd -> same (lg, a::ld) dd - | same_cons : forall lg ld lg' ld' a, same (lg, ld) (lg',ld') -> same (lg, a::ld) (lg', a::lg) - | same_s : forall dd dd', same dd dd' -> same dd' dd. + | 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. @@ -435,115 +435,142 @@ apply IHl in H2. apply H2. Qed. -Lemma same_nil_plus : forall ld ld', same ([], ld) ([], ld') -> ld=ld'. -Abort. -(* -induction ld. -intro ld'. -induction ld'. -reflexivity. -intro H. -inversion H. -subst. -reflexivity. -subst. -case ld'. -reflexivity. +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. -inversion H. -intros. -inversion H. -subst. reflexivity. -subst. apply IHld in H1. subst. reflexivity. -Qed.*) +apply IHlg. +apply same_decale_r in H. +assumption. +intro H. +apply IHlg in H. +apply same_decale. +assumption. +Qed. -Lemma same_left : forall l l', same ([],l) ([],l') -> l=l'. -Abort. - -(* On prouve ensuite que compare_dl et same coïncident. *) -Lemma same_first_equal : forall lg ld lg' ld', same (lg,ld) (lg',ld') -> lg=lg' -> ld=ld'. -intros lg. -induction ld. +Lemma same_s_r : forall dd lg', same ([], lg') dd -> same dd ([], lg'). +induction dd as [lg ld]. intro lg'. -induction ld'. -reflexivity. -intros. subst. -induction lg'. -induction ld'. -exfalso. inversion H. subst. +intro H. inversion H. -subst. reflexivity. -subst. +subst. assumption. +subst. assumption. +Qed. - - -apply cons_toi_meme in H4. exfalso. apply H4. -subst. induction lg'. -inversion H2. -subst. reflexivity. -subst. apply same_nil in H1. -subst. reflexivity. -inversion H +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. -induction d1 as [lg ld]. -induction lg. -intros. -unfold compare_dl. -simpl. -induction d2 as [lg' ld']. -simpl. -induction lg'. -simpl. -apply same_first_equal in H. -apply compare_Prop_bool. -assumption. -reflexivity. -simpl. -inversion H. -intro d2. -induction d2 as [ lg' ld' ]. -induction lg'. -intro H. -inversion H. subst. -unfold compare_dl. -simpl. -destruct (Nat.eq_dec a a). -apply compare_lists_r. -contradiction. -intro H. -inversion H. subst lg' ld' a0 ld0 lg0. -unfold compare_dl. -apply compare_lists_r. -subst ld' lg lg0 ld0 a1. -rename a0 into b; rename lg' into lg. -unfold compare_dl. -unfold two2one. -simpl. -apply compare_lists_r. + + 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 lg. induction d2 as [lg' ld']. - intro H. unfold compare_dl in H. - unfold two2one in H. - simpl in H. apply compare_bool_Prop in H. - induction lg'. - simpl in H. subst. apply same_idem. - simpl in H. subst. - unfold t2o in H. + apply compare_same_deca2. + assumption. Qed. diff --git a/tp3.v b/tp3.v new file mode 100644 index 0000000..85fd875 --- /dev/null +++ b/tp3.v @@ -0,0 +1,501 @@ + +(*** TP3 : Prédicats Inductifs et Relations ***) + +Require Import Lia. + +(** * Petit Rappel de Certaines Tactiques Coq **) + +(* On rappelle ici quelques tactiques de Coq qui vous serviront pour ce TP. Si vous savez ce qu'elle font, +passez à la suite *) + +(* + [induction x],[induction H] + Quand cette tactique est utilisé sur un objet "x" avec un type inductif (comme les listes), cela permet de + faire une preuve par induction sur ce type. De la même façon, si "H" est une hypothèse sur une relation + inductive, cette tactique permet de faire une preuve par induction sur cette relation. + + [inversion H] + Demande à Coq de trouver les conditions nécessaires pour que H soit vrai, permet intuitivement de faire du cas par cas + + [constructor] + Coq essaye les différentes règles d'une définition inductive, et s'il en trouve une qui correspond, il l'applique + + [assumption] + Si vous avez "H" en hypothèse, et que vous devez prouver "H", cette tactique termine immédiatement la preuve. + + [apply H with x1 x2] + Cette tactique permet de résoudre l'erreur Coq "unable to find an instance for the variable..." lors +d'un [apply], en lui donnant explicitement ce qu'il doit prendre comme instantiation (ici, x1 x2) + + [unfold f] + Permet de remplacer "f" par sa définition dans le but. SI vous voulez remplacer "f" dans une hypothèse "H", vous +pouvez utiliser [unfold f in H] + + [rewrite H] + Si "H" est de la forme "a=b", cette tactique remplace toutes les occurences de "a" dans le but par "b". Symétriquement, +[rewrite <- H] remplacera toutes les occurences de "b" dans le but par "a". Enfin, comme pour unfold, +[rewrite H in H'] permet de remplacer les occurences de "a" dans l'hypothèse "H'" par "b". +*) + + + + + + +(*** Prédicats Inductifs ***) + + + +(* Comme au TP précédent, on va considérer des listes et définir une relation + binaire inductive sur les listes, que l'on notera "perm l1 l2", exprimant + le fait que l2 est une permutation de l1. + + Cette définition inductive est donnée par les quatres règles d'inférence suivantes : + + perm l₁ l₂ perm l₂ l₃ + ───────────── (refl) ──────────────────────────── (trans) + perm l l perm l₁ l₃ + + + perm l₁ l₂ + ────────────────────── (tail) ────────────────────────── (head) + perm (x::l₁) (x::l₂) perm (x::y::l) (y::x::l) + +*) + +(* Donnez une réprésentation en Coq de cette définition (on travaillera avec des liste d'entiers pour simplifier) *) + +Require Import List. + +Inductive perm : list nat -> list nat -> Prop := + | perm_r : forall l, perm l l + | perm_t : forall l l' l'', perm l l' -> perm l' l'' -> perm l l'' + | perm_tl : forall l l' x, perm l l' -> perm (x::l) (x::l') + | perm_hd : forall x y l, perm (x::y::l) (y::x::l). + + +(* On se donne le prédicat "mem" défini par : *) + +Inductive mem : nat -> list nat -> Prop := +|mem_head : forall x l, mem x (x::l) +|mem_tail : forall x y l, mem x l -> mem x (y::l). + +(* Pour s'échauffer, montrez que mem et perm donnent bien + ce que l'on attend sur des exemples simples. *) + +Lemma perm_example : perm (1::2::4::5::3::nil) (2::1::4::3::5::nil). + cut (perm (5::3::nil) (3::5::nil)). + intro H. + apply perm_tl with (x := 4) in H. + apply perm_tl with (x := 2) in H. + apply perm_tl with (x := 1) in H. + + cut (perm (1 :: 2 :: 4 :: 3 :: 5 :: nil) (2 :: 1 :: 4 :: 3 :: 5 :: nil)). + intro HH. + apply (perm_t (1 :: 2 :: 4 :: 5 :: 3 :: nil) (1 :: 2 :: 4 :: 3 :: 5 :: nil) (2 :: 1 :: 4 :: 3 :: 5 :: nil)). + assumption. + assumption. + + apply perm_hd. + apply perm_hd. + +Qed. + + +Lemma mem_example : mem 5 (1::2::4::5::3::nil). + repeat constructor. +Qed. + + +(* Définir maintenant un prédicat mem1, tel que mem1 x l exprimera + le fait que la liste l contient exactement une occurrence de l. + + On rappelle que même si vous pourriez en avoir très envie, il n'est + pas possible¹ (pour des raisons de bonnes fondaisons, a.k.a. pour + éviter les serpents qui se mordent la queue) d'utiliser la négation + d'un prédicat inductif comme hypothèse d'un des cas le définissant : + + Inductive malfondé : nat -> Prop := + | ok : forall x, bli x -> malfondé x + | pasok : forall x, (not (malfondé x)) -> malfondé (x+1) + . + + ——————————————————— + ¹: Coq vous dira gentiment "Non strictly positive occurence of ..." + +*) + +Inductive mem0 : nat -> list nat -> Prop := + | mem0_nil : forall x, mem0 x nil + | mem0_cons : forall x y l, x<>y -> mem0 x l -> mem0 x (y::l). + +Inductive mem1 : nat -> list nat -> Prop := + | mem1_cons : forall x y l, x<>y -> mem1 x l -> mem1 x (y::l) + | mem1_x : forall x l, mem0 x l -> mem1 x (x::l). + + + +(* Définir aussi un prédicat mem_n tel que "mem_n x l n" + exprime le fait que x apparaît exactement n fois dans l. *) + +Inductive mem_n : nat -> list nat -> nat -> Prop := + | memn_nil : forall x, mem_n x nil 0 + | memn_cons : forall x l k, mem_n x l k -> mem_n x (x::l) (S k) + | memn_fcons : forall x l k y, x<>y -> mem_n x l k -> mem_n x (y::l) k. + + + +(* Montrez là encore que mem1/mem_n fonctionne bien sur des exemples simples. + Vous pourrez utiliser la tactique: + [subst] + qui permet de faire toutes les substitutions possibles pour éliminer + les égalités de la forme x = bla dans le contexte (en remplaçant donc + x par bla partout). *) + +Lemma test_subst : forall A B C D E F : nat, A = B -> B = C -> C = D -> D = E -> E = F -> A = F. +intros. subst. reflexivity. Qed. + +(* + Pour ne pas vous embarasser avec les (in)égalités arithmétiques, vous + avez aussi le droit de "tricher" en utilisant la tactique + [lia] + (que l'on considérera comme une grosse boîte noire à propos de + laquelle on ne donnera pas plus d'explication). + + *) + +Lemma lia_example : 3 <= 5 /\ 1<>0. +split. lia. lia. Qed. + + + +Lemma mem_n_example : mem_n 5 (1::5::4::5::3::nil) 2. + apply memn_fcons. lia. + apply memn_cons. + apply memn_fcons. lia. + apply memn_cons. + apply memn_fcons. lia. + apply memn_nil. + +Qed. + + +Lemma mem1_example : mem1 5 (1::2::4::5::3::nil). + apply mem1_cons. lia. + apply mem1_cons. lia. + apply mem1_cons. lia. + apply mem1_x. + apply mem0_cons. lia. + apply mem0_nil. + +Qed. + +Lemma mem1_example2 : mem1 5 (1::5::4::5::nil) -> False. + intro. + inversion H. subst. + inversion H4. subst. + contradiction. (* 5<>5 *) + subst. + inversion H2. subst. + inversion H7. + contradiction. + +Qed. + + + +(** * Teaser *) + +(* Maintenant que vous êtes échauffé.e.s, vous réveriez sûrement de montrer + des résultats un peu plus sérieux sur perm et mem, par exemple : + +Lemma perm_mem : forall l1 l2, perm l1 l2 -> (forall x, mem x l1 -> mem x l2). + + + Malheureusement, il nous manque pour le moment un outil conceptuel pour + faire cela : l'induction sur la relation / sur les dérivations. + Vous pouvez évidemment essayer, mais vous devriez¹ rencontrer assez rapidement + un problème... + + Promis, vous pourrez bientôt le faire, mais pour cela il vous faudra attendre + le prochaine exercice pour goûter à de telles inductions. + + ———————————————————————– + ¹ Vos chargés de TP, prudents, laissent ouverte la possibilité d'un malentendu, + même s'ils n'y croient guère =) +*) + + + +(*** Arbres & inductions ***) + + + +(* On rappelle qu'un arbre binaire étiqueté est constitué soit par une feuille, +soit par un noeud contenant une étiquette et deux arbres (appelés respectivement +fils droit et gauche. *) + +(* Définir ici les arbres binaires étiquetés par des entiers au moyen d'un type +inductif. *) + +Inductive tree : Set := + L : tree | N : nat -> tree -> tree -> tree. + + +(* Définissez deux fonctions calculant respectivement la taille (nombre de noeuds) et + la profondeur d'un arbre. *) + +Fixpoint size (t:tree) := match t with + | L => 0 + | N n g d => S ((size g) + (size d)) +end. + +Fixpoint depth (t:tree) := match t with + | L => 0 + | N n g d => S (max (depth g) (depth d)) +end. + + + + +(* On dit qu'un arbre est un brin si chaque noeud a au moins un de ses + deux fils qui est une feuille (les feuilles sont des brins). + + Définir le prédicat "brin" au moyen de règles inductives.*) + + + +Inductive brin : tree -> Prop := + | brin_l : brin L + | brin_ng : forall n d, brin d -> brin (N n L d) + | brin_nd : forall n g, brin g -> brin (N n g L). + + +(* On va montrer que pour les brins, les notions de taille et profondeur + coïncident. *) + +Lemma zero_not_max : forall n, max n 0 = n. + induction n. + simpl. reflexivity. + simpl. reflexivity. +Qed. + +Lemma plus_zero : forall n, n + 0 = n. +induction n. +simpl. reflexivity. +simpl. +rewrite IHn. +reflexivity. +Qed. + +Lemma brin_sd : forall t, brin t -> size t = depth t. + induction t. + simpl. reflexivity. + + intro Hb. + inversion Hb. subst. + simpl. + apply IHt2 in H0. + rewrite H0. reflexivity. + + subst. simpl. + apply IHt1 in H0. + rewrite H0. + rewrite zero_not_max. + rewrite plus_zero. + reflexivity. + +Qed. + + +(* On va ici découvrir une nouvelle façon de faire des inductions, + non plus sur les objets (ici les arbres) dont on veut prouver des propriétés, + mais sur les preuves elles-même. + Pour ce faire, on va refaire la preuve précédente en utilisant ce procédé. *) + +Lemma brin_sd_bis : forall t, brin t -> size t = depth t. + intros t H. + (* On va ici raisonner par induction sur la preuve de (brin t). + On obtient naturellement autant de sous-buts que de cas définissant le type + inductif brin. *) + induction H. + simpl. reflexivity. + simpl. rewrite IHbrin. reflexivity. + simpl. rewrite IHbrin. rewrite zero_not_max. rewrite plus_zero. reflexivity. + +Qed. + +(* Maintenant que vous avez réussi, observez bien dans chacun des cas les + hypothèses d'induction, que l'on pourra comparer avec les hypothèses obtenues + dans la preuve précédente après l'induction sur t *et* l'inversion sur H. *) + + +(*** Pair et impair sont sur un bateau ***) + +(* On définit les prédicats suivants qui devraient vous être familiers. *) + + +Inductive even:nat -> Prop := +|even0: even 0 +|evenS: forall n, even n -> even (S(S n)). + +Inductive odd:nat -> Prop := +|odd1: odd 1 +|oddS: forall n, odd n -> odd (S(S n)). + +(* Vous n'êtes pas sans savoir que tout entier est soit pair soit impair. Mais + saurez-vous le démontrer ? *) + + + + +Lemma odd_or_even: forall n, odd n \/ even n. + cut (forall n, (odd n \/ even n) /\ (odd (S n) \/ even (S n))). + intros. apply H. + + induction n. + split. right. apply even0. left. apply odd1. + + split. + destruct IHn. + destruct H0. + left. assumption. + right. assumption. + + destruct IHn. + destruct H. + left. apply oddS. assumption. + right. apply evenS. assumption. +Qed. + + +(** Bonus : **) + +(*** Tri de listes ***) + +(* Dans cette section, on travaille encore une fois sur les listes d'entiers *) + +(* Ecrivez un prédicat inductif "sorted" indiquant si une liste est triée *) + +Inductive sorted : list nat -> Prop := + | sorted_nil : sorted nil + | sorted_sg : forall x, sorted (x::nil) + | sorted_cons : forall a b l, (a <= b) -> sorted (a::l) -> sorted (b::a::l). + +(* Écrivez un programme "insert_sort" pour le tri par insertion *) +(* Vous allez avoir besoin de la fonction suivante :*) +Check Nat.compare. +Print comparison. +Print comparison_ind. + +(* En particulier, cela nous permet d'écrire quelque chose comme + +match (Nat.compare x y) with + | Eq => ... + | Lt => ... + | Gt => ... +end. + +*) + +Fixpoint insert x lt := match lt with + | nil => x::nil + | cons e s => match (Nat.compare x e) with + | Gt | Eq => x::lt + | Lt => e::(insert x s) + end + end. + +Fixpoint insert_sort l := match l with + | nil => nil + | cons x s => insert x (insert_sort s) + end. + +(* Il faut d'abord prouver que la fonction insert_sort ne renvoie pas n'importe quoi, notamment qu'elle renvoie une permutation de la liste de départ. Prouvez ainsi le lemme suivant : *) + +(* Lorsque vous êtes face à un (Nat.compare a b) et que vous voulez traiter les 3 cas, vous pouvez faire [destruct (Nat.compare a b)] pour traiter les trois cas possibles *) + +Lemma perm_lgth : forall l l', perm l l' -> length l = length l'. + intros. + induction H. + reflexivity. + rewrite IHperm1. rewrite IHperm2. reflexivity. + simpl. rewrite IHperm. reflexivity. + simpl. reflexivity. +Qed. + + +Lemma perm_nil : forall l, perm l nil -> l=nil. + intros. + apply perm_lgth in H. + apply length_zero_iff_nil in H. + assumption. +Qed. + +Lemma eq_s (A:Type): forall a b:A, a=b -> b=a. + intros. + rewrite H. + reflexivity. +Qed. + +Lemma insert_sort_perm : forall l, perm l (insert_sort l). + induction l. + simpl. apply perm_r. + induction (insert_sort l). + inversion IHl. + subst. apply perm_r. + subst. apply perm_nil in IHl. subst. apply perm_tl. apply perm_r. + rename a0 into b. + simpl. + remember (PeanoNat.Nat.compare a b) as x. + destruct x. + apply eq_s in Heqx. + apply PeanoNat.Nat.compare_eq_iff in Heqx. subst. + + apply perm_tl. assumption. + +Qed. + +(* Vous avez peut-être remarqué plus haut qu'avec [destruct (Nat.compare a b)], + on fait effectivement les 3 cas mais Coq ne rajoute pas dans quel cas on est + en hypothèse ! Pour la preuve précédente, ce n'est pas important, mais pour + prouver que la liste est triée, il faut savoir dans quel cas on est. + + Et donc, lorsque vous êtes face à une preuve pour laquelle vous voulez + intuitivement faire "Si a=b alors je fais ça, si a