The tactic to prove the `step_pos` field in `Std.range` should be stronger than `decide`

Description

Currently, using the syntax for Std.range, the step_pos field is always filled with decide tactic.

syntax:max "[" withoutPosition(":" term) "]" : term
syntax:max "[" withoutPosition(term ":" term) "]" : term
syntax:max "[" withoutPosition(":" term ":" term) "]" : term
syntax:max "[" withoutPosition(term ":" term ":" term) "]" : term

macro_rules
  | `([ : $stop]) => `({ stop := $stop, step_pos := Nat.zero_lt_one : Range })
  | `([ $start : $stop ]) => `({ start := $start, stop := $stop, step_pos := Nat.zero_lt_one : Range })
  | `([ $start : $stop : $step ]) => `({ start := $start, stop := $stop, step := $step, step_pos := by decide : Range })
  | `([ : $stop : $step ]) => `({ stop := $stop, step := $step, step_pos := by decide : Range })

Therefore, step_pos cannot be proved in the following cases

def eratosthenesAux (n : Nat) : Array Bool := Id.run do
  let mut isPrime := Array.replicate (n + 1) true

  isPrime := isPrime.set! 0 false
  isPrime := isPrime.set! 1 false

  for p in [2 : n + 1] do
    if not isPrime[p]! then
      continue

    if p ^ 2 > n then
      break

    /- expected type must not contain free variables
      0 < p
    Use the '+revert' option to automatically cleanup and revert free variables.Lean 4
    p : Nat -/
    for q in [p * p : n : p] do
      isPrime := isPrime.set! q false

  return isPrime

Versions

v4.19.0-rc2

Additional Information

see Zulip: #lean4 > why Std.range has field step_pos?

Start by locating the Std.range syntax and its macro_rules, then reproduce the eratosthenesAux example from the issue. Investigate how the step_pos proof is generated for ranges with variable steps; done means the shown nested range can elaborate without the free-variable error while preserving the existing range syntax.