feat(slim_check): sampleable instance for generating functions and in…

…jective functions (#3967)

This also adds `printable_prop` to trace why propositions hold or don't hold and `sampleable_ext` to allow the data structure generated and shrunken by `slim_check` to have a different type from the type we are looking for.

src/control/uliftable.lean

@@ -58,7 +58,7 @@ def down {f : Type u₀ → Type u₁} {g : Type (max u₀ v₀) → Type v₁}
 (uliftable.congr f g equiv.ulift.symm).inv_fun
 
 /-- convenient shortcut to avoid manipulating `ulift` -/
-def adapt_up {F : Type u₀ → Type u₁} {G : Type (max u₀ v₀) → Type v₁}
+def adapt_up (F : Type v₀ → Type v₁) (G : Type (max v₀ u₀) → Type u₁)
   [uliftable F G] [monad G] {α β}
   (x : F α) (f : α → G β) : G β :=
 up x >>= f ∘ ulift.down

src/data/list/perm.lean

@@ -902,6 +902,7 @@ begin
   { refine (IH₁ H).trans (IH₂ ((p₁.pairwise_iff _).1 H)),
     exact λ a b h h₁ h₂, h h₂ h₁ }
 end
+
 lemma perm.take_inter {α} [decidable_eq α] {xs ys : list α} (n : ℕ)
   (h : xs ~ ys) (h' : ys.nodup) :
   xs.take n ~ ys.inter (xs.take n) :=

src/system/random/basic.lean

@@ -83,11 +83,9 @@ class bounded_random (α : Type u) [preorder α] :=
               (x ≤ y) → rand_g g (x .. y))
 
 /-- `random α` gives us machinery to generate values of type `α` -/
-class random (α : Type u) [preorder α] extends bounded_random α :=
+class random (α : Type u) :=
 (random [] : Π (g : Type) [random_gen g], rand_g g α)
 
-attribute [instance, priority 100] random.to_bounded_random
-
 /-- shift_31_left = 2^31; multiplying by it shifts the binary
 representation of a number left by 31 bits, dividing by it shifts it
 right by 31 bits -/
@@ -107,7 +105,7 @@ def split : rand_g g g := ⟨ prod.map id up ∘ random_gen.split ∘ down ⟩
 variables {g}
 
 section random
-variables [preorder α] [random α]
+variables [random α]
 
 export random (random)
 
@@ -157,7 +155,7 @@ def run_rand_with (seed : ℕ) (cmd : _root_.rand α) : io α :=
 return $ (cmd.run ⟨mk_std_gen seed⟩).1
 
 section random
-variables [preorder α] [random α]
+variables [random α]
 
 /-- randomly generate a value of type α -/
 def random : io α :=
@@ -213,7 +211,7 @@ end bounded_random
 
 section random
 
-variables [preorder α] [random α]
+variables [random α]
 
 /-- randomly generate a value of type α -/
 meta def random : tactic α :=
@@ -250,9 +248,23 @@ instance nat_bounded_random : bounded_random ℕ :=
      pure ⟨z.val + x, nat.le_add_left _ _,
        by rw ← nat.le_sub_right_iff_add_le hxy; apply le_of_succ_le_succ z.is_lt⟩ }
 
+/-- This `bounded_random` interval generates integers between `x` and
+`y` by first generating a natural number between `0` and `y - x` and
+shifting the result appropriately. -/
+instance int_bounded_random : bounded_random ℤ :=
+{ random_r := λ g inst x y hxy,
+  do ⟨z,h₀,h₁⟩ ← @bounded_random.random_r ℕ _ _ g inst 0 (int.nat_abs $ y - x) dec_trivial,
+     pure ⟨z + x,
+       int.le_add_of_nonneg_left (int.coe_nat_nonneg _),
+       int.add_le_of_le_sub_right $ le_trans
+         (int.coe_nat_le_coe_nat_of_le h₁)
+         (le_of_eq $ int.of_nat_nat_abs_eq_of_nonneg (int.sub_nonneg_of_le hxy)) ⟩ }
+
 instance fin_random (n : ℕ) [fact (0 < n)] : random (fin n) :=
