502 lines
14 KiB
Coq
502 lines
14 KiB
Coq
|
|
(*** 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<b je fais ça et sinon
|
|
je fais ça", il faut utiliser les tactiques suivantes :
|
|
[remember expr as x]
|
|
qui permet de mettre en hypothèse "x = expr", avec "x" du même type que "expr".
|
|
[destruct x]
|
|
Quand x est de type "comparison", destruct x permet de traiter les trois cas
|
|
possibles de la comparaison.
|
|
|
|
Ainsi, vous aurez en hypothèse, grâce à [remember], la valeur de Nat.compare. *)
|
|
|
|
(* Enfin, vous devez utiliser les lemmes suivant pour passer d'un Nat.compare
|
|
aux relations usuelles. *)
|
|
|
|
Check PeanoNat.Nat.compare_eq_iff.
|
|
Check PeanoNat.Nat.compare_lt_iff.
|
|
Check PeanoNat.Nat.compare_gt_iff.
|
|
|
|
(* Allez-y, prouvez que insert_sort est effectivement un tri. Bonne chance *)
|
|
|
|
|
|
|
|
Lemma insert_sort_correct : forall l, sorted (insert_sort l).
|
|
[...]
|
|
Qed.
|
|
|
|
|
|
|
|
(*** Bonus ***)
|
|
|
|
(* Si par hasard vous finissiez ce TP avant l'heure, signalez-le à vos chargés
|
|
de TP qui se feront une joie de vous faire quelques suggestions d'exercices
|
|
supplémentaires. *)
|
|
|
|
|
|
|
|
|
|
|