Reasonning about PRange sizes (with `Int`)

Stream: lean4

[Clément Blaudeau]

Since #10045, #10303 and 10633 we have polymorphic ranges over integers:

#eval ((0:Int)...(5:Int)).toList -- [0, 1, 2, 3, 4]
#eval ((-5:Int32)...(5:Int32)).toList -- [-5, -4, -3, -2, -1, 0, 1, 2, 3, 4]
#eval ((0:UInt32)...(5:UInt32)).toList -- [0, 1, 2, 3, 4]

I'm using such ranges in for loops, and trying to prove properties with mvcgen. The size of the range appears in the proof : (s...e).size. While it computes fine:

#eval  ((0:Int)...(5:Int)).size -- 5

and while there are instances of HasSize for Int, proving anything about them is hard. I had to do this to prove a simple statement :

theorem int_range_size (s e : Int) :
  (s...e).size = (e - s).toNat
:= by
  simp [
    Std.Rco.size,
    Id.run,
    Std.Rco.Internal.iter,
    Std.Rxo.HasSize.size,
    Std.Rxc.HasSize.size,
    Std.Iterators.Iter.size,
    Std.Iterators.Iter.toIterM,
    Std.Iterators.IteratorSize.size,
    Pure.pure,
  ]
  rw [← Int.toNat_sub']
  omega

link to playground

Am I missing something or is it to be expected ?

[Markus Himmel]

The standard library should provide these, but adding them is somewhere in the middle of the (very long) TODO list for iterators/ranges/slices. If you would like to open a PR to the lean4 repo which adds these lemmas in an analogous fashion to the Nat ones here, I would be happy to merge it.

[Clément Blaudeau]

Nice! I missed those for Nat. I'll try to find some time to open a PR on that! Thanks.

[Alexander Bentkamp]

@Markus Himmel https://github.com/leanprover/lean4/pull/11159