Iterating ranges with PRange

Stream: lean4

[Eric Wieser]

What am I doing wrong here?

import Std

instance : Std.PRange.UpwardEnumerable UInt32 where
  succ? i := if i + 1 = 0 then none else some (i + 1)

def silly : Bool := Id.run do
  for c in (0...(0xD800 : UInt32)).iter do
    return true
  return false

def silly' : Bool := Id.run do
  for h : c in (0...(0xD800 : UInt32)).iter do
    return true
  return false

both fail to synthesize the instance needed for the for construct

[Alfredo Moreira-Rosa]

Not sure, but you may be missing an instance ? i see many in the Nat implementation :
https://github.com/leanprover/lean4/blob/master/src/Init/Data/Range/Polymorphic/Nat.lean

[Alfredo Moreira-Rosa]

The ForIn impl seems to require a ton of them :
https://github.com/leanprover/lean4/blob/master/src/Init/Data/Range/Polymorphic/Iterators.lean#L95

[Paul Reichert]

Indeed. The generality of the polymorphic ranges unfortunately requires a host of type classes. (I'm planning to write a manual entry for iterators/ranges, but it's not there yet.)

[Eric Wieser]

It looks like the version at head has changed quite a lot since the one in 4.22.0, so perhaps I should wait before trying to do this for UInt32 (for which the motivation was batteries#1344)

[Eric Wieser]

Paul Reichert said:

The generality of the polymorphic ranges unfortunately requires a host of type classes

In fairness I should have expected the for h : i in version to require a handful of lawfulness typeclasses.

[Alfredo Moreira-Rosa]

Maybe for number types we could have a common generic implementation (or at least common helpers if genericity is not possible), so that it would not require everyone to implement their own Lawfulness typeclasses ?

[Paul Reichert]

Range instances for (U)Int* are also something I certainly want to provide in the standard library. Here's the UInt part: lean4#10303

@ecyrbe What do you mean by number types -- the types from the standard library (SInt*, UInt*, Fin, Int, Nat, ...), types from Batteries/Mathlib or custom types?

[Alfredo Moreira-Rosa]

yes, the ones from standard library