fix: fix bug in Random.randFin. (#11587)

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Bug.20in.20randFin/near/428340514

Mathlib/Control/Random.lean

@@ -95,7 +95,7 @@ def randBound (α : Type u)
   (BoundedRandom.randomR lo hi h : RandGT g _ _)
 
 def randFin {n : Nat} [RandomGen g] : RandGT g m (Fin n.succ) :=
-  fun ⟨g⟩ ↦ pure <| randNat g 0 n.succ |>.map Fin.ofNat ULift.up
+  fun ⟨g⟩ ↦ pure <| randNat g 0 n |>.map Fin.ofNat ULift.up
 
 instance {n : Nat} : Random m (Fin n.succ) where
   random := randFin

test/random.lean

@@ -6,7 +6,7 @@ open Random
 section Rand
 
 /--
-info: 44
+info: 33
 -/
 #guard_msgs in
 #eval do
@@ -17,7 +17,7 @@ info: 44
 
 -- using higher universes
 /--
-info: ULift.up 17
+info: ULift.up 19
 -/
 #guard_msgs in
 #eval do
@@ -31,9 +31,9 @@ end Rand
 section RandT
 
 /--
-info: Got 15
-Got 29
-44
+info: Got 6
+Got 27
+33
 -/
 #guard_msgs in
 #eval show IO _ from do
@@ -45,9 +45,9 @@ Got 29
     return i.1 + j.1)
 
 /--
-info: Got 15
-Got 29
-44
+info: Got 6
+Got 27
+33
 -/
 #guard_msgs in
 #eval show Lean.Meta.MetaM _ from do
@@ -74,4 +74,46 @@ Got 4
     IO.println s!"Got {i}"
     return i.1 + j.1)
 
+/--
+info: GOOD
+-/
+#guard_msgs in
+#eval show IO _ from do
+  IO.runRandWith 257 <| do
+    let mut count := 0
+    for _ in [:10000] do
+      if (← randFin (n := 2)) == 1 then count := count + 1
+    if Float.abs (0.333 - (count / Nat.toFloat 10000)) < 0.01 then
+      IO.println "GOOD"
+    else
+      IO.println "BAD"
+
+/--
+info: GOOD
+-/
+#guard_msgs in
+#eval show IO _ from do
+  IO.runRandWith 257 <| do
+    let mut count := 0
+    for _ in [:10000] do
+      if (← randFin (n := 1)) == 0 then count := count + 1
+    if Float.abs (0.5 - (count / Nat.toFloat 10000)) < 0.01 then
+      IO.println "GOOD"
+    else
+      IO.println "BAD"
+
+/--
+info: GOOD
+-/
+#guard_msgs in
+#eval show IO _ from do
+  IO.runRandWith 257 <| do
+    let mut count := 0
+    for _ in [:10000] do
+      if (← randFin (n := 9)) == 5 then count := count + 1
+    if Float.abs (0.1 - (count / Nat.toFloat 10000)) < 0.01 then
+      IO.println "GOOD"
+    else
+      IO.println "BAD"
+
 end RandT

test/slim_check.lean

@@ -7,7 +7,7 @@ import Mathlib.Tactic.Have
 private axiom test_sorry : ∀ {α}, α
 
 /--
-warning: Gave up 91 times
+warning: Gave up 90 times
 ---
 warning: declaration uses 'sorry'
 -/
@@ -50,9 +50,9 @@ example : true := by
     success_if_fail_with_msg "
 ===================
 Found problems!
-x := 116
+x := 104
 guard: ⋯
-issue: 116 < 100 does not hold
+issue: 104 < 100 does not hold
 (0 shrinks)
 -------------------
 "
@@ -84,9 +84,9 @@ example (x : ℕ) (_h : 2 ∣ x) : true := by
     "
 ===================
 Found problems!
-x := 116
+x := 104
 guard: ⋯
-issue: 116 < 100 does not hold
+issue: 104 < 100 does not hold
 (0 shrinks)
 -------------------
 "
@@ -101,10 +101,10 @@ example (α : Type) (xs ys : List α) : true := by
 ===================
 Found problems!
 α := \"ℤ\"
-xs := [0]
-ys := [1]
-issue: [0, 1] = [1, 0] does not hold
-(4 shrinks)
+xs := [0, 0]
+ys := [-1]
+issue: [0, 0, -1] = [-1, 0, 0] does not hold
+(2 shrinks)
 -------------------
 "
       slim_check (config := { randomSeed := some 257 })
