prove termination of a function defined by `let rec`

Stream: Is there code for X?

[Asei Inoue]

I'm working on Lean 99, which is lean translation of Haskell 99. This is Problem 24.

Why does the proof of termination fail while fuel trick is used? Can it be rewritten so that termination is clear without using fuel?

/-- Draw `N` different random numbers from the set `1..M`. -/
def diffSelect (count range : Nat) : IO (List Nat) :=
  if count > range then
    dbg_trace s!"can't draw {count} different numbers from 1..{range}"
    pure []
  else
    let rec loop (count : Nat) (acc : List Nat) (fuel : Nat) : IO (List Nat) := do
      match count, fuel with
      | 0, _ => pure acc
      | _, 0 =>
        dbg_trace "out of fuel!"
        pure []
      | _, _ =>
        let pick ← IO.rand 1 range
        if acc.contains pick then
          loop count acc (fuel - 1) -- failed to prove termination
        else
          loop (count - 1) (pick :: acc) (fuel - 1)
      termination_by fuel
    loop count [] 10000

[Kim Morrison]

/-- Draw `N` different random numbers from the set `1..M`. -/
def diffSelect (count range : Nat) : IO (List Nat) :=
  if count > range then
    dbg_trace s!"can't draw {count} different numbers from 1..{range}"
    pure []
  else
    let rec loop (count : Nat) (acc : List Nat) (fuel : Nat) : IO (List Nat) := do
      match count, fuel with
      | 0, _ => pure acc
      | _, 0 =>
        dbg_trace "out of fuel!"
        pure []
      | _, fuel + 1 =>
        let pick ← IO.rand 1 range
        if acc.contains pick then
          loop count acc fuel
        else
          loop (count - 1) (pick :: acc) fuel
      termination_by fuel
    loop count [] 10000

[Asei Inoue]

Thanks.