From 3ef408bcacebfede586275e4171b54004ad66e5a Mon Sep 17 00:00:00 2001 From: Mysaa Date: Mon, 27 Sep 2021 00:15:13 +0200 Subject: [PATCH] =?UTF-8?q?Continuation=20du=20DM=20et=20deuxi=C3=A8me=20T?= =?UTF-8?q?P.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- dm1-AVRILLON.v | 378 +++++++++++++++++++++++++++++++-- tp2.v | 561 +++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 918 insertions(+), 21 deletions(-) create mode 100644 tp2.v diff --git a/dm1-AVRILLON.v b/dm1-AVRILLON.v index 617fd97..8a9e49f 100644 --- a/dm1-AVRILLON.v +++ b/dm1-AVRILLON.v @@ -99,30 +99,142 @@ Check Nat.eq_dec. 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. -(* 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. -[...] +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. @@ -130,34 +242,132 @@ 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 := [...]. +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 *) (* @@ -169,15 +379,38 @@ Veillez à prendre en compte les recommandations ci-dessus à propos du fait que é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 dl -> Prop := [...]. -[...] +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. +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_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. +intros. +intro H. +inversion H. +intros. +inversion H. +subst. reflexivity. +subst. apply IHld in H1. subst. reflexivity. +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. +intro lg'. +induction ld'. +reflexivity. +intros. subst. +induction lg'. +induction ld'. +exfalso. inversion H. subst. +inversion H. +subst. reflexivity. +subst. + +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 +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. Qed. - -[...] - Theorem compare_same : forall d1 d2, compare_dl d1 d2 = true -> same d1 d2. -[...] + 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. Qed. diff --git a/tp2.v b/tp2.v new file mode 100644 index 0000000..7a9865d --- /dev/null +++ b/tp2.v @@ -0,0 +1,561 @@ +(*** TP 2 : Loqique, booléens, propositions et IMP ***) + + +(** Note : si au bout d'une heure votre TP-man oublie de le dire, passez à la partie sur les listes !! *) + + +(** * Logique "avancée" et Coq : négation, booléens et Prop **) + +(* Négation *) +(* On peut voir le faux, noté False, comme un connecteur logique, qui +peut être inséré dans le "tableau" où figuraient la conjonction et +l'existentielle dans l'énoncé du TP 1 : + + connecteur | pour utiliser | pour construire + ----------------|---------------|--------------------- + P /\ Q | destruct H. | split. + P \/ Q | destruct H. | left. / right. + exists x:nat, P | destruct H. | exists 17. + False | destruct H. | + +Devinez : +- pourquoi il n'y a pas de tactique dans la colonne "pour construire" de ce tableau. +- ce que fait "destruct H." si H est une hypothèse qui dit False. *) + +(* A vous de jouer : prouvez les lemmes suivants *) + +Lemma ex_falso: forall P : Prop, False -> P. +intros P H. +destruct H. +Qed. + +(* Si l'on a A:Prop, alors ~A, la négation de A, est une notation pour "A -> False". *) +(* Si la notation vous perturbe, vous pouvez toujours utiliser la tactique [unfold not.] *) + +Lemma not_not : forall P : Prop, P -> ~~P. +intro P. +intros H. +unfold not. +intros H0. +apply H0. +apply H. +Qed. + +Lemma morgan1 : forall P Q : Prop, ~P \/ ~Q -> ~(P /\ Q). +intros P Q. +intro H. +unfold not. +intros HH. +destruct HH. +destruct H. +apply H. +apply H0. +apply H. +apply H1. +Qed. + +Lemma morgan2 : forall P Q : Prop, ~P /\ ~Q -> ~(P \/ Q). +intros P Q H. +destruct H. +intro HH. +destruct HH. +apply H. +apply H1. +apply H0. +apply H1. +Qed. + + +(* Pour la prochaine preuve, vous aurez besoin d'une nouvelle tactique : + [inversion H.] +Formellement, lorsque l'on appelle [inversion H], Coq essaye de +trouver les conditions nécessaires pour que l'hypothèse H soit vérifiée. +Coq fait aussi quelques simplifications lorsque l'on utilise inversion : si H est fausse, alors +il termine automatiquement la preuve, si H implique une égalité entre 2 expressions, il fait +parfois automatiquement le remplacement. +Essayez cette tactique sur les prochains lemmes pour comprendre comment elle marche en pratique *) + +Lemma zero_un : ~(0=1). + intro H. + inversion H. +Qed. +(*Notez que "x <> y" est un raccourci de "x = y -> False".*) + +(* Un autre exemple d'application de la tactique inversion, indépendamment de la négation *) +Lemma S_out : forall n m : nat, S n = S m -> n = m. + intros n m H. + inversion H. + reflexivity. +Qed. + + +(* Dans le même style, les différents constructeurs d'un type inductif ne peuvent pas renvoyer la même valeur. +Revenons sur la tentative de définition des entiers avec le successeur ET le prédécesseur, évoquée en cours. *) +Inductive t : Set := + Ze : t | Pr : t -> t | Su : t -> t. + +Lemma S_et_P : forall x y, Su x = Pr y -> False. + intros x y H. + inversion H. +Qed. + +(** Food for thought : à méditer après ce TP, ou si par hasard vous avez fini +le reste avant la fin. Avec la syntaxe au-dessus, il est évident que le +"prédécesseur" du "successeur" de "zéro" et "zéro" ne définissent pas le même + objet: *) + +Lemma PSZ: Pr (Su Ze) = Ze -> False. + intros H. inversion H. +Qed. + +Require Export ZArith. + +(** Sauriez-vous montrer la même chose en remplaçant "zéro" par un x (de type t) +quelconque ? +On insiste sur le fait que cette question est plutôt pour emmener à la maison +que pour pendant le TP. Nous serons par ailleurs ravis de recevoir des mails +si vous avez des questions là-dessus. +Un indice : souvenez-vous de vos cours de maths, où vous avez sûrement été déjà +amené.e.s à prouver des résultats plus forts et plus généraux pour parvenir à +vos fins. +Si besoin, vous pourrez vous servir de la tactique [omega] (chargée avec la +librairie ZArith au-dessus, pour résoudre de buts arithmétiques (notamment +obtenir faux à partir d'une hypothèse évidemment fausse comme x < x ou 2 < 0), +et vous pouvez aussi invoquer la tactique [Search bla] pour chercher des lemmes +contenant "bla", comme dans: *) + +Search "<" "S". + + + +Lemma inj_PS: forall x, Pr (Su x) = x -> False. + induction x. + apply PSZ. + intro H. + inversion H. + apply IHx. + Abort. + + + + +(** * Les booléens et les propositions **) + +(* Il y a en Coq deux moyens d'exprimer des affirmations logiques, avec des booléens (le type bool) ou +des propositions (le type prop *) +Check True. +Check False. +Check true. +Check false. + +(*Un booléen est soit "true" soit "false". Ainsi, si on définit la fonction "and" suivante : *) + +Definition Booland a b := match a,b with + | true,true => true + | true,false => false + | false,true => false + | false,false => false +end. + +(* Et qu'on l'évalue, on obtient soit true, soit false *) + +Eval compute in (Booland false true). +Eval compute in (Booland true true). + + +(* Il est important de garder à l'esprit que ceci est spécifique au type "bool". +En effet, un objet de type "Prop" n'est pas quelque chose que l'on peut +simplifier soit en True soit en False, mais plutôt un énoncé dont on peut +avoir une preuve (preuve que l'on peut construire en Coq à l'aide de tactiques). +*) + + +Eval compute in (False /\ True). + +(* On va travailler un peu sur ces différences dans un exemple *) +(* On donne deux moyens de prouver qu'un entier est pair. *) + +Definition not a := match a with + |false => true + |true => false +end. + +Fixpoint evenb n := match n with + | 0 => true + | S n' => not (evenb n') +end. + +Definition even_bool n := evenb n = true. + +(* Prouvez que 42 est pair avec cette définition *) + +Lemma even_42_bool : even_bool 42. + unfold even_bool. + unfold evenb. + simpl. + reflexivity. +Qed. + +(* Une seconde définition avec une fonction "double" *) + +Fixpoint double n := match n with + |0 => 0 + |S n' => S (S (double n')) +end. + +Definition even_prop n := exists k, n = double k. + +(* Prouvez une nouvelle fois que 42 est pair *) + +Lemma even_42_prop : even_prop 42. + unfold even_prop. + exists 21. + unfold double. + reflexivity. +Qed. + +(* Et maintenant, on va prouvez que finalement, ces deux définitions sont équivalentes *) +(* On aura besoin pour cela de lemmes auxiliaires, prouvez les. *) +(* Indice : Vous pouvez utiliser la tactique [case a] quand "a" est un booléen pour traiter les deux cas "true" et "false". +Cela ne modifiera que dans l'objectif.*) + +Lemma Not_invol : forall a, not (not a) = a. + intro a. + case a. + simpl. reflexivity. + simpl. reflexivity. +Qed. + +Lemma Not_false : forall a, not a = false -> a = true. + intro a. + case a. + simpl. + intro H. reflexivity. + simpl. intro H. inversion H. +Qed. + +Lemma Not_true : forall a, not a = true -> a = false. + intro a. case a. + intro H. inversion H. + intro H. reflexivity. +Qed. + +Lemma evenb_double : forall k, even_bool (double k). + intro k. + unfold even_bool. + induction k. + simpl. reflexivity. + simpl. + rewrite (Not_invol (evenb (double k))). + apply IHk. + +Qed. + +Lemma moinsDeuxParite : forall n, (even_bool (S (S n))) -> (even_bool n). + intro n. + intro H. + unfold even_bool in H. + unfold evenb in H. + fold evenb in H. + rewrite Not_invol in H. + trivial. +Qed. + +(*Tentez de prouver que la définition booléenne implique la définition propositionnelle*) +Lemma even_bool_to_prop : forall n, even_bool n -> even_prop n. + + cut (forall n, (even_bool n -> even_prop n) /\ (even_bool (S n) -> even_prop (S n))). + intros. + destruct (H n). + apply H1. + apply H0. + + induction n. + split. + + intro H. + unfold even_prop. + exists 0. + simpl. + reflexivity. + + intro H. + unfold even_bool in H. + unfold evenb in H. + apply Not_true in H. + inversion H. + + destruct IHn. + split. + apply H0. + + intro HH. + unfold even_prop. + unfold even_bool in HH. + apply moinsDeuxParite in HH. + apply H in HH. + unfold even_prop in HH. + destruct HH. + exists (S x). + simpl. + rewrite H1. + reflexivity. +Qed. + +(* Dans certains cas, on aura besoin d'une hypothèse d'induction plus forte que ce l'on souhaite prouver. +Note : Comme l'hypothèse d'induction 'est' notre objectif, "intro H. induction x" donnera une hypothèse d'induction +plus faible que "induction x" puis "intro H" dans les sous-cas.*) +(* Comprenez et completez la preuve à trous suivante: *) + +Lemma evenb_double_conv : forall n, +(evenb n = true -> exists k, n = double k) /\ (evenb n = false -> exists k, n = S (double k)). +induction n. + (* Traitez le cas n = 0 de l'induction *) + split. + intro H. + exists 0. + simpl. + reflexivity. + intro H. + inversion H. + (* Début du cas successeur : *) + simpl. destruct IHn. split. + intros. destruct H0. (* Premier cas du split à traiter. Si vous avez du mal à lire l'intérface Coq, n'hésitez pas à demander de l'aide *) + apply Not_true in H1. assumption. + apply Not_true in H1. exists (S x). rewrite H0. simpl. reflexivity. + intros. destruct H. (* Deuxième cas du split à traiter *) + apply Not_false in H1. assumption. + exists x. rewrite H. reflexivity. +Qed. + +(* On peut maintenant prouver l'équivalence entre les deux *) +Lemma even_bool_prop : forall n, even_prop n <-> even_bool n. + intro n. + split. + intro H. + unfold even_prop in H. + destruct H. + rewrite H. + apply evenb_double. + + apply even_bool_to_prop. +Qed. + +(* Sur cet exemple, vous avez normalement constaté qu'il est plus difficile de travailler sur +les preuves avec les booléens que les propositions. +En effet, on est passé assez facilement des propositions aux booléens (evenb_double) mais l'inverse était plus compliqué. *) + +(* En revanche, sur la preuve que 42 est paire, sur les booléens il n'y a presque rien à faire, mais pour les propositions, +il faut au minimum donner l'entier correspondant à l'existentiel... *) +(* Ou bien, si on ne veut pas donner l'entier, on peut faire la preuve suivante... *) + +Lemma even_42_prop_bis : even_prop 42. +apply even_bool_prop. reflexivity. Qed. + +(* Sur cet exemple, on ne gagne pas vraiment à utiliser cette preuve. Mais sur certains cas, il peut être utile de connaitre cette +technique. Un exemple extreme serait la preuve en Coq du théorème des 4 couleurs, +dans laquelle ce procédé est utilisé pour qu'une preuve qui aurait eu besoin d'une analyse de centaines de cas soit +capturé par un calcul sur les booléens. *) + +(* Un exemple plus simple serait le suivant. Prouvez ce lemme *) + +Lemma not_even_1001 : ~(even_bool 1001). + intro H. + unfold even_bool in H. + unfold evenb in H. + repeat (apply Not_true in H;apply Not_false in H). + apply Not_true in H. + inversion H. +Qed. + +(* Et celui-ci ? Voyez-vous le problème ?*) + +Lemma not_even_1001_bis : ~(even_prop 1001). + intro H. +Abort. + + + +(* Petit bonus : La fin de cette partie permet de vous familiariser d'avantager aux équivalences bool/Prop. +Il n'est pas nécessaire de la faire en TP, particulièrement si vous avez l'impression d'être en retard.*) +(* Si Coq râle, n'hésitez à commenter les parties non faites *) + +(* Prouvez le lemme suivant *) + +Lemma andb_true_iff : forall a b, Booland a b = true <-> (a = true /\ b = true). + Abort. + +(* Définissez la fonction "Boolor" pour les booléens *) + +Fail Definition Boolor a b := 0. + +(* Prouvez comme ci-dessus l'équivalence avec \/ *) + + + +(* Fin du bonus. *) + + + + +(** * Prédicats inductifs, listes et relations **) + +Require Import List. + +(* On va définir des prédicats sur des listes. Pour simplifier, on supposera qu'il s'agit de listes d'entiers.*) + +Definition listn := list nat. + +(* Inspirez vous de ce que vous avez vu en cours pour écrire le prédicat inductif (is_size l n) qui signifie que l est de taille n *) +Inductive is_size :listn -> nat -> Prop := + | size_nil : is_size nil 0 + | size_cons : forall (x:nat) (l:list nat) (n:nat), (is_size l n) -> (is_size (x::l) (S n)). + +(* La tactique [inversion H] ne sert pas que dans les égalités, en fait, elle fonctionne aussi sur tous les prédicats inductifs. +Elle va vérifier quels cas sont possibles. Cela se voit dans le lemme suivant: *) + +Lemma non_empty_size : forall p l n, is_size (p::l) n -> n <> 0. + intros p l n. + intro H. + inversion H. + intro HH. + inversion HH. +Qed. + +(* Définissez un prédicat (mem l x) qui signifie que x ∈ l *) +Inductive mem : listn -> nat -> Prop := + | mem_in : forall x l, mem (x::l) x + | mem_cons : forall a x l, mem l x -> mem (a::l) x. + +(* Le prédicat (update l x y l') signifie que l' est obtenu en + remplaçant la première occurence de x dans l par y. *) + +(* On vous donne un des cas : + + ──────────────────────────────── head + update (x::l) x y (y::l) + +*) + +(* Ecrivez ce prédicat *) +Inductive update : listn -> nat -> nat -> listn -> Prop := + | update_yep : forall x y l, update (x::l) x y (y::l) + | update_end : forall x y z l l', update l x y l' -> z<>x -> update (z::l) x y (z::l'). +(* update_nil : forall x y, update nil x y nil *) + + +(* Pour montrer une cohérence entre les deux prédicats, prouvez le lemme suivant *) +Lemma update_mem : forall l x y l', update l x y l' -> mem l x. + induction l. + intros. + inversion H. + intros x y. + intro l'. + case l'. + intro HH. + inversion HH. + intros n ll. + intro HH. + inversion HH. + subst. + apply mem_in. + subst. + apply mem_cons. + apply (IHl x y ll). + assumption. + +Qed. + +(* On pourrait prouver de manière similaire "forall l' l x y, update l x y l' -> mem l' y." *) + +(* Petit bonus *) +(* Pour prouver une implication dans l'autre sens, vous pourrez avoir besoin du lemme suivant: *) +Lemma eq_dec : forall n m : nat, n = m \/ n <> m. + induction n. + intro m. + case m. + left. reflexivity. + intro mm. + right. intro HH. inversion HH. + + intro m. + destruct (IHn (S m)). + right. + intro. + rewrite H in H0. + inversion H0. +Qed. + +Lemma mem_update : forall l x, mem l x -> forall y, exists l', update l x y l'. +[...] +Qed. + +(* P.S : Si vous avez réussi à le prouver sans utiliser le lemme au-dessus, +votre définition de mem aurait probablement pu être plus simple. *) + +(* Fin du petit bonus *) + +(* On considère les listes et on définit une relation binaire inductive sur les listes. On note +"perm l1 l2" cette relation, avec l'idée que "perm l1 l2" représente 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) + + +*) + +Inductive perm : [...]:= +[...]. + +(* Petit bonus *) +(* Vous vous êtes peut être demandé pourquoi est-ce que l'on a pris cette règle-là pour head et pas une autre ? + Notamment, on aurait pu penser à prendre cette règle-ci : + + perm l₁ l₂ + ─────────────────────────────(head') + perm (x::y::l₁) (y::x::l₂) + +On peut cependant prouver que l'on a pas besoin de cette règle. +Pour vous aider à comprendre pourquoi, montrez d'abord l'exemple suivant. *) + +Lemma perm_example : perm (1::2::4::5::3::nil) (2::1::4::3::5::nil). +[...] +Qed. + +(* Prouvez maintenant le lemme suivant, montrant que la règle donnée + précédemment est vraie dans notre définition. *) + +Lemma perm_head_alt : forall x y l1 l2, perm l1 l2 -> perm (x::y::l1) (y::x::l2). +[...] +Qed. + +(* Fin du petit bonus *) + + + +Parameter X : Set. +Definition relation:= X -> X -> Prop. + +(* Définir le prédicat inductif union R1 R2 qui est l'union de deux relations *) +Inductive union : relation -> relation -> X -> X -> Prop := +[...] + +(* De même pour l'intersection *) +Inductive inter : relation -> relation -> relation := +[...] + +(* Pour comparer des relations entre elles, il faut définir la notion d'égalité, '=' est trop fort ici.*) +Definition equal : relation -> relation -> Prop := [...] + +(* On peut maintenant prouver la distributivité entre les deux par exemple *) +Lemma distr : forall R1 R2 R3, equal (inter (union R1 R2) R3) (union (inter R1 R3) (inter R2 R3)). +[...] +Qed.