Sort1.lean

class Preorder (α) extends LE α where
  trans {x y z : α} : x ≤ y → y ≤ z → x ≤ z
  refl (x : α) : x ≤ x

class TotalPreorder (α) extends Preorder α where
  total (x y : α) : x ≤ y ∨ y ≤ x
  refl x := (total x x).elim id id

theorem le_of_not_le [I : TotalPreorder α] {x y : α} (h : ¬x ≤ y) : y ≤ x :=
  (I.total x y).elim (False.elim ∘ h) id

instance : TotalPreorder Nat where
  trans := Nat.le_trans
  total := Nat.le_total

inductive List.Chain (R : α → α → Prop) : α → List α → Prop
  | nil : Chain R a []
  | cons : R a b → Chain R b l → Chain R a (b :: l)

def List.Chain' (R : α → α → Prop) : List α → Prop
  | [] => True
  | a :: l => Chain R a l

inductive List.Perm : List α → List α → Prop
  | nil : Perm [] []
  | cons (x) : Perm l₁ l₂ → Perm (x :: l₁) (x :: l₂)
  | swap (x y l) : Perm (y :: x :: l) (x :: y :: l)
  | trans : Perm l₁ l₂ → Perm l₂ l₃ → Perm l₁ l₃

@[simp]
theorem List.Perm.refl : (l : List α) → Perm l l
  | [] => nil
  | x :: l => cons x (refl l)

theorem List.Perm.symm (h : Perm l₂ l₁) : Perm l₁ l₂ := by
  induction h with
  | nil => exact nil
  | cons x _ ih => exact cons x ih
  | swap x y l => exact swap y x l
  | trans _ _ ih₁ ih₂ => exact trans ih₂ ih₁

theorem List.Perm.swap' (y) (h : Perm l₁ (x :: l₂)) : Perm (y :: l₁) (x :: y :: l₂) :=
  trans (cons y h) (swap x y l₂)

theorem List.Perm.length_eq (h : Perm l₁ l₂) : length l₁ = length l₂ := by
  induction h <;> simp [*]

theorem List.Perm.middle (x : α) : ∀ l₁ l₂, Perm (l₁ ++ x :: l₂) (x :: l₁ ++ l₂)
  | [], _ => refl _
  | y :: l₁, l₂ => swap' y (middle x l₁ l₂)

theorem List.Perm.inv : Perm (l₁ ++ x :: r₁) (l₂ ++ x :: r₂) → Perm (l₁ ++ r₁) (l₂ ++ r₂) := by
  generalize h₁ : l₁ ++ x :: r₁ = s₁
  generalize h₂ : l₂ ++ x :: r₂ = s₂
  intro h
  induction h generalizing l₁ r₁ l₂ r₂ with
  | nil => sorry
  | cons y h ih =>
    cases l₁ <;> cases l₂ <;> cases h₁ <;> cases h₂
    . exact h
    . exact trans h (middle _ _ _)
    . exact trans (symm (middle _ _ _)) h
    . exact cons y (ih rfl rfl)
  | swap _ _ _ => sorry
  | trans _ _ _ _ => sorry

@[simp]
theorem List.Perm.cons_iff : Perm (x :: l₁) (x :: l₂) ↔ Perm l₁ l₂ where
  mp h := inv (l₁ := []) (l₂ := []) h
  mpr := cons x

@[simp]
theorem List.Perm.cons_iff' : Perm (y₁ :: x :: l₁) (y₂ :: x :: l₂) ↔ Perm (y₁ :: l₁) (y₂ :: l₂) where
  mp h := inv (l₁ := [y₁]) (l₂ := [y₂]) h
  mpr h := trans (trans (swap x y₁ l₁) (cons x h)) (swap y₂ x l₂)

@[simp]
theorem List.Perm.swap_iff : Perm (y :: l₁) (x :: y :: l₂) ↔ Perm l₁ (x :: l₂) where
  mp h := inv (l₁ := []) (l₂ := [x]) h
  mpr := swap' y

@[simp]
theorem List.Perm.swap_iff' : Perm (y₁ :: x :: l₁) (x :: y₂ :: l₂) ↔ Perm (y₁ :: l₁) (y₂ :: l₂) where
  mp h := inv (l₁ := [y₁]) (l₂ := []) h
  mpr h := symm (swap' x (symm h))

class ComparisonSort (f : ∀ {α} [I : LE α] [DecidableRel I.le], List α → List α) where
  perm [I : LE α] [DecidableRel I.le] (l : List α) : (f l).Perm l
  sort [I : TotalPreorder α] [DecidableRel I.le] (l : List α) : (f l).Chain' I.le

section

variable [I : LE α] [DecidableRel I.le]

def insert (x : α) : List α → List α
  | [] => [x]
  | y :: l =>
    if x ≤ y
    then x :: y :: l
    else y :: insert x l

def insertionSort : List α → List α
  | [] => []
  | x :: l => insert x (insertionSort l)

theorem perm_insert (x : α) (l) : (insert x l).Perm (x :: l) := by
  induction l <;> simp [insert]; split <;> simp [*]

end

theorem sort_insert [I : TotalPreorder α] [DecidableRel I.le] (x) (h : l.Chain' I.le) : (insert x l).Chain' I.le := by
  induction l
  case nil => exact .nil
  case cons y l ih =>
    unfold insert
    split
    case _ h' => exact .cons h' h
    case _ h' =>
      have h' := le_of_not_le h'
      dsimp [List.Chain']
      cases h
      case nil => exact .cons h' .nil
      case cons z l h₁ h₂  =>
        specialize ih h₁
        unfold insert at ih ⊢
        split
        case _ h'' =>
          simp [h''] at ih
          exact .cons h' ih
        case _ h'' =>
          simp [h''] at ih
          exact .cons h₂ ih

instance : ComparisonSort @insertionSort where
  perm l := by
    induction l with
    | nil => exact .nil
    | cons x l ih => exact .trans (perm_insert x (insertionSort l)) (.cons x ih)
  sort l := by
    induction l with
    | nil => exact trivial
    | cons x l ih => exact sort_insert x ih

section

variable [I : LE α] [DecidableRel I.le]

def select (x : α) : List α → α × List α
  | [] => (x, [])
  | y :: l =>
    if x ≤ y
    then ((select x l).1, y :: (select x l).2)
    else ((select y l).1, x :: (select y l).2)

theorem perm_select (x : α) (l) : ((select x l).1 :: (select x l).2).Perm (x :: l) := by
  induction l generalizing x <;> simp [select]; split <;> simp [*]

def selectionSort : List α → List α
  | [] => []
  | x :: l =>
    have := Nat.le_of_eq (perm_select x l).length_eq
    (select x l).1 :: selectionSort (select x l).2
termination_by _ l => l.length

end

instance : ComparisonSort @selectionSort where
  perm l := by
    generalize hn : l.length = n
    induction n generalizing l with
    | zero =>
      cases l with
      | nil => exact .nil
      | cons => cases hn
    | succ _ ih =>
      cases l with
      | nil => cases hn
      | cons x l =>
        simp [selectionSort]
        exact .trans (.cons _ (ih _ (Nat.succ.inj ((perm_select x l).length_eq.trans hn)))) (perm_select x l)
  sort l := by
    sorry

-- todo: comparison in monad, time complexity

section

variable [Monad m] (le : α → α → m Bool)

def insertM (x : α) : List α → m (List α)
  | [] => return [x]
  | y :: l =>
    return if ← le x y
      then x :: y :: l
      else y :: (← insertM x l)

def insertM' (x : α) : List α → m (List α)
  | [] => return [x]
  | y :: l => do
    if ← le x y
    then return x :: y :: l
    else return y :: (← insertM' x l)

def myLe (x y : Nat) : IO Bool := do
  IO.println s!"{x} ≤ {y}"
  return x ≤ y

#print insertM
#print insertM'

def insertionSortM : List α → List α
  | [] => []
  | x :: l => insertM ifLE x (insertionSortM l)

end

variable [I : LE α] [DecidableRel I.le]

def isLE (x y : α) (t e : List α) : List α :=
  if x ≤ y then t else e

theorem insert_eq_insertM (x : α) (l) : insert x l = insertM isLE x l := by
  unfold isLE
  induction l <;> simp [insert, insertM]
  split <;> simp [*]

theorem insertionSort_eq_insertionSortM (l : List α) : insertionSort l = insertionSortM isLE l := by
  induction l <;> simp [insertionSort, insertionSortM, insert_eq_insertM, *]