@@ -158,11 +158,11 @@ example (f : ℤ → ℤ) (_h : Injective f) (g : ℤ → ℤ) (_h : Injective g
 Found problems!
 f := [x ↦ x]
 guard: ⋯ (by construction)
-g := [-2 ↦ 0, 0 ↦ -2, x ↦ x]
+g := [0 ↦ 0, 1 ↦ 3, 2 ↦ 1, 3 ↦ 2, x ↦ x]
 guard: ⋯ (by construction)
-i := 0
-issue: 0 = -2 does not hold
-(3 shrinks)
+i := 1
+issue: 1 = 3 does not hold
+(2 shrinks)
 -------------------
 "
       slim_check (config := { randomSeed := some 257 })
@@ -175,13 +175,13 @@ example (f : ℤ → ℤ) (_h : Injective f) : true := by
     "
 ===================
 Found problems!
-f := [-1 ↦ -1, 0 ↦ 0, 1 ↦ 7, 2 ↦ 2, 3 ↦ 1, 4 ↦ 3, 5 ↦ 5, 6 ↦ 6, 7 ↦ 8, 8 ↦ 4, x ↦ x]
+f := [-2 ↦ 8, -3 ↦ -5, -5 ↦ -3, 8 ↦ -2, x ↦ x]
 guard: ⋯ (by construction)
-x := 1
-y := 3
+x := -2
+y := 0
 guard: ⋯
-issue: 7 ≤ 1 does not hold
-(4 shrinks)
+issue: 8 ≤ 0 does not hold
+(7 shrinks)
 -------------------
 "
       slim_check (config := { randomSeed := some 257 })
@@ -199,7 +199,7 @@ x := 0
 y := 1
 guard: 0 = 0
 issue: 0 = 1 does not hold
-(3 shrinks)
+(5 shrinks)
 -------------------
 "
       slim_check (config := { randomSeed := some 257 })
@@ -212,12 +212,12 @@ example (f : ℤ → ℤ) : true := by
     "
 ===================
 Found problems!
-f := [-3 ↦ 0, -4 ↦ -1, 4 ↦ 3, _ ↦ -2]
-x := -4
-y := 1
+f := [-2 ↦ 5, -4 ↦ 1, _ ↦ -1]
+x := -2
+y := 0
 guard: ⋯
-issue: -1 ≤ -2 does not hold
-(2 shrinks)
+issue: 5 ≤ -1 does not hold
+(5 shrinks)
 -------------------
 "
       slim_check (config := { randomSeed := some 257 })
@@ -231,14 +231,14 @@ example (xs ys : List ℤ) (_h : xs ~ ys) : true := by
     "
 ===================
 Found problems!
-xs := [-2, -1]
-ys := [-1, -2]
+xs := [0, -2]
+ys := [-2, 0]
 guard: ⋯
-issue: #[-2, -1] = #[-1, -2] does not hold
+issue: #[0, -2] = #[-2, 0] does not hold
 (0 shrinks)
 -------------------
 "
-      slim_check (config := { randomSeed := some 257, maxSize := 3, numRetries := 1 })
+      slim_check (config := { randomSeed := some 257, maxSize := 3, numRetries := 2 })
     exact test_sorry
   trivial
 
@@ -248,10 +248,10 @@ example (x y : ℕ) : true := by
     "
 ===================
 Found problems!
-x := 68
-y := 34
-guard: 34 ≤ 68
-issue: 102 < 100 does not hold
+x := 61
+y := 52
+guard: 52 ≤ 61
+issue: 113 < 100 does not hold
 (0 shrinks)
 -------------------
 "
@@ -281,10 +281,10 @@ example (x y : ℤ) : true := by
     "
 ===================
 Found problems!
-x := 73
-y := 73
-guard: 73 ≤ 73
-issue: 146 < 100 does not hold
+x := 55
+y := 51
+guard: 51 ≤ 55
+issue: 106 < 100 does not hold
 (0 shrinks)
 -------------------
 "
@@ -298,9 +298,9 @@ example (x y : Prop) : true := by
     "
 ===================
 Found problems!
-x := true
-y := false
-guard: true ∨ false
+x := false
+y := true
+guard: false ∨ true
 issue: false does not hold
 (0 shrinks)
 -------------------
@@ -315,9 +315,9 @@ example (x y : Prop) : true := by
     "
 ===================
 Found problems!
-x := true
-y := false
-guard: ¬true ↔ false
+x := false
+y := true
+guard: ¬false ↔ true
 issue: false does not hold
 (0 shrinks)
 -------------------
@@ -369,8 +369,8 @@ example (x y : Prop) : true := by
     "
 ===================
 Found problems!
-x := true
-y := false
+x := false
+y := true
 issue: false does not hold
 issue: true ≠ true does not hold
 (0 shrinks)
@@ -389,9 +389,9 @@ example (f : ℕ →₀ ℕ) : true := by
     "
 ===================
 Found problems!
-f := [2 ↦ 1, _ ↦ 0]
+f := [1 ↦ 1, _ ↦ 0]
 issue: ⋯ does not hold
-(3 shrinks)
+(1 shrinks)
 -------------------
 "
       slim_check (config := { randomSeed := some 257 })
@@ -404,9 +404,9 @@ example (f : Π₀ _n : ℕ, ℕ) : true := by
     "
 ===================
 Found problems!
-f := [2 ↦ 1, _ ↦ 0]
+f := [1 ↦ 1, _ ↦ 0]
 issue: ⋯ does not hold
-(3 shrinks)
+(1 shrinks)
 -------------------
 "
       slim_check (config := { randomSeed := some 257 })