-{ random := λ g inst, @fin.random g inst _ _,
-  random_r := λ g inst (x y : fin n) p,
+{ random := λ g inst, @fin.random g inst _ _ }
+
+instance fin_bounded_random (n : ℕ) : bounded_random (fin n) :=
+{ random_r := λ g inst (x y : fin n) p,
     do ⟨r, h, h'⟩ ← @rand.random_r ℕ g inst _ _ x.val y.val p,
        pure ⟨⟨r,lt_of_le_of_lt h' y.is_lt⟩, h, h'⟩ }
 
@@ -272,8 +284,10 @@ begin
 end
 
 instance : random bool :=
-{ random   := λ g inst, (bool.of_nat ∘ subtype.val) <$> @bounded_random.random_r ℕ _ _ g inst 0 1 (nat.zero_le _),
-  random_r := λ g _inst x y p, subtype.map bool.of_nat (bool_of_nat_mem_Icc_of_mem_Icc_to_nat x y) <$> @bounded_random.random_r ℕ _ _ g _inst x.to_nat y.to_nat (bool.to_nat_le_to_nat p) }
+{ random   := λ g inst, (bool.of_nat ∘ subtype.val) <$> @bounded_random.random_r ℕ _ _ g inst 0 1 (nat.zero_le _) }
+
+instance : bounded_random bool :=
+{ random_r := λ g _inst x y p, subtype.map bool.of_nat (bool_of_nat_mem_Icc_of_mem_Icc_to_nat x y) <$> @bounded_random.random_r ℕ _ _ g _inst x.to_nat y.to_nat (bool.to_nat_le_to_nat p) }
 
 open_locale fin_fact
 
@@ -295,5 +309,7 @@ subtype.map bitvec.of_fin h' <$> rand.random_r x.to_fin y.to_fin (bitvec.to_fin_
 open nat
 
 instance random_bitvec (n : ℕ) : random (bitvec n) :=
-{ random := λ _ inst, @bitvec.random _ inst n,
-  random_r := λ _ inst x y p, @bitvec.random_r _ inst _ _ _ p }
+{ random := λ _ inst, @bitvec.random _ inst n }
+
+instance bounded_random_bitvec (n : ℕ) : bounded_random (bitvec n) :=
+{ random_r := λ _ inst x y p, @bitvec.random_r _ inst _ _ _ p }

src/tactic/slim_check.lean

@@ -5,6 +5,8 @@ Author: Simon Hudon
 -/
 
 import testing.slim_check.testable
+import testing.slim_check.functions
+import data.list.sort
 
 /-!
 ## Finding counterexamples automatically using `slim_check`
@@ -102,7 +104,10 @@ open tactic slim_check
 
 declare_trace slim_check.instance
 declare_trace slim_check.decoration
-declare_trace slim_check.discared
+declare_trace slim_check.discarded
+declare_trace slim_check.success
+declare_trace slim_check.shrink.steps
+declare_trace slim_check.shrink.candidates .
 open expr
 
 /-- Tree structure representing a `testable` instance. -/
@@ -179,12 +184,19 @@ Optional arguments given with `slim_check_cfg`
 Options:
   * `set_option trace.slim_check.decoration true`: print the proposition with quantifier annotations
   * `set_option trace.slim_check.discarded true`: print the examples discarded because they do not satisfy assumptions
+  * `set_option trace.slim_check.shrink.steps true`: trace the shrinking of counter-example
+  * `set_option trace.slim_check.shrink.candidates true`: print the lists of candidates considered when shrinking each variable
   * `set_option trace.slim_check.instance true`: print the instances of `testable` being used to test the proposition
+  * `set_option trace.slim_check.success true`: print the tested samples that satisfy a property
 -/
 meta def slim_check (cfg : slim_check_cfg := {}) : tactic unit := do
 { tgt ← retrieve $ tactic.revert_all >> target,
   let tgt' := tactic.add_decorations tgt,
-  let cfg := { cfg with enable_tracing := cfg.enable_tracing || is_trace_enabled_for `slim_check.discared },
+  let cfg := { cfg with
+               trace_discarded         := cfg.trace_discarded         || is_trace_enabled_for `slim_check.discarded,
+               trace_shrink            := cfg.trace_shrink            || is_trace_enabled_for `slim_check.shrink.steps,
+               trace_shrink_candidates := cfg.trace_shrink_candidates || is_trace_enabled_for `slim_check.shrink.candidates,
+               trace_success           := cfg.trace_success           || is_trace_enabled_for `slim_check.success },
   inst ← mk_app ``testable [tgt'] >>= mk_instance <|>
     fail!"Failed to create a `testable` instance for `{tgt}`.
 What to do: