(* dans ce td, on définit et on prouve le tri fusion *)

(* listes d'entiers *)
Inductive list  : Set :=
| nil: list 
| cons: nat -> list -> list.
Infix "::" := cons (at level 60, right associativity).

(* longueur d'une liste *)
Fixpoint length (l:list) :=
match l with
  | nil => 0
  | a::suite => S (length suite)
end.

(* préfixe de longueur n d'une liste *)
Fixpoint prefix (n:nat) (l: list) {struct n} : list:= 
match n with
  | 0 => nil
  | S p => match l with
             | nil => nil
             | a::suite => a::(prefix p suite)
           end
end.

(* zappage des n premiers éléments *)
Fixpoint suffix (n:nat) (l: list) {struct n}: list :=
match n with
  | 0 => l
  | S p => match l with
             | nil => nil
             | a::suite => (suffix p suite)
           end
end.


(* concaténation *)
Fixpoint app (l1 l2: list) {struct l1}: list :=
match l1 with
  | nil => l2
  | a::suite => a::(app suite l2)
end.

(* lemme d'échauffement, qui ne sera pas utilisé par la suite... *)
Lemma prefix_suffix : forall n l, app (prefix n l) (suffix n l) = l.
Proof.
induction n ; intro l.
  simpl. reflexivity.
  destruct l as [|a suite] ; simpl.
    reflexivity.
    rewrite (IHn suite). reflexivity. 
Qed.



(* on importe Arith pour accéder à le_ge_dec, qui décide le sur les entiers *)
Require Import Arith.
Check le_ge_dec.


(* prédicat indiquant si une liste est triée *)
Inductive sorted: list -> Prop := 
|SortedNil: sorted nil
|SortedElem: forall a, sorted (a::nil)
|SortedCons: forall a b suite, a<=b -> (sorted (b::suite)) -> sorted (a::b::suite).

(* fusion de deux listes (a priori triées) *)
Fixpoint merge (l l': list) (n:nat) {struct n}: list := 
match n with
  | 0 => nil
  | S p => match l with 
             | nil => l'
             | a::suite => match l' with
                            | nil => l
                            | b::suite' => if (le_ge_dec a b)
                                           then a::(merge suite l' p)
                                           else b::(merge l suite' p) 
                           end
           end
end.

(* on va prouver que la fusion de deux listes triées est triée, le
   prédicat suivant sera utile: il indique lorsque le premier élément
   d'une liste (la troisième) est le premier élément d'une des deux
   autres listes données *)
Inductive first_elem: list -> list -> list ->  Prop :=
| first_elem_0: forall l1 l2, first_elem l1 l2 nil
| first_elem_1: forall x l1 l2 l3, first_elem (x::l1) l2 (x::l3)
| first_elem_2: forall x l1 l2 l3, first_elem l1 (x::l2) (x::l3).

(* quand on fusionne, on satisfait cette propriété *)
Lemma merge_first_elem : forall n l1 l2,
  first_elem l1 l2 (merge l1 l2 n).
Proof.
induction n.
  simpl. constructor.
  intros [|a1 suite1] [|a2 suite2] ; simpl ; try constructor.
  destruct (le_ge_dec a1 a2) ; constructor.
Qed.

     
(* préservation du tri par la fusion *)
Theorem merge_sorted: forall n l1 l2,
  sorted l1 -> sorted l2 -> sorted (merge l1 l2 n).
Proof.
Qed.


(* fonction de séparation d'une liste en deux listes de taille *)
(* comparables.                                                *)

Fixpoint split (l:list) : list * list := ...


(* le tri fusion se déduit naturellement (on utilise encore un *)
(* entier pour borner la récursion                             *)
Fixpoint pre_sort l n {struct n} : list := ...

(* Il suffit de donner un entier suffisament grand pour que a marche *)
Definition sort l := pre_sort l (length l).

(* Nous allons montrer que sort renvoie bien une liste triée. Remarquons *)
(* que, en fait, pre_sort lui-même renvoie toujours une liste triée,     *)
(* quelque soit la valeur de n. Nous montrons donc le théorème plus      *)
(* général suivant :                                                     *)
Theorem pre_sort_sorts : forall n l, sorted (pre_sort l n).
Proof.
Qed.

(* le tri fusion renvoie effectivement des listes triées *)
Theorem sort_sorts : forall l, sorted (sort l).
Proof.
Qed.



(* Une seconde approche pour le tri fusion est de construire *)
(* une liste de listes toutes triées.  Au premier tour, on   *)
(* transforme une liste de n éléments en une liste de n      *)
(* listes à un élément chacune.  Ensuite à chaque tour on    *)
(* fusionne la première liste avec la deuxième, puis la      *)
(* troisième avec la quatrième, et ainsi de suite jusqu'à ce *)
(* qu'il n'y ait plus qu'une seule liste.                    *)

(* Liste de listes *)
Inductive listlist  : Set :=
| empty: listlist 
| conslist: list -> listlist -> listlist.

(* longueur d'une liste *)
Fixpoint lengthlist (ll:listlist) :=
match ll with
  | empty => 0
  | conslist l suite => S (lengthlist suite)
end.

(* Comme d'habitude, on va écrire une fonction structurelle  *)
(* sur un argument naturel                                   *)
(* imerge_sort: nat -> listlist -> list                      *)
(* où (imerge_sort n ll) est la liste triée contenant la     *)
(* concaténation de toutes les listes contenues dans ll si n *)
(* est plus grand que la longueur de ll.  En fait n décroit  *)
(* d'une unité à chaque tour de réucrrence structurelle,     *)
(* mais la longueur de ll est divisée par deux.              *)

(* la fonction imerge_sort devra faire appel à la fonction   *)
(* auxiliaire qui effectue la fusion de la première et de la *)
(* deuxième, de la troisième et de la quatrième, etc.        *)
(* Cette fonction aura le type suivant:                      *)
(*      imerge_aux : listlist -> listlist                    *)

(* Écrire la fonction imerge_aux, définir la proposition     *)
(* inductive sorted_lists: listlist -> Prop                  *)
(* qui exprime que toutes les listes présentes dans          *)
(* l'argument sont triées et démontrer les théorèmes         *)
(* suivants (on pourra ajouter des lemmes intermédiaires     *)
(* bien choisis).                                            *)

Fixpoint imerge_aux (ll:listlist) : listlist := ...

Inductive sorted_lists: listlist->Prop := ...

Theorem imerge_aux_shorter : forall (ll : listlist),
    1 < (lengthlist ll) -> (lengthlist (imerge_aux ll)) < (lengthlist ll).
Proof.
Qed.

Theorem imerge_aux_sorted : forall (ll : listlist),
  sorted_lists ll -> sorted_lists (imerge_aux ll).
Proof.
Qed.

(* Écrire la fonction imerge_sort, puis démontrer qu'elle    *)
(* est correcte, c'est-à-dire :                              *)
Fixpoint imerge_sort (n:nat) (ll:listlist) {struct n} : list := ...

Theorem imerge_sort_correct : forall (ll : listlist),
   sorted_lists ll -> sorted (imerge_sort ll)

(* Écrire la fonction                                         *)
(* singletons : list-> listlist                               *)
(* qui construit la liste de listes à un élément contenant    *)
(* tous les éléments de l'argument, et démontrer le théorème :*)

Fixpoint singletons (l:list) : listlist := ...

Theorem singletons_sorted : forall l, sorted_lists (singletons l).

(* Enfin conclure en construisant une fonction de type  *)
(*        merge_sort_2 : list -> list                   *)
(* et démontrer le théorème suivant :                   *)

Theorem merge_sort_2_correct : forall l, sorted (merge_sort_2 l).
Proof.
Qed.