coq-en-stock/tp7.v

(*** 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.


(*******************)