Probleme – Le tri par insertion, prouvé entièrement par induction structurelle

1. Les deux fonctions.

(* Insere x dans l. Precondition : l est triee par ordre croissant.
   Postcondition : le resultat est trie et est une permutation de x :: l. *)
let rec insere x = function
  | [] -> [x]
  | y :: r -> if x <= y then x :: y :: r else y :: insere x r

(* Renvoie une permutation triee de l. Precondition : aucune. *)
let rec tri = function
  | [] -> []
  | x :: r -> insere x (tri r)

Les prédicats de la spécification s'écrivent eux aussi par induction, et c'est ce qui rend les preuves mécaniques :

let rec trie = function
  | [] | [_] -> true
  | x :: (y :: _ as r) -> x <= y && trie r

2. Les deux propriétés de insere, par induction structurelle sur $\ell$.

Terminaison. L'appel récursif porte sur $r$, argument du constructeur :: : l'ordre induit décroît, il est bien fondé, la fonction termine. Aucun entier n'a été invoqué — c'est tout l'apport du chapitre.

(a) Le résultat est trié. Cas $\ell =\text{[]}$ : $[x]$ est triée. Cas $\ell =y::r$, avec $\ell$ triée — donc $r$ triée et $y$ minorant de $r$.

• Si $x\le y$ : le résultat est $x::y::r$. Il est trié car $x\le y$ et $y::r$ l'était.
• Sinon $x>y$, et le résultat est $y::\text{insere}(x,r)$. Par hypothèse d'induction, $\text{insere}(x,r)$ est triée. Reste à voir que $y$ minore sa tête : cette tête est soit $x$, et $y<x$ ; soit la tête de $r$, que $y$ minore par hypothèse. C'est le seul point qui demande à réfléchir, et c'est celui qu'une preuve pressée saute.

(b) C'est une permutation de $x::\ell$. Cas $\ell =\text{[]}$ : immédiat. Cas $y::r$ : ou bien le résultat est $x::y::r$, ou bien $y::\text{insere}(x,r)$, qui contient $y$ et — par hypothèse d'induction — les éléments de $x::r$. Les multiplicités sont préservées dans les deux branches.

3. Correction de tri, par induction structurelle sur $\ell$.

Cas $\text{[]}$ : la liste vide est triée et est sa propre permutation.

Cas $x::r$ : par hypothèse d'induction, $\text{tri}(r)$ est triée et permute $r$. Par la propriété (a), $\text{insere}(x,\text{tri}(r))$ est triée ; par (b), elle permute $x::\text{tri}(r)$, qui permute $x::r$. La composition de deux permutations en est une.

Deux cas de preuve, deux motifs de filtrage : la démonstration a exactement la forme du code. C'est ce que le cours annonçait, et c'est ici littéral.

Vérification mesurée : sur $5000$ listes tirées au hasard, de longueur jusqu'à $30$ et à valeurs dans $\{0,\dots ,19\}$ — donc avec des doublons, le cas où un tri fautif se trahit — le résultat est trié et permutation de l'entrée à chaque fois.

4. Le nombre de comparaisons, compté.

Le meilleur cas est $n-1$, le pire est $n(n-1)/2$, et les mesures collent exactement.

Pourquoi, et attention au sens. tri trie d'abord la queue, puis insère la tête. Sur une liste croissante, chaque élément inséré est plus petit que tout ce qui a déjà été trié : il s'arrête à la première comparaison, d'où $n-1$ au total. Sur une liste décroissante, chaque élément est plus grand que tous les autres et traverse toute la liste triée : $0+1+\cdots +(n-1)=n(n-1)/2$.

Le fait à retenir, contre-intuitif : c'est la liste déjà triée qui est le meilleur cas, et la liste à l'envers le pire — l'inverse de ce que produirait la version qui insère dans le résultat construit de gauche à droite. Le coût dépend de l'écriture, pas seulement de l'algorithme, et il se mesure.

Complexité en mémoire. La récursion n'est pas terminale : la pile atteint la profondeur $n$. Sur une liste de $10^6$ éléments, cela dépasse la limite mesurée au chapitre chap:memoire. Le tri par insertion sur listes est donc un excellent objet de preuve et un mauvais outil de production — le chapitre chap:diviser en donnera un qui est les deux.