feat(slim_check): add test cases (#4100)

src/system/random/basic.lean

@@ -147,11 +147,15 @@ return $ mk_std_gen seed
 
 variables {α : Type}
 
-/-- run `cmd` using a randomly seeded random number generator -/
+/-- Run `cmd` using a randomly seeded random number generator -/
 def run_rand (cmd : _root_.rand α) : io α :=
 do g ← io.mk_generator,
    return $ (cmd.run ⟨g⟩).1
 
+/-- Run `cmd` using the provided seed. -/
+def run_rand_with (seed : ℕ) (cmd : _root_.rand α) : io α :=
+return $ (cmd.run ⟨mk_std_gen seed⟩).1
+
 section random
 variables [preorder α] [random α]
 

src/tactic/slim_check.lean

@@ -205,8 +205,8 @@ set_option trace.class_instances true
   when_tracing `slim_check.instance   $ do
   { inst ← summarize_instance inst >>= pp,
     trace!"\n[testable instance]{format.indent inst 2}" },
-  code ← eval_expr (io bool) e,
-  b ← unsafe_run_io code,
-  if b then admit else failed }
+  code ← eval_expr (io punit) e,
+  unsafe_run_io code,
+  admit }
 
 end tactic.interactive

src/testing/slim_check/testable.lean

@@ -503,9 +503,12 @@ variable [testable p]
 /-- configuration for testing a property -/
 @[derive [has_reflect, inhabited]]
 structure slim_check_cfg :=
-(num_inst : ℕ := 100) -- number of examples
-(max_size : ℕ := 100) -- final size argument
-(enable_tracing : bool := ff) -- enable the printing out of discarded samples
+(num_inst : ℕ := 100)            -- number of examples
+(max_size : ℕ := 100)            -- final size argument
+(enable_tracing : bool := ff)    -- enable the printing out of discarded samples
+(random_seed : option ℕ := none) -- specify a seed to the random number generator to
+                                 -- obtain a deterministic behavior
+(quiet : bool := ff)             -- suppress success message when running `slim_check`
 
 /-- Try `n` times to find a counter-example for `p`. -/
 def testable.run_suite_aux (cfg : slim_check_cfg) : test_result p → ℕ → rand (test_result p)
@@ -526,7 +529,10 @@ testable.run_suite_aux p cfg (success $ psum.inl ()) cfg.num_inst
 
 /-- Run a test suite for `p` in `io`. -/
 def testable.check' (cfg : slim_check_cfg := {}) : io (test_result p) :=
-io.run_rand (testable.run_suite p cfg)
+match cfg.random_seed with
+| some seed := io.run_rand_with seed (testable.run_suite p cfg)
+| none := io.run_rand (testable.run_suite p cfg)
+end
 
 namespace tactic
 
@@ -592,18 +598,23 @@ exact $ add_decorations p
 end tactic
 
 /-- Run a test suite for `p` and return true or false: should we believe that `p` holds? -/
-def testable.check (p : Prop) (cfg : slim_check_cfg := {}) (p' : tactic.decorations_of p . tactic.mk_decorations) [testable p'] : io bool := do
-x ← io.run_rand (testable.run_suite p' cfg),
+def testable.check (p : Prop) (cfg : slim_check_cfg := {}) (p' : tactic.decorations_of p . tactic.mk_decorations) [testable p'] : io punit := do
+x ← match cfg.random_seed with
+    | some seed := io.run_rand_with seed (testable.run_suite p' cfg)
+    | none := io.run_rand (testable.run_suite p' cfg)
+    end,
 match x with
-| (success _) := io.put_str_ln ("Success") >> return tt
-| (gave_up n) := io.put_str_ln ("Gave up " ++ repr n ++ " times") >> return ff
+| (success _) := when (¬ cfg.quiet) $ io.put_str_ln "Success"
+| (gave_up n) := io.fail sformat!"Gave up {repr n} times"
 | (failure _ xs) := do
-   io.put_str_ln "\n===================",
-   io.put_str_ln "Found problems!",
-   io.put_str_ln "",
-   list.mmap' io.put_str_ln xs,
-   io.put_str_ln "-------------------",
-   return ff
+   let counter_ex := string.intercalate "\n" xs,
+   io.fail sformat!"
+===================
+Found problems!
+
+{counter_ex}
+-------------------
+"
 end
 
 end io

test/random.lean

@@ -0,0 +1,65 @@
+import system.random.basic
+import data.nat.prime
+import data.zmod.basic
+
+/-- fermat's primality test -/
+def primality_test (p : ℕ) (h : fact (0 < p)) : rand bool :=
+if h : 2 ≤ p-1 then do
+  n ← rand.random_r 2 (p-1) h,
+  return $ (n : zmod p)^(p-1) = 1 -- we do arithmetic with `zmod n` so that modulo and multiplication are interleaved
+else return (p = 2)
+
+/-- `iterated_primality_test_aux p h n` generating `n` candidate witnesses that `p` is a
+composite number and concludes that `p` is prime if none of them is a valid witness  -/
+def iterated_primality_test_aux (p : ℕ) (h : fact (0 < p)) : ℕ → rand bool
+| 0 := pure tt
+| (n+1) := do
+  b ← primality_test p h,
+  if b
+    then iterated_primality_test_aux n
+    else pure ff
+
+def iterated_primality_test (p : ℕ) : rand bool :=
+if h : 0 < p
+  then iterated_primality_test_aux p h 10
+  else pure ff
+
+/-- `find_prime_aux p h n` generates a candidate prime number, tests
+it as well as the 19 odd numbers following it. If none of them is
+(probably) prime, try again `n-1` times. -/
+def find_prime_aux (p : ℕ) (h : 1 ≤ p / 2) : ℕ → rand (option ℕ)
+| 0 := pure none
+| (n+1) := do
+  k ← rand.random_r 1 (p / 2) h,
+  let xs := (list.range' k 20).map (λ i, 2*i+1),
+  some r ← option_t.run $ xs.mfirst (λ n, option_t.mk $ mcond (iterated_primality_test n) (pure (some n)) (pure none))
+    | find_prime_aux n,
+  pure r
+
+def find_prime (p : ℕ) : rand (option ℕ) :=
+if h : 1 ≤ p / 2 then
+  find_prime_aux p h 20
+else pure none
+
+open tactic
+
+/- `ps` should be `[97, 101, 103, 107, 109, 113]` but
+it uses a pseudo primality test and some composite numbers
+also sneak in -/
+run_cmd do
+  let xs := list.range' 90 30,
+  ps ← tactic.run_rand (xs.mfilter iterated_primality_test),
+  when (ps ≠ [97, 101, 103, 107, 109, 113])
+    (trace!"The random primality test also included some composite numbers: {ps}")
+
+/- `ps` should be `[97, 101, 103, 107, 109, 113]`. This
+test is deterministic because we pick the random seed -/
+run_cmd do
+  let xs := list.range' 90 30,
+  let ps : list ℕ := (xs.mfilter iterated_primality_test).eval ⟨ mk_std_gen 10 ⟩,
+  guard (ps = [97, 101, 103, 107, 109, 113]) <|> fail "wrong list of prime numbers"
+
+/- this finds a random probably-prime number -/
+run_cmd do
+  some p ← tactic.run_rand (find_prime 100000) | trace "no prime found, gave up",
+  when (¬ nat.prime p) (trace!"The number {p} fooled Fermat's test")

test/slim_check.lean

@@ -1,66 +1,96 @@
 
-import system.random.basic
-import data.nat.prime
-import data.zmod.basic
+import tactic.slim_check
 
-/-- fermat's primality test -/
-def primality_test (p : ℕ) (h : fact (0 < p)) : rand bool :=
-if h : 2 ≤ p-1 then do
-  n ← rand.random_r 2 (p-1) h,
-  return $ (n : zmod p)^(p-1) = 1 -- we do arithmetic with `zmod n` so that modulo and multiplication are interleaved
-else return (p = 2)
+example : true :=
+begin
+  have : ∀ i j : ℕ, i < j → j < i,
+  success_if_fail_with_msg
+  { slim_check { random_seed := some 257 } }
+  "
+===================
+Found problems!
 
-/-- `iterated_primality_test_aux p h n` generating `n` candidate witnesses that `p` is a
-composite number and concludes that `p` is prime if none of them is a valid witness  -/
-def iterated_primality_test_aux (p : ℕ) (h : fact (0 < p)) : ℕ → rand bool
-| 0 := pure tt
-| (n+1) := do
-  b ← primality_test p h,
-  if b
-    then iterated_primality_test_aux n
-    else pure ff
+i := 0
+j := 1
+-------------------
+",
+  admit,
+  trivial
+end
 
-def iterated_primality_test (p : ℕ) : rand bool :=
-if h : 0 < p
-  then iterated_primality_test_aux p h 10
-  else pure ff
+example : true :=
+begin
+  have : (∀ x : ℕ, 2 ∣ x → x < 100),
+  success_if_fail_with_msg
+  { slim_check { random_seed := some 257 } }
+  "
+===================
+Found problems!
 
-/-- `find_prime_aux p h n` generates a candidate prime number, tests
-it as well as the 19 odd numbers following it. If none of them is
-(probably) prime, try again `n-1` times. -/
-def find_prime_aux (p : ℕ) (h : 1 ≤ p / 2) : ℕ → rand (option ℕ)
-| 0 := pure none
-| (n+1) := do
-  k ← rand.random_r 1 (p / 2) h,
-  let xs := (list.range' k 20).map (λ i, 2*i+1),
-  some r ← option_t.run $ xs.mfirst (λ n, option_t.mk $ mcond (iterated_primality_test n) (pure (some n)) (pure none))
-    | find_prime_aux n,
-  pure r
+x := 102
+-------------------
+",
+  admit,
+  trivial
+end
 
-def find_prime (p : ℕ) : rand (option ℕ) :=
-if h : 1 ≤ p / 2 then
-  find_prime_aux p h 20
-else pure none
+example (xs : list ℕ) (w : ∃ x ∈ xs, x < 3) : true :=
+begin
+  have : ∀ y ∈ xs, y < 5,
+  success_if_fail_with_msg
+  { slim_check { random_seed := some 257 } }
+"
+===================
+Found problems!
 
-open tactic
+xs := [0, 5]
+x := 0
+y := 5
+-------------------
+",
+  admit,
+  trivial
+end
 
-/- `ps` should be `[97, 101, 103, 107, 109, 113]` but
-it uses a pseudo primality test and some composite numbers
-also sneak in -/
-run_cmd do
-  let xs := list.range' 90 30,
-  ps ← tactic.run_rand (xs.mfilter iterated_primality_test),
-  when (ps ≠ [97, 101, 103, 107, 109, 113])
-    (trace!"The random primality test also included some composite numbers: {ps}")
+example (x : ℕ) (h : 2 ∣ x) : true :=
+begin
+  have : x < 100,
+  success_if_fail_with_msg
+  { slim_check { random_seed := some 257 } }
+"
+===================
+Found problems!
 
-/- `ps` should be `[97, 101, 103, 107, 109, 113]`. This
-test is deterministic because we pick the random seed -/
-run_cmd do
-  let xs := list.range' 90 30,
-  let ps : list ℕ := (xs.mfilter iterated_primality_test).eval ⟨ mk_std_gen 10 ⟩,
-  guard (ps = [97, 101, 103, 107, 109, 113]) <|> fail "wrong list of prime numbers"
+x := 102
+-------------------
+",
+  admit,
+  trivial
+end
 
-/- this finds a random probably-prime number -/
-run_cmd do
-  some p ← tactic.run_rand (find_prime 100000) | trace "no prime found, gave up",
-  when (¬ nat.prime p) (trace!"The number {p} fooled Fermat's test")
+example (α : Type) (xs ys : list α) : true :=
+begin
+  have : xs ++ ys = ys ++ xs,
+  success_if_fail_with_msg
+  { slim_check { random_seed := some 257 } }
+"
+===================
+Found problems!
+
+α := ℤ
+xs := [0]
+ys := [1]
+[0, 1] ≠ [1, 0]
+-------------------
+",
+  admit,
+  trivial
+end
+
+example : true :=
+begin
+  have : ∀ x ∈ [1,2,3], x < 4,
+  slim_check { random_seed := some 257, quiet := tt },
+    -- success
+  trivial,
+end