Require Import List.
Import ListNotations.
Require Import Nat.
Require Import Bool.

Fixpoint insertAt {X: Type} (x: X) (n: nat) (l: list X): list X :=
match l with
| nil => if n =? 0 then [x] else nil
| h :: t => if n =? 0 then x :: h :: t else h :: (insertAt x (n-1) t)
end.

Fixpoint range (n: nat): list nat :=
match n with
| O => [0]
| S n => (range n) ++ [S n]
end.

Fixpoint permutations {X: Type} (l: list X) : list (list X) :=
match l with
| nil => [nil]
| h :: t => flat_map (fun l =>
    map (fun n => insertAt h n l) (range (length l))
  ) (permutations t)
end.

Class Ord A := {
  lt : A -> A -> bool
}.
Instance natOrd : Ord nat := { lt := Nat.ltb }.
Fixpoint listLt {X} {H: Ord X} (l1 l2: list X): bool :=
match l1, l2 with
| nil, _ => true
| _, nil => false
| (h1 :: t1), (h2 :: t2) => if @lt X H h1 h2
                            then true
                            else if @lt X H h2 h1
                            then false
                            else @listLt X H H t1 t2
end.

Instance listOrd {X} `{H: Ord X}: Ord (list X) := {
  lt := @listLt X H H
}.

Fixpoint insertSorted {X: Type} `{Ord X} (x: X) (l: list X): list X :=
match l with
| nil => [x]
| h :: t => if lt x h then x :: h :: t else h :: (insertSorted x t)
end.

Fixpoint badSort {X} `{_: Ord X} (k: nat) (l: list X): list X :=
match k with
| O => fold_right insertSorted [] l
| S n => hd nil (@badSort (list X) listOrd n (permutations l))
end.