why Std.range has field step_pos?

Stream: lean4

[Asei Inoue]

this code does not work.

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

this is because Std.range has step_pos field.

structure Range where
  start : Nat := 0
  stop  : Nat
  step  : Nat := 1
  step_pos : 0 < step

I think we need a special notation that does not give a proof for step_pos to make the notation [start : end : step] more convenient to use.

[Mario Carneiro]

you need a proof that p is positive or else the for loop won't terminate

[Asei Inoue]

I want a syntax for Std.range that does not require a proof to be given.

[Mario Carneiro]

what would it do?

[Mario Carneiro]

the syntax doesn't require a fourth argument

[Mario Carneiro]

as you can see, you only wrote 3 things

[Mario Carneiro]

you are getting an error because the automatic proof method failed, because you don't have things in the context to help lean prove that p is positive

[Mario Carneiro]

p comes from another range earlier; so I think if you do for _h : p in [2 : n + 1] do then omega will be able to prove the later side condition

[Asei Inoue]

Is it appropriate to fill in the proof part with decide? Wouldn't a stronger tactic be better, and wouldn't decide only accept concrete numbers?

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 })

[Asei Inoue]

p comes from another range earlier; so I think if you do for _h : p in [2 : n + 1] do then omega will be able to prove the later side condition

I don't think omega can be used because decide fills up automatically.

[Mario Carneiro]

you're right, I was hoping it would use get_elem_tactic or similar

[Mario Carneiro]

it seems there is no alternative to just writing the range constructor manually :(

[Asei Inoue]

I think this should be an issue on Lean 4.

[Asei Inoue]

@Mario Carneiro done!

https://github.com/leanprover/lean4/issues/7833