Bug in randFin

Stream: mathlib4

[Adam Topaz]

I think there's a bug in docs#Random.randFin (namely, it should say randNat 0 n as opposed to randNat 0 n.succ). E.g.

import Mathlib

def foo : RandT IO (Fin 2) := Random.randFin

#eval show IO Unit from do
  let mut out := 0
  let n := 10000
  for _ in [:n] do
    if (← IO.runRand foo) == 0 then out := out + 1
  println! out

-- 6615

[Adam Topaz]

Pinging @Henrik Böving who is the author on that file.

[Adam Topaz]

In general with the current implementation I think $0$ will come up more often than it should.

[Adam Topaz]

assuming one expects the uniform distribution, of course.

[Henrik Böving]

I agree yes, that's an off by one.

[Adam Topaz]

I guess the real question is whether we want randNat to be inclusive in the upper bound. What does haskell do?

[Henrik Böving]

https://hackage.haskell.org/package/random-1.2.1.2/docs/System-Random.html#g:2 bsaed on the usage here it appears that if you ask haskell for a uniform distribution 1, 6 you get upper and lower bound inclusive

[Adam Topaz]

ok, I can open a quick pr with a fix to randFin then.

[Adam Topaz]

#11587

[Adam Topaz]

@Matthew Ballard has already deligated the PR, but I did add some additional nontrivial tests. @Henrik Böving and Matt -- are you okay with these new tests?

[Henrik Böving]

I guess those are fine. They might flipper when we are really unlucky but let's just hope that doesn't happen^^

[Adam Topaz]

But an explicit seed is provided, so these tests should be deterministic

[Henrik Böving]

Ah I didn't see that while quickly reading the file, then everything is fine :thumbs_up:

[Adam Topaz]

great. I'll merge it once it passes CI

[Adam Topaz]

... it just failed CI :-/

[Adam Topaz]

oh... just because I didn't update the slim check test file!