Valider un tri

let est_permutation l1 l2 = tri_insertion l1 = tri_insertion l2

let verifie tri l =
  let r = tri l in
  est_trie r && est_permutation r l

Deux listes sont permutations l'une de l'autre si et seulement si elles donnent la même liste une fois triées (on compare alors par égalité structurelle =). verifie vérifie les deux clauses du contrat — ordonné et permutation : c'est un test de propriété, à lancer sur des entrées variées pour gagner confiance dans une fonction de tri.