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