Require Import Arith. (* Quelques tactiques utiles, qu'on verra au fur et a mesure : - auto - auto with arith - assumption - assert (un énoncé) H12 - replace (un terme) with (un autre) - inversion H. *) (** Partie I : Sémantique à grands pas *) (* Considérons la grammaire d'expressions suivante, avec les mots inhabituels "Randombit" et "AssertZero", qui sont expliqués plus bas. *) Inductive expr : Set := | N : nat -> expr | Randombit : expr | Plus : expr -> expr -> expr | Mult : expr -> expr -> expr | Minus : expr -> expr -> expr | AssertZero : expr -> expr -> expr. Infix "[+]" := Plus (at level 50, left associativity). Infix "[*]" := Mult (at level 40, left associativity). Infix "[-]" := Minus(at level 50, left associativity). Notation "[?]" := Randombit. (* Donnez une sémantique à grand pas avec le sens suivant : - N n représente l'entier n ------- N n → n - Plus, Mult et Minus comme en cours e₁ → n₁ e₂ → n₂ ------------------- e₁ [+] e₂ → n₁ + n₂ ... - Randombit peut engendrer 0 peut engendrer 1 ------- ------- [?] → 0 [?] → 1 - AssertZero e1 e2 s'assure que e1 peut réduire vers 0 et se comporte comme e2 dans ce cas. e₁ → 0 e₂ → n₂ --------------------- AssertZero e₁ e₂ → n₂ *) Inductive bs : expr -> nat -> Prop := | bs_nat : forall n, bs (N n) n | bs_randombit_0 : bs [?] 0 | bs_randombit_1 : bs [?] 1 | bs_plus : forall e1 e2 n1 n2, bs e1 n1 -> bs e2 n2 -> bs (e1 [+] e2) (n1+n2) | bs_mult : forall e1 e2 n1 n2, bs e1 n1 -> bs e2 n2 -> bs (e1 [*] e2) (n1*n2) | bs_minus : forall e1 e2 n1 n2, bs e1 n1 -> bs e2 n2 -> bs (e1 [-] e2) (n1-n2) | bs_assertZero : forall e1 e2 n2, bs e1 0 -> bs e2 n2 -> bs (AssertZero e1 e2) n2. (* | bs_assertZeo_false : forall e1 e2 n2, not (bs e1 0) -> bs e2 n2 -> bs (AssertZero e1 e2) n2. *) (* Question : Essayez de définir une telle sémantique pour faire en sorte que "AssertZero e1 e2" se comporte comme "e2" si "e1" ne peut PAS se réduire vers 0. Coq accepte-t'il la définition ? Pourquoi ? *) Lemma expression_example : bs (AssertZero (N 2 [-] [?] [-] [?]) (N 5 [*] N 3)) 15. constructor. replace 0 with (1-1). constructor. replace 1 with (2-1). constructor. simpl. constructor. constructor. trivial. constructor. trivial. replace 15 with (5*3). constructor. constructor. constructor. trivial. (* replace expr1 with expr2 => substitue expr1 par expr2 et un but apparait pour prouver l'égalité *) Qed. (** Partie II : Petits prédicats inductifs *) (* Réflechissez un peu au sens de nat -> Prop *) (* En plus des types de données inductifs, Coq permet de définir des propriétés inductives. Par exemple, la propriété que un nat est pair peut être définie de la facon suivante : *) Inductive even : nat -> Prop := | even_zero : even 0 | even_succ : forall n, even n -> even (S (S n)). (* even n -------- -------------- even 0 even (S (S n)) *) (* Définissez vous-même le prédicat "odd" pour designer les impairs. Essayez de trouver une définition avec un seul constructeur. *) Inductive odd : nat -> Prop := | odd_succ : forall n, even n -> odd (S n). (* [inversion H] est une tactique compliquée qui élimine les cas impossibles dans les types inductifs. Servez-vous en pour prouver : *) Lemma not_even: ~ odd 0. intro. inversion H. Qed. Lemma odd_even : forall n, odd n -> even (S n). intro. induction n. intro. inversion H. intro. inversion H. constructor. assumption. Qed. Lemma eventwo_times : forall n, even (n * 2). (* vous pouvez essayer "assumption" et "constructor" *) induction n. simpl. constructor. simpl. constructor. assumption. Qed. Lemma odd_or_even : forall n, even n \/ odd n. intros. induction n. left ; constructor. destruct IHn. right. constructor. assumption. left. apply odd_even. assumption. Qed. Lemma evenS_odd : forall n, even (S n) -> odd n. intro. intro. inversion H. constructor. assumption. Qed. Lemma oddS_even : forall n, odd (S n) -> even n. intros. inversion H. assumption. Qed. (* Conseil: utilisez inversion. *) Lemma odd_and_even : forall n, ~ (even n /\ odd n). (* induction n; intros [H1 H2]. inversion H2. apply IHn; split. apply oddS_even; assumption. apply evenS_odd; assumption. *) intros. intro. induction n. destruct H. inversion H0. apply IHn. destruct H. split. apply oddS_even ; assumption. apply evenS_odd ; assumption. Qed. (* Un autre prédicat : nombres de la suite de Hamming *) (* L'ensemble H de Hamming est le plus petit ensemble défini de la manière suivante : 1 est dans H, et si n est dans H alors 2n, 3n, et aussi 5n sont dans H *) Inductive hamming : nat -> Prop := | H1 : hamming 1 | H2 : forall n, hamming n -> hamming (2 * n) | H3 : forall n, hamming n -> hamming (3 * n) | H5 : forall n, hamming n -> hamming (5 * n). (** Partie III : Types de donnees inductifs *) (* En coq, on peut définir des nouveaux types de données (habitant dans Set) via des définitions inductives. On a vu dans le TP1 le type des entiers naturels. *) Print nat. (* De facon informelle, quand on definit un type inductif on donne toutes les manières de construire un élément de ce type. Un entier naturel est soit zéro (construit par le constructeur "O"), soit le successeur d'un autre entier naturel (construit par le constructeur "S"). n : nat ---------- -------------- 0 : nat S n : nat Un autre exemple : le type des booleens. ----------- ------------ true : bool false : bool *) Print bool. (* Définir le type "listN" de liste des entiers naturels avec deux constructeurs : "videN" qui permet de construire la liste vide et "consN" qui permet de construire une nouvele liste à partir d'un entier et une liste. l : listN n : nat ------------- -------------------------- videN : listN consN n l : listN Chaque fois qu'on définit un type inductif, Coq génère un principe d'induction pour ce type. *) Inductive listN := | videN : listN | consN : nat -> listN -> listN. Check listN_ind. Check nat_ind. Check bool_ind. (* Ce principe va être automatiquement invoqué quand on utilise la tactique [induction]. Morale : on peut utiliser [induction] pour faire de preuves sur tous les types inductifs. *) (* Définir la fonction "longN" qui prend en argument une "listN" et retourne un "nat" représentant la longeur de la liste. Définir la fonction "concatN" qui prend en argument deux listes et retourne la concatenation de ces deux listes. Enfin, montrer les propriétés suivantes : *) Fixpoint longN (l: listN) := match l with | videN => 0 | consN n l => 1 + longN l end. Fixpoint concatN (l : listN) (l' : listN) := match l with | videN => l' | consN x l => consN x (concatN l l') end. Eval compute in concatN (consN 1 (consN 2 videN)) (consN 3 (consN 4 videN)). Infix "++" := concatN (right associativity, at level 60). Infix "::" := consN (right associativity, at level 60). Notation " [] " := videN. Eval compute in concatN (1 :: 2 :: []) (3 :: 4 :: []). Lemma videN_concat : forall l, [] ++ l = l. Proof. auto. Qed. Lemma concat_videN : forall l, l ++ [] = l. Proof. intro. induction l. simpl. reflexivity. simpl. rewrite IHl. reflexivity. (* induction l; simpl; try rewrite IHl; reflexivity.*) Qed. Lemma long_concat: forall (l1 l2 : listN), longN (l1 ++ l2) = longN l1 + longN l2. Proof. intros. induction l1. simpl ; trivial. simpl. f_equal. rewrite IHl1. reflexivity. Qed. Lemma concat_assoc : forall x y z, x ++ (y ++ z) = (x ++ y) ++ z. Proof. intros. induction x. simpl ; trivial. simpl. rewrite <- IHx. trivial. Qed. (** Partie IV : Retournement de listes *) (* Définir une fonction "rev" qui retourne (dans les deux sens du terme) une liste en utilisant la fonction "concatN" puis prouver que c'est une involution, en s'aidant de ces lemmes intermédiaires. *) Fixpoint rev (l : listN) := match l with | [] => [] | x::l => concatN (rev l) (x::[]) end. Lemma rev_concat : forall xs ys, rev (xs ++ ys) = rev ys ++ rev xs. intros. induction xs. simpl. Lemma concat_vide : forall l, l = l ++ []. induction l. simpl ; trivial. simpl. rewrite <- IHl. trivial. Qed. apply concat_vide. simpl. rewrite IHxs. rewrite concat_assoc. reflexivity. Qed. Lemma rev_singleton : forall xs x, rev (xs ++ (x :: [])) = x :: rev xs. intros. apply rev_concat. Qed. Lemma rev_involution : forall l, rev (rev l) = l. intros. induction l. simpl ; trivial. simpl. rewrite rev_singleton. rewrite IHl. reflexivity. Qed. (* Ce n'est pas très économique de retourner des listes en appelant à chaque fois "concatN". Trouver une solution plus rapide puis prouver l'équivalence des deux. *) Fixpoint revconcat (xs ys : listN) := match xs with | [] => ys | x::xs => revconcat xs ( x :: ys) end. Eval compute in revconcat (1::2::3::[]) (5::7::[]). Definition revopt (l : listN) := revconcat l []. Lemma revconcat_correct : forall xs ys, revconcat xs ys = rev xs ++ ys. Proof. intros xs. induction xs. intros ys. simpl. auto. intros ys. simpl. rewrite IHxs. rewrite <-concat_assoc. auto. Qed. Lemma revopt_correct : forall l, revopt l = rev l. Proof. intros l. unfold revopt. rewrite revconcat_correct. apply concat_videN. Qed.