fail to show termination of mergeSort

Stream: Is there code for X?

[Asei Inoue]

variable {α : Type}
variable (le : α → α → Prop) [DecidableRel le]

local infixl:50 " ≼ " => le

def merge (xs ys : Array α) : Array α := Id.run do
  let mut i := 0
  let mut j := 0
  let mut result := Array.empty
  while h : i < xs.size && j < ys.size do
    have : i < xs.size := by grind
    have : j < ys.size := by grind
    if xs[i] ≼ ys[j] then
      result := result.push xs[i]
      i := i + 1
    else
      result := result.push ys[j]
      j := j + 1
  return result ++ xs.extract (start := i) ++ ys.extract (start := j)

#guard merge (fun x y : Nat => x ≤ y) #[] #[] = #[]
#guard merge (fun x y : Nat => x ≤ y) #[1, 2] #[] = #[1, 2]
#guard merge (fun x y : Nat => x ≤ y) #[] #[1, 2] = #[1, 2]
#guard merge (fun x y : Nat => x ≤ y) #[3, 4, 5] #[1, 2] = #[1, 2, 3, 4, 5]

def mergeSort (xs : Array α) : Array α := Id.run do
  if h : xs.size ≤ 1 then
    return xs
  else
    let mid := xs.size / 2
    have left_lem : (xs.extract 0 mid).size < xs.size := calc
      _ = mid - 0 := by apply Array.size_extract_of_le (as := xs) (h := by grind)
      _ = xs.size / 2 := by simp [mid]
      _ < xs.size := by grind
    /- failed to prove termination, possible solutions:
      - Use `have`-expressions to prove the remaining goals
      - Use `termination_by` to specify a different well-founded relation
      - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
      α : Type
      xs : Array α
      h : ¬xs.size ≤ 1
      mid : Nat := xs.size / 2
      left_lem : (xs.extract 0 mid).size < xs.size
      ⊢ sizeOf (xs.extract 0 (xs.size / 2)) < sizeOf xs -/
    let left := mergeSort <| xs.extract (start := 0) (stop := mid)
    let right := mergeSort <| xs.extract (start := mid) (stop := xs.size)

    return merge le left right
termination_by xs

[Asei Inoue]

how to show this? I think sizeOf xs = xs.size, but is this wrong?

[Weiyi Wang]

Just by specifying termination_by xs.size it passes

[Asei Inoue]

@Weiyi Wang Thank you!

[Violeta Hernández]

FYI, docs#List.sort is a version of merge-sort for lists.

[Robin Arnez]

you probably meant docs#List.mergeSort