Démontrer, par l'invariant, que le tri par insertion est stable, puis…

L'invariant renforcé. Au lieu de « t[0..i-1] est trié », on énonce : avant le tour $i$, t[0..i-1] est trié, et deux éléments de même clé y apparaissent dans leur ordre d'arrivée initial.

Initialisation. Un seul élément : rien à ordonner, vrai.

Conservation. La boucle interne décale les éléments strictement supérieurs à x — c'est le >, et c'est tout le point. Un élément de clé égale à celle de x ne passe donc pas le test : la boucle s'arrête, et x est déposé après lui. Comme x arrive d'un indice plus grand, il est bien plus récent : l'ordre d'arrivée est respecté. Quant aux éléments décalés, ils glissent tous d'un cran sans se croiser, donc leur ordre relatif est intact.

Terminaison. À la sortie, la propriété porte sur le tableau entier : c'est la stabilité.

La vérification. On trie des couples (clé, rang d'arrivée) sur la seule clé, et l'on compare à sorted, qui est stable :

t = [(random.randint(0, 3), i) for i in range(n)]
c = list(t)
tri_insertion_cle(c)
assert c == sorted(t, key=lambda p: p[0])

$3000$ tirages passent.

Le contraste avec le tri par sélection est instructif : là-bas, la stabilité s'achetait avec des écritures supplémentaires ; ici elle est gratuite, et elle tient à un seul caractère — le > plutôt que >= de l'exercice de TD. Un tri stable et un tri instable peuvent différer d'un signe.