import Mathlib.Data.Nat.Basic

-- variable {α : Type} [Ord a]
variable {α : Type} [LinearOrder α] [DecidableRel (· ≤ · : α → α → Prop)]

@[simp]
def insort (a : α) (as : List α) : List α :=
  match as with
  | [] => [a]
  | (y::ys) => if a ≤ y then a :: insort y ys else y :: insort a ys

@[simp]
def isort (as : List α) : List α :=
  match as with
  | [] => []
  | (x::xs) => insort x $ isort xs

def insort_is_perm
    (tail : List α) (head : α) :
    (head :: tail).Perm (insort head tail) := by
  sorry

def insertion_sort_is_perm
    (l : List α) :
    List.Perm l (isort l) := by
  sorry

theorem insort_ne_nil
    (x : α) (xs : List α) :
    insort x xs ≠ [] := by
  sorry

def isort_ne_list_is_insort_head
    (ys : List α) (y : α) :
    List.Pairwise (fun x1 x2 => x1 ≤ x2) (y :: ys) →
      y :: ys = insort y ys := by
  sorry

def mem_insort
    (a : α) (y : α) (ys : List α) :
    a ∈ insort y ys → a = y ∨ a ∈ ys := by
  sorry

def insort_is_sorted
    (head : α) (tail : List α) :
    List.Pairwise (· ≤ ·) tail →
      List.Pairwise (. ≤ .) (insort head tail) := by
  sorry

def insertion_sort_is_sorted
    (l : List α) :
    List.Pairwise (. ≤ .) (isort l) := by
  sorry

def sort_is_valid
    {α : Type}
    [LinearOrder α]
    [DecidableRel (· ≤ · : α → α → Prop)]
    (sort_fn : List α → List α) :
    Prop :=
  ∀ l : List α,
    (List.Perm l (sort_fn l)) ∧
      List.Pairwise (fun x y : α => x ≤ y) (sort_fn l)

def isort_valid :
    sort_is_valid (α := α) isort := by
  sorry