Séance du 12 novembre

tp7.v

@@ -0,0 +1,457 @@
+(*** TP7 : Coinduction et induction bien fondée ***)
+
+(*** Partie 1 : Divergence et coinduction ***)
+
+(* Rappel de certaines tactiques de Coq : 
+
+La tactique [constructor.] en Coq permet d'utiliser directement un constructeur 
+d'une définition inductive sans redonner son nom (Coq le cherchera de lui même) 
+
+[apply H with v.] 
+Parfois, en utilisant la tactique [apply] en Coq, vous aurez le message d'erreur 
+suivant: "Error: Unable to find an instance for the variable x."
+Dans ce cas là, Coq n'arrive pas à deviner tout seul quel choix il doit faire 
+pour la variable x de la proposition H. En utilisant [apply H with v], vous 
+pouvez indiquer à Coq qu'il faut prendre "v" comme valeur pour la variable "x". 
+
+[assumption.]
+ Si vous devez prouver "H" et que "H" est en hypothèse, assumption termine 
+automatiquement la preuve. 
+
+[inversion H.] 
+Demande à Coq de trouver les conditions nécéssaires pour que l'hypothèse H soit 
+vraie. Dans le cas ou H est fausse, inversion termine directement la preuve. 
+
+[unfold f.] 
+Lorsque "f" est une définition, unfold permet de remplacer le nom "f" par sa 
+définition. La variante [unfold f in H] permet de remplacer "f" par sa 
+définition dans l'hypothèse H.
+
+[simpl.] 
+Demande à Coq de simplifier le but, en appliquant des fonctions par exemple.
+
+[case a.] 
+Quand "a" est un objet défini par une définition inductive, "case a" permet de 
+traiter les différents cas possibles de la définition.
+
+[subst.] Lorsque vous utilisez cette tactique, Coq simplifie vos hypothèse en 
+utilisant des substitutions intelligentes, par exemple "a=b", "b = c", "c = d", 
+et "a + b = c + d" seront remplacés par "a + a = a + a".
+Très pratique lorsque vous avez utiliseé la tactique [inversion] juste avant,
+ qui introduit souvent des noms de variables pas très utiles.
+
+*)
+
+
+
+(* En cours, vous aviez vu que pour définir la divergence des programmes de IMP,
+   une définition inductive ne fonctionnait pas. Vous avez alors utilisé
+   Knaster-Tarski en version duale, en prenant un plus grand post-point fixe 
+   au lieu du plus petit pré-point fixe. *)
+
+(* On va illustrer ce principe en Coq, pour cela on va travailler sur la 
+   divergence dans un graphe orienté infini.  Le graphe que l'on considère 
+   est le suivant : 
+
+   Ensemble des sommets : 
+       { a ; b ; c ; d } ∪ { p n | n ∈ ℕ}
+   Arêtes : 
+       { (a,b) ; (b,c) ; (b,d) ; (d,b) ; (c,p 0) } ∪ { (p n,p (n+1)) | n ∈ ℕ }
+
+   Tout d'abord, formalisez en Coq ce graphe. *)
+
+Inductive state : Set := 
+  | a : state
+  | b : state
+  | c : state
+  | d : state
+  | p : nat -> state
+.  
+
+Inductive step : state -> state -> Prop :=
+  | step_ab : step a b
+  | step_bc : step b c
+  | step_bd : step b d
+  | step_db : step d b
+  | step_cp : step c (p 0)
+  | step_pp : forall n, step (p n) (p (S n))
+.
+
+
+(* On définit la divergence comme un prédicat **coinductif** :
+   on applique le théorème de Knaster-Tarski, pour raisonner sur le plus grand
+   post-point fixe d'un opérateur f. On rappelle qu'un post-point fixe pour f 
+   est un ensemble X tel que  X ⊆ f(X). *)
+
+(* Pour rappel, l'utilisation "classique" de Knaster-Tarski consiste à travailler 
+   sur le plus petit point fixe, qui est un ensemble X tel que f(X) ⊆ X. *)
+
+CoInductive diverges : state -> Prop :=
+| div : forall s1 s2, step s1 s2 -> diverges s2 -> diverges s1.
+
+(* Tout d'abord, des questions sur Knaster-Tarski:
+
+1] Quelle est la définition de l'opérateur f correspondant à la définition
+de "diverges" ci-dessus ? 
+f(X) = {x tq exists y€X step x y}
+
+2] Que donnerait cette définition si on remplaçait CoInductive par Inductive ?
+f(X) = {x tq exists y€X tq x --> y}
+
+*)
+
+(* On veut d'abord montrer qu'il existe une divergence à partir de a, 
+   en suivant la boucle b ⟳ d. Essayez de prouver ce lemme en utilisant
+   les tactiques que vous connaissez en Coq. Quel est le problème ? *)
+
+Lemma div_abd_fail : diverges a.
+cut (diverges b).
+apply (div a b).
+apply step_ab.
+repeat
+((apply (div b d));
+(apply (step_bd));
+(apply (div d b));
+(apply (step_db))).
+Abort.
+
+(* Pour résoudre ce problème, il vous faudra utiliser la "tactique miraculeuse" [cofix.]
+   ou [cofix H.], dont vous pourrez découvrir l'effet.
+   L'idée de "cofix" est d'ajouter en hypothèse le but que vous souhaitez prouvez...
+   Mais ne croyez pas trop aux miracles : [cofix.] suivi de [assumption.] engendrera une
+   erreur au moment de sauvegarder la preuve avec [Qed.] (ce que vous êtes invité.e.s à
+   vérifier).
+*)
+
+Lemma div_abd : diverges a.
+apply (div a b).
+apply step_ab.
+cofix H.
+apply (div b d).
+apply step_bd.
+apply (div d b).
+apply step_db.
+assumption.
+Qed.
+
+(*******************)
+
+
+(* Vous pouvez ensuite inspecter la preuve qui a été engendrée *)
+Print div_abd.
+
+
+(* Principe de preuve par coinduction *)
+(* Un ensemble d'états est représenté par une fonction :
+      f : state → bool 
+   correspondant à sa fonction indicatrice.
+   On définit un prédicat sur les ensembles d'états, pour dire qu'un 
+   tel ensemble est un post-point fixe (pour la fonction f donnée plus haut) *)
+
+(* Donnez cette définition *)
+Definition post_fixpoint (X : state -> bool) : Prop :=
+  forall y, X y = true -> (exists x, step y x /\ X x = true).
+
+
+(* Le théorème important exprime le principe de preuve par coinduction : 
+  tout post-point fixe est inclus dans le plus grand post-point fixe. 
+   Prouvez-le, en ayant à l'esprit qu'il faudra utiliser un cofix quelque part. 
+
+
+Post point fixe : X € f(X)*)
+
+Theorem coinduction : forall X : state -> bool, post_fixpoint X -> forall s, X s = true -> diverges s.
+intro.
+intro H.
+cofix Hc.
+unfold post_fixpoint in H.
+intro s.
+intro Hh.
+apply H in Hh. destruct Hh. destruct H0.
+apply (div s x). assumption.
+apply Hc. assumption.
+Qed.
+
+(*******************)
+
+
+
+(* On souhaite maintenant prouver que tous les sommets de la forme (p n) sont 
+   aussi divergents. Pourquoi la preuve précédente avec la boucle b ⟳ d pour a 
+   ne peut-elle pas marcher ? 
+
+Parce que y a un nombre arbitraire d'étapes *)
+
+(* Il faut donc utiliser plus en détail le principe de preuve par coinduction, 
+   et notamment s'aider de post-point fixes. *)
+
+(* Pour commencer, définissez l'ensemble Xp des sommets de la forme "p n". *)
+
+Definition Xp (s : state) : bool :=
+match s with
+  | a|b|c|d => false
+  | p n => true
+end.
+
+(* Prouvez ensuite le lemme suivant *)
+
+(* Si vous voulez, vous pouvez essayer ici la notation ";" de Coq. 
+   Lorsque vous lancez une preuve avec différents cas, le ";" permet d'appliquer 
+   les même tactiques à tous les cas sans copier/coller. Vous pouvez alors 
+   utiliser "try" pour essayer d'appliquer une tactique sans que Coq ne s'arrête 
+   s'il n'y arrive pas.  
+   Observez par exemple la preuve suivante : *)
+
+Lemma example_step : forall s, s = a \/ s = d -> step s b.
+intro s. case s;intros ;destruct H;try constructor; try inversion H.
+Qed.
+
+(* Tous les cas ont été traités d'un coup, on commence par un intros,
+   on fait une analyse de cas sur le "ou", puis si il y a un step 
+   vers b ("try constructor") on le fait, sinon c'est qu'on n'est ni a ni d, 
+   donc "try inversion H" doit finir la preuve *)
+
+(* Comprendre cette syntaxe n'est pas obligatoire, mais elle peut parfois 
+   accélerer les preuves, ce qui peut vous être utile. Vous pouvez trouver 
+   plus d'infos en ligne si vous voulez. *)
+
+Lemma inv_Xp : forall s, Xp s = true -> exists n, s = p n.
+  induction s; intro H; try simpl in H; inversion H.
+  exists n. reflexivity.
+Qed.
+
+(* Vous pouvez maintenant prouver la divergence des "p n" en vous aidant 
+   du théoreme  de coinduction *)
+
+(* Vous aurez sûrement besoin de la tactique suivante :
+   
+   [destruct f.]
+    
+    si "f" est le nom d'un lemme f : A -> B, "destruct f" vous permet de 
+    récuperer "B" dans vos hypothèses, mais Coq vous demandera de prouver 
+    également "A". C'est utile pour utiliser un lemme que vous avez prouvé 
+    précedemment mais pour lequel vous ne pouvez pas utiliser directement [apply].
+    Remarque : Comme [apply with ...], on peut aussi utiliser 
+       
+       [destruct with ...] 
+    
+    quand Coq n'arrive pas à deviner tout seul la valeur de certaines variables. *)
+
+Lemma div_p : forall n, diverges (p n).
+intro.
+destruct coinduction with Xp (p n).
+unfold post_fixpoint. intro. intro.
+apply inv_Xp in H.
+destruct H. subst.
+exists (p (S x)).
+split.
+apply step_pp.
+simpl. reflexivity.
+simpl. reflexivity.
+apply (div s1 s2).
+assumption.
+assumption.
+
+Qed.
+
+
+
+
+(*******************)
+
+
+
+
+(*** Partie 2 : Bonne fondation, accessibilité, définition de fonctions ***)
+
+(* Nous allons travailler ici sur les relations bien fondées *) 
+Print well_founded.
+
+(* En Coq, une relation de A*A est bien fondée si tous les éléments de A 
+   sont accessibles pour cette relation *)
+
+Print Acc.
+
+(* Un élément est dit accessible si tous ses prédécesseurs sont accessibles *)
+(* Notez que la définition d'Acc est similaire au PIBF.
+   Cependant, par rapport au cours, la relation considérée est la relation réciproque.
+   C'est-à-dire que la relation (nat, >) est terminante, mais pour Coq,
+   c'est < qui est bien-fondée. *)
+   
+(*Remarque : on peut avoir l'impression ici qu'il n'y a pas de cas de base,
+  et que donc Acc est toujours vide, mais il faut remarquer qu'un élément minimal 
+  pour R satisfait toujours Acc_intro. *)
+
+(* Pour résumer, une relation "R" est bien fondée, pour cette définition Coq de
+   bonne fondation, quand tous les élements sont atteignables à partir des éléments 
+   minimaux, de façon inductive. *)
+
+(* Pour commencer, montrez que la relation < est bien fondée *)
+Require Import Lt.
+
+(* Indice : La preuve suivante est valide: *)
+Lemma trivialité : forall x y, S x <= y -> x < y.
+  intros. apply H.
+Qed.
+
+Lemma lemme_nul : forall n y, y <= n -> y < n \/ y = n.
+
+induction n.
+intros.
+right. inversion H. reflexivity.
+induction y.
+intros. left. apply PeanoNat.Nat.lt_0_succ.
+intro H.
+simpl in H.
+Search le.
+apply PeanoNat.Nat.le_S_n.
+
+Theorem well_founded_lt : well_founded lt.
+Proof.
+intro n.
+induction n.
+apply Acc_intro.
+intros.
+inversion H.
+
+apply Acc_intro.
+inversion IHn.
+intro y.
+intro Hh.
+cut (y<n \/ y=n).
+intro.
+inversion H0.
+apply H in H1. assumption.
+subst. assumption.
+cut (y<=n).
+intro.
+Search le.
+apply H0.
+
+cut (y <= n).
+intro.
+apply H0.
+assumption.
+
+Qed.
+
+(*******************)
+
+
+(*** Accessibilité et divergence ***)
+Require Import Lists.Streams.
+
+(* le type des listes infinies -- **uniquement** infinies : pas de constructeur Nil. *)
+Print Stream.
+
+(* On souhaite donner la définition usuelle de relation bien fondée : 
+   "il n'existe pas de chaine infinie décroissante".
+   Pour faire ça, il faut d'abord définir la notion de chaine infinie décroissante en Coq, 
+   et surprise, on a besoin de coinduction pour ça. *)
+
+CoInductive infiniteDecreasingChain A (R : A -> A -> Prop) : Stream A -> Prop :=
+  | ChainCons : forall x y s, infiniteDecreasingChain A R (Cons y s) (*Si on a une chaine infinie décroissante de la forme y::s, avec s infinie décroissante *)
+    -> R y x   (* Si en plus on sait que x est plus grand que y *)
+    -> infiniteDecreasingChain A R (Cons x (Cons y s)). (* Alors x::y::s est aussi ine chaine infinie décroissante *)
+
+(* Définissez maintenant une notion alternative de "être bien fondée" en utilisant les chaines *)
+Definition wf2 A (R : A -> A -> Prop) := [...]
+
+(* Maintenant, prouvez que si un élément est accessible, il ne peux pas commencer de chaine infinie décroissante *)
+
+Lemma noBadChains : forall A (R : A -> A -> Prop) x, Acc R x 
+  -> forall s, ~infiniteDecreasingChain A R (Cons x s).
+[...]
+Qed.
+
+(* Prouvez maintenant le lemme suivant *)
+Lemma well_founded_bad_chains : forall A (R: A -> A -> Prop), well_founded R -> wf2 A R.
+[...]
+Qed.
+
+(*******************)
+
+
+
+(*** Donner des arguments de terminaison à Coq ***)
+
+Require Import ZArith.
+Require Import Recdef.
+Require Import List.
+
+(* Dans Coq, toutes les fonctions que vous donnez doivent terminer. Sur des 
+   fonctions récursives simples, Coq va trouver automatiquement qu'elles 
+   terminent en cherchant un objet qui décroit strictement à chaque appel 
+   récursif. Cependant, Coq n'arrive parfois pas à inférer ce qui décroit 
+   strictement, et il faut l'aider. *)
+
+(* Essayez d'écrire une fonction "merge", qui prend en entrée deux listes 
+   d'entiers triées et retourne la liste triée correspondant à la fusion 
+   de ces deux listes. Vous pouvez utiliser la  fonction "leb".
+ *)
+Check leb.
+
+
+Fixpoint merge_fail1 (p: list nat) (q: list nat) : list nat :=
+[...]
+
+(* Essayons également en utilisant la forme non curryfiée... *)
+
+
+Fixpoint merge_fail2 (p:list nat * list nat) : list nat :=
+[...]
+
+
+(* Coq devrait vous donner une erreur dans les deux cas. On va alors
+   l'aider à comprendre pourquoi cette fonction termine. *)
+
+(* Trouvez une fonction:
+
+        mesure : (list nat * list nat) → nat
+
+   telle que "mesure" décroit strictement dans les appels récursifs de merge. *)
+
+Definition mesure (p : list nat *list nat) :=
+[...]
+
+(* On va maintenant pouvoir définir la fonction merge. On utilise alors une autre syntaxe : 
+
+     [Function ... ]
+
+   généralise Fixpoint en autorisant à faire autre chose qu'une récurrence sur
+   la structure du premier argument de la fonction, on peut donc lui donner 
+   explicitement la mesure qui va décroitre. 
+
+   Coq va alors nous demander de prouver que cette mesure décroit effectivement 
+   Allez-y, definissez merge et prouvez que "mesure" décroit.
+ *)
+Function merge (p:list nat * list nat) { measure mesure p } : list nat :=
+[...]
+.
+[...]
+Qed.
+
+(*******************)
+
+
+(*** Retour aux relations bien fondées ***)
+
+(*Donnez la définition de l'ordre lexicographique sur le type bool*nat, 
+en prenant false est plus petit que true *)
+Inductive lexico : bool*nat -> bool*nat -> Prop :=
+[...]
+
+(* Prouvez ensuite que cet ordre est bien fondé. *)
+
+
+
+Theorem well_founded_lex : well_founded lexico.
+[...]
+Qed.
+
+
+(*******************)
+
+
+
+