Range with steps

Stream: lean4

[Floris van Doorn]

What is the canonical way in Lean to write

for (i = a; i < b; i += c):
  ...

This used to be

for k in [a : b : c] do
  ...

but this is now a legacy notation.
It isn't easily written with the new Std.PRange, I believe. Is the use case where c ≠ 1 deemed obscure enough that this is not supported?

[Floris van Doorn]

(side remark: is it intended that for k in (2*p)...n do requires parentheses?)

[Floris van Doorn]

I guess I could use

for i in List.range' a ((b - a - 1) / c) c do
  ...

[Sebastian Ullrich]

(/cc @Paul Reichert)

[Adam Topaz]

#eval show IO Unit from do
  for i in [1:10:4] do
    println! i

works for me with 4.27.

[Adam Topaz]

There is an issue that if c is a parameter you need to prove that c > 0, and there isn't a convenient way to do this with the [a:b:c] notation, but something like this works:

def foo (a b c : Nat) : IO Unit := do
  for i in Std.Range.mk a b (c + 1) (by grind) do
    println! i

[Robin Arnez]

Yes, it works but if you hover over [1:10:4] it says Std.Legacy.Range

[Adam Topaz]

really?

[Adam Topaz]

what version of lean?

[Robin Arnez]

Latest mathlib in live lean, i.e. 4.28.0-rc1

[Robin Arnez]

But you're right, it's a recent change

[Adam Topaz]

aha ok I'm just one version behind.

[Paul Reichert]

You can use the stepSize combinator (which is efficient no matter what the step size is):

import Std

def f (n : Nat) : IO Unit := do
  for x in (1...n).iter.stepSize 2 do
    IO.println (toString x)

#eval f 10

This is admittedly less convenient than the previous notation. Step sizes aren't integrated more deeply into the ranges to keep the complexity in check, given that there are some complications with the polymorphism of the new ranges.

[Floris van Doorn]

Adam Topaz said:

There is an issue that if c is a parameter you need to prove that c > 0, and there isn't a convenient way to do this with the [a:b:c] notation, but something like this works:

def foo (a b c : Nat) : IO Unit := do
  for i in Std.Range.mk a b (c + 1) (by grind) do
    println! i

I was indeed also running into this issue.

[Floris van Doorn]

Paul Reichert said:

You can use the stepSize combinator (which is efficient no matter what the step size is):

Oh, this is nice! docs#Std.IterM.stepSize is indeed what I was looking for. The notation is indeed less nice, but still pretty good.