Termination of a sorting function

Stream: new members

[Sílvio Zacomelli]

Hello. As the title states, I have this sort function:

mutual
  def qsort [LE α] [DecidableEq α] [DecidableRel (@LE.le α _)] (y : List α) : List α :=
    if  h₁ : y = [] then []
    else
      let x::xs := y
      help x xs [] []
   termination_by y

  def help (x : α) (ys us vs: List α) [LE α] [DecidableEq α] [DecidableRel (@LE.le α _)] : List α:=
    if h₂ : ys = [] then
      (qsort us) ++ [x] ++ (qsort vs)
    else
      let y::xs := ys
    if h₃ : x ≤ y then
      help x xs us (y::vs)
    else
      help x xs (y::us) vs
    termination_by ys
end

As you can tell by the code, Lean fails in proving it's termination. Indeed, I had tried to prove it using the length of the lists before figuring out that (obviously) the length of y doesn't change (it's a sort function). Then, I've tried the approach of using a new parameter to track the "number of unsorted elements" of the list. This idea is shown in the code below:

mutual
  def qsort₁ [LE α] [DecidableEq α] [DecidableRel (@LE.le α _)] (n : Nat) (y : List α) : List α :=
    if h₁ : n = 0 then y else
      if  h₂ : y.length = 0 then []
      else
        let x::xs := y
        help₁ n x xs [] []
   termination_by n

  def help₁  (t : Nat) (x : α) (ys us vs: List α) [LE α] [DecidableEq α] [DecidableRel (@LE.le α _)] : List α:=
    if h₃ : t = 0 then x::ys else
    if h₄ : ys = [] then
      (qsort₁ (t - 1 - vs.length) us) ++ [x] ++ (qsort₁ (t- 1 - us.length) vs)
    else
      let y::xs := ys
    if h₅ : x ≤ y then
      help₁ t x xs us (y::vs)
    else
      help₁ t x xs (y::us) vs
    termination_by t
end

But I haven't had any luck with it either. In both cases, Lean asks me to make impossible proofs. How do I prove this termination?