diff --git a/src/data/lazy_list2.lean b/src/data/lazy_list2.lean
index 8727b52f34522..03029980b52e3 100644
--- a/src/data/lazy_list2.lean
+++ b/src/data/lazy_list2.lean
@@ -76,4 +76,29 @@ begin
     simp! with functor_norm, refl },
 end
 
+/-- `init xs`, if `xs` non-empty, drops the last element of the list.
+Otherwise, return the empty list. -/
+def init {α} : lazy_list α → lazy_list α
+| lazy_list.nil := lazy_list.nil
+| (lazy_list.cons x xs) :=
+  let xs' := xs () in
+  match xs' with
+  | lazy_list.nil := lazy_list.nil
+  | (lazy_list.cons _ _) := lazy_list.cons x (init xs')
+  end
+
+/-- `interleave xs ys` creates a list where elements of `xs` and `ys` alternate. -/
+def interleave {α} : lazy_list α → lazy_list α → lazy_list α
+| lazy_list.nil xs := xs
+| a@(lazy_list.cons x xs) lazy_list.nil := a
+| (lazy_list.cons x xs) (lazy_list.cons y ys) :=
+  lazy_list.cons x (lazy_list.cons y (interleave (xs ()) (ys ())))
+
+/-- `interleave_all (xs::ys::zs::xss)` creates a list where elements of `xs`, `ys`
+and `zs` and the rest alternate. Every other element of the resulting list is taken from
+`xs`, every fourth is taken from `ys`, every eighth is taken from `zs` and so on. -/
+def interleave_all {α} : list (lazy_list α) → lazy_list α
+| [] := lazy_list.nil
+| (x :: xs) := interleave x (interleave_all xs)
+
 end lazy_list
diff --git a/src/tactic/slim_check.lean b/src/tactic/slim_check.lean
new file mode 100644
index 0000000000000..ea968a1889127
--- /dev/null
+++ b/src/tactic/slim_check.lean
@@ -0,0 +1,197 @@
+/-
+Copyright (c) 2020 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Simon Hudon
+-/
+
+import testing.slim_check.testable
+
+/-!
+## Finding counterexamples automatically using `slim_check`
+
+A proposition can be tested by writing it out as:
+
+```lean
+example (xs : list ℕ) (w : ∃ x ∈ xs, x < 3) : ∀ y ∈ xs, y < 5 := by slim_check
+-- ===================
+-- Found problems!
+
+-- xs := [0, 5]
+-- x := 0
+-- y := 5
+-- -------------------
+
+example (x : ℕ) (h : 2 ∣ x) : x < 100 := by slim_check
+-- ===================
+-- Found problems!
+
+-- x := 258
+-- -------------------
+
+example (α : Type) (xs ys : list α) : xs ++ ys = ys ++ xs := by slim_check
+-- ===================
+-- Found problems!
+
+-- α := ℤ
+-- xs := [-4]
+-- ys := [1]
+-- -------------------
+
+example : ∀ x ∈ [1,2,3], x < 4 := by slim_check
+-- Success
+```
+
+In the first example, `slim_check` is called on the following goal:
+
+```lean
+xs : list ℕ,
+h : ∃ (x : ℕ) (H : x ∈ xs), x < 3
+⊢ ∀ (y : ℕ), y ∈ xs → y < 5
+```
+
+The local constants are reverted and an instance is found for
+`testable (∀ (xs : list ℕ), (∃ x ∈ xs, x < 3) → (∀ y ∈ xs, y < 5))`.
+The `testable` instance is supported by instances of `sampleable (list ℕ)`,
+`decidable (x < 3)` and `decidable (y < 5)`. `slim_check` builds a 
+`testable` instance step by step with:
+
+```
+- testable (∀ (xs : list ℕ), (∃ x ∈ xs, x < 3) → (∀ y ∈ xs, y < 5)) 
+                                     -: sampleable (list xs)
+- testable ((∃ x ∈ xs, x < 3) → (∀ y ∈ xs, y < 5))
+- testable (∀ x ∈ xs, x < 3 → (∀ y ∈ xs, y < 5))
+- testable (x < 3 → (∀ y ∈ xs, y < 5))
+                                     -: decidable (x < 3) 
+- testable (∀ y ∈ xs, y < 5)
+                                     -: decidable (y < 5) 
+```
+
+`sampleable (list ℕ)` lets us create random data of type `list ℕ` in a way that
+helps find small counter-examples.  Next, the test of the proposition
+hinges on `x < 3` and `y < 5` to both be decidable. The
+implication between the two could be tested as a whole but it would be
+less informative. Indeed, if we generate lists that only contain numbers
+greater than `3`, the implication will always trivially hold but we should 
+conclude that we haven't found meaningful examples. Instead, when `x < 3`
+does not hold, we reject the example (i.e.  we do not count it toward
+the 100 required positive examples) and we start over. Therefore, when
+`slim_check` prints `Success`, it means that a hundred suitable lists
+were found and successfully tested.
+
+If no counter-examples are found, `slim_check` behaves like `admit`.
+
+`slim_check` can also be invoked using `#eval`:
+
+```lean
+#eval slim_check.testable.check (∀ (α : Type) (xs ys : list α), xs ++ ys = ys ++ xs)
+-- ===================
+-- Found problems!
+
+-- α := ℤ
+-- xs := [-4]
+-- ys := [1]
+-- -------------------
+```
+
+For more information on writing your own `sampleable` and `testable`
+instances, see `testing.slim_check.testable`.
+-/
+
+namespace tactic.interactive
+open tactic slim_check
+
+declare_trace slim_check.instance
+declare_trace slim_check.decoration
+declare_trace slim_check.discared
+open expr
+
+/-- Tree structure representing a `testable` instance. -/
+meta inductive instance_tree
+| node : name → expr → list instance_tree → instance_tree
+
+/-- Gather information about a `testable` instance. Given
+an expression of type `testable ?p`, gather the
+name of the `testable` instances that it is built from
+and the proposition that they test. -/
+meta def summarize_instance : expr → tactic instance_tree
+| (lam n bi d b) := do
+   v ← mk_local' n bi d,
+   summarize_instance $ b.instantiate_var v
+| e@(app f x) := do
+   `(testable %%p) ← infer_type e,
+   xs ← e.get_app_args.mmap_filter (try_core ∘ summarize_instance),
+   pure $ instance_tree.node e.get_app_fn.const_name p xs
+| e := do
+  failed
+
+/-- format a `instance_tree` -/
+meta def instance_tree.to_format : instance_tree → tactic format
+| (instance_tree.node n p xs) := do
+  xs ← format.join <$> (xs.mmap $ λ t, flip format.indent 2 <$> instance_tree.to_format t),
+  ys ← pformat!"testable ({p})",
+  pformat!"+ {n} :{format.indent ys 2}\n{xs}"
+
+meta instance instance_tree.has_to_tactic_format : has_to_tactic_format instance_tree :=
+⟨ instance_tree.to_format ⟩
+
+/--
+`slim_check` considers a proof goal and tries to generate examples
+that would contradict the statement.
+
+Let's consider the following proof goal.
+
+```lean
+xs : list ℕ,
+h : ∃ (x : ℕ) (H : x ∈ xs), x < 3
+⊢ ∀ (y : ℕ), y ∈ xs → y < 5
+```
+
+The local constants will be reverted and an instance will be found for
+`testable (∀ (xs : list ℕ), (∃ x ∈ xs, x < 3) → (∀ y ∈ xs, y < 5))`.
+The `testable` instance is supported by an instance of `sampleable (list ℕ)`,
+`decidable (x < 3)` and `decidable (y < 5)`.
+
+Examples will be created in ascending order of size (more or less)
+
+The first counter-examples found will be printed and will result in an error:
+
+```
+===================
+Found problems!
+
+xs := [1, 28]
+x := 1
+y := 28
+-------------------
+```
+
+If no counter-examples are found, `slim_check` behaves like `admit`.
+
+For more information on writing your own `sampleable` and `testable`
+instances, see `testing.slim_check.testable`.
+
+Optional arguments given with `slim_check_cfg`
+ * num_inst (default 100): number of examples to test properties with
+ * max_size (default 100): final size argument
+ * enable_tracing (default ff): enable the printing of discarded samples
+
+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.instance true`: print the instances of `testable` being used to test the proposition
+-/
+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 },
+  e ← mk_mapp ``testable.check [tgt, `(cfg), tgt', none],
+  `(@testable.check _ _ _ %%inst) ← pure e,
+  when_tracing `slim_check.decoration trace!"[testable decoration]\n  {tgt'}",
+  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 }
+
+end tactic.interactive
diff --git a/src/testing/slim_check/gen.lean b/src/testing/slim_check/gen.lean
new file mode 100644
index 0000000000000..d32b890357725
--- /dev/null
+++ b/src/testing/slim_check/gen.lean
@@ -0,0 +1,125 @@
+/-
+Copyright (c) 2020 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Simon Hudon
+-/
+
+import control.uliftable
+import system.random
+import system.random.basic
+
+/-!
+# `gen` Monad
+
+This monad is used to formulate randomized computations with a parameter
+to specify the desired size of the result.
+
+This is a port of the Haskell QuickCheck library.
+
+## Main definitions
+  * `gen` monad
+
+## Local notation
+
+ * `i .. j` : `Icc i j`, the set of values between `i` and `j` inclusively;
+
+## Tags
+
+random testing
+
+## References
+
+  * https://hackage.haskell.org/package/QuickCheck
+
+-/
+
+universes u v
+
+namespace slim_check
+
+/-- Monad to generate random examples to test properties with.
+It has a `nat` parameter so that the caller can decide on the
+size of the examples. -/
+@[reducible, derive [monad, is_lawful_monad]]
+def gen (α : Type u) := reader_t (ulift ℕ) rand α
+
+variable (α : Type u)
+
+local infix ` .. `:41 := set.Icc
+
+/-- Execute a `gen` inside the `io` monad using `i` as the example
+size and with a fresh random number generator. -/
+def io.run_gen {α} (x : gen α) (i : ℕ) : io α :=
+io.run_rand (x.run ⟨i⟩)
+
+namespace gen
+
+section rand
+
+variables [preorder α]
+
+/-- Lift `random.random` to the `gen` monad. -/
+def choose_any [random α] : gen α :=
+⟨ λ _, rand.random α ⟩
+
+variables {α}
+
+/-- Lift `random.random_r` to the `gen` monad. -/
+def choose [bounded_random α] (x y : α) (p : x ≤ y) : gen (x .. y) :=
+⟨ λ _, rand.random_r x y p ⟩
+
+end rand
+
+open nat (hiding choose)
+
+/-- Generate a `nat` example between `x` and `y`. -/
+def choose_nat (x y : ℕ) (p : x ≤ y) : gen (x .. y) :=
+choose x y p
+
+open nat
+
+instance : uliftable gen.{u} gen.{v} :=
+reader_t.uliftable' (equiv.ulift.trans equiv.ulift.symm)
+
+instance : has_orelse gen.{u} :=
+⟨ λ α x y, do
+  b ← uliftable.up $ choose_any bool,
+  if b.down then x else y ⟩
+
+variable {α}
+
+/-- Get access to the size parameter of the `gen` monad. For
+reasons of universe polymorphism, it is specified in
+continuation passing style. -/
+def sized (cmd : ℕ → gen α) : gen α :=
+⟨ λ ⟨sz⟩, reader_t.run (cmd sz) ⟨sz⟩ ⟩
+
+/-- Create `n` examples using `cmd`. -/
+def vector_of : ∀ (n : ℕ) (cmd : gen α), gen (vector α n)
+| 0 _ := return vector.nil
+| (succ n) cmd := vector.cons <$> cmd <*> vector_of n cmd
+
+/-- Create a list of examples using `cmd`. The size is controlled
+by the size parameter of `gen`. -/
+def list_of (cmd : gen α) : gen (list α) :=
+sized $ λ sz, do
+do ⟨ n ⟩ ← uliftable.up $ choose_nat 0 (sz + 1) dec_trivial,
+   v ← vector_of n.val cmd,
+   return v.to_list
+
+open ulift
+
+/-- Given a list of example generators, choose one to create an example.
+This definition is needed for to provide a local `fact $ 0 < xs.length`
+instance to the type resolution system. -/
+def one_of_aux (xs : list (gen α)) (pos : fact $ 0 < xs.length) : gen α := do
+n ← uliftable.up $ choose_any (fin xs.length),
+list.nth_le xs (down n).val (down n).is_lt
+
+/-- Given a list of example generators, choose one to create an example. -/
+def one_of (xs : list (gen α)) (pos : 0 < xs.length) : gen α := do
+one_of_aux xs pos
+
+end gen
+
+end slim_check
diff --git a/src/testing/slim_check/sampleable.lean b/src/testing/slim_check/sampleable.lean
new file mode 100644
index 0000000000000..efdc15ee146a8
--- /dev/null
+++ b/src/testing/slim_check/sampleable.lean
@@ -0,0 +1,294 @@
+/-
+Copyright (c) 2020 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Simon Hudon
+-/
+import data.lazy_list
+import data.lazy_list2
+import data.tree
+import tactic.linarith
+import testing.slim_check.gen
+
+/-!
+# `sampleable` Class
+
+This class permits the creation samples of a given type
+controlling the size of those values using the `gen` monad`. It also
+helps minimize examples by creating smaller versions of given values.
+
+When testing a proposition like `∀ n : ℕ, prime n → n ≤ 100`,
+`slim_check` requires that `ℕ` have an instance of `sampleable` and for
+`prime n` to be decidable.  `slim_check` will then use the instance of
+`sampleable` to generate small examples of ℕ and progressively increase
+in size. For each example `n`, `prime n` is tested. If it is false,
+the example will be rejected (not a test success nor a failure) and
+`slim_check` will move on to other examples. If `prime n` is true, `n
+≤ 100` will be tested. If it is false, `n` is a counter-example of `∀
+n : ℕ, prime n → n ≤ 100` and the test fails. If `n ≤ 100` is true,
+the test passes and `slim_check` moves on to trying more examples.
+
+
+This is a port of the Haskell QuickCheck library.
+
+## Main definitions
+  * `sampleable` class
+
+## Tags
+
+random testing
+
+## References
+
+  * https://hackage.haskell.org/package/QuickCheck
+
+-/
+universes u
+
+namespace slim_check
+
+variables (α : Type u)
+
+/-- `sampleable α` provides ways of creating examples of type `α`,
+and given such an example `x : α`, gives us a way to shrink it
+and find simpler examples.  -/
+class sampleable :=
+(sample [] : gen α)
+(shrink : α → lazy_list α)
+
+export sampleable (sample shrink)
+
+open nat lazy_list
+
+/-- Apply `f` to combine every element of the first list with every element
+of the second list and interleave the resulting lists.
+
+For instance `lseq prod.mk [1,2,3] [4,5,6]` results in
+
+```
+[(1, 4), (2, 4), (1, 5), (3, 4), (1, 6), (2, 5), (3, 5), (2, 6), (3, 6)]
+```
+
+The purpose is to take two lists of shrunken values in ascending order of size
+and produce a list of combined values in roughly ascending order of size too.
+
+If we add the samples instead with `lseq (+) [1,2,3] [1,2,3]`, we
+obtain:
+
+```
+[2, 3, 3, 4, 4, 4, 5, 5, 6]
+```
+ -/
+def lazy_list.lseq {α β γ} (f : α → β → γ) : lazy_list α → lazy_list β → lazy_list γ
+| lazy_list.nil xs := lazy_list.nil
+| (lazy_list.cons x xs) lazy_list.nil := lazy_list.nil
+| (lazy_list.cons x xs) ys := interleave (ys.map $ f x) (lazy_list.lseq (xs ()) ys)
+
+/-- `nat.shrink' k n` creates a list of smaller natural numbers by
+successively dividing `n` by 2 and subtracting the difference from
+`k`. For example, `nat.shrink 100 = [50, 75, 88, 94, 97, 99]`. -/
+def nat.shrink' (k : ℕ) : ℕ → list ℕ → list ℕ
+| n ls :=
+if h : n ≤ 1
+  then ls.reverse
+  else
+    have 1 * n / 2 < n,
+      from nat.div_lt_of_lt_mul (nat.mul_lt_mul_of_pos_right (by norm_num) (by linarith)),
+    have n / 2 < n, by simpa,
+    let m := n / 2 in
+    nat.shrink' m ((k - m) :: ls)
+
+/-- `nat.shrink n` creates a list of smaller natural numbers by
+successively dividing by 2 and subtracting the difference from
+`n`. For example, `nat.shrink 100 = [50, 75, 88, 94, 97, 99]`. -/
+def nat.shrink (n : ℕ) : list ℕ :=
+nat.shrink' n n []
+
+open gen
+
+/--
+Transport a `sampleable` instance from a type `α` to a type `β` using
+functions between the two, going in both directions.
+-/
+def sampleable.lift (α : Type u) {β : Type u} [sampleable α] (f : α → β) (g : β → α) : sampleable β :=
+{ sample := f <$> sample α,
+  shrink := λ x, f <$> shrink (g x) }
+
+instance sampleable_nat : sampleable ℕ :=
+{ sample := sized $ λ sz, coe <$> choose_any (fin $ succ (sz^3)) <|>
+                          coe <$> choose_any (fin $ succ sz),
+  shrink := lazy_list.of_list ∘ nat.shrink }
+
+instance sampleable_pnat : sampleable ℕ+ :=
+sampleable.lift ℕ nat.succ_pnat (λ i, i - 1)
+
+/-- `int.shrink' k n` creates a list of integers by successively
+dividing `n` by 2, subtracting the result from `k` and alternating the signs.
+For example, `int.shrink 40 = [20, -20, 30, -30, 35, -35, 38, -38, 39, -39]`. -/
+def int.shrink' (k : ℕ) : ℕ → list ℤ → list ℤ
+| n ls :=
+if h : 1 < n
+  then
+    have n / 2 < n, from div_lt_self (by linarith) (by norm_num),
+    let m := n / 2 in
+    let m' := k - m in
+    int.shrink' m (-↑m' :: m' :: ls)
+  else ls.reverse
+
+/-- `int.shrink n` creates a list of integers by successively
+dividing by 2, subtracting the result from `n` and alternating the signs.
+For example, `int.shrink 40 = [20, -20, 30, -30, 35, -35, 38, -38, 39, -39]`. -/
+def int.shrink (i : ℤ) : list ℤ :=
+int.shrink' (int.nat_abs i) (int.nat_abs i) []
+
+instance sampleable_int : sampleable ℤ :=
+{ sample := sized $ λ sz,
+       let k := sz^5 in
+       (λ n : fin _, n.val - int.of_nat (k / 2) ) <$> choose_any (fin $ succ k),
+  shrink := lazy_list.of_list ∘ int.shrink   }
+
+instance sampleable_bool : sampleable bool :=
+{ sample := do { x ← choose_any bool,
+                 return x },
+  shrink := λ _, lazy_list.nil }
+
+instance sampleable_prod {β} [sampleable α] [sampleable β] : sampleable (α × β) :=
+{ sample := do { ⟨x⟩ ← uliftable.up $ sample α,
+                 ⟨y⟩ ← uliftable.up $ sample β,
+                 pure (x,y) },
+  shrink := λ x, lazy_list.lseq prod.mk (shrink x.1) (shrink x.2) }
+
+/-- shrinking function for sum types -/
+def sum.shrink {β} [sampleable α] [sampleable β] : α ⊕ β → lazy_list (α ⊕ β)
+| (sum.inr x) := (shrink x).map sum.inr
+| (sum.inl x) := (shrink x).map sum.inl
+
+instance sampleable_sum {β} [sampleable α] [sampleable β] : sampleable (α ⊕ β) :=
+{ sample := uliftable.up_map sum.inl (sample α) <|>
+            uliftable.up_map sum.inr (sample β),
+  shrink := sum.shrink _ }
+
+instance sampleable_rat : sampleable ℚ :=
+sampleable.lift (ℤ × ℕ+) (λ x, prod.cases_on x rat.mk_pnat) (λ r, (r.num, ⟨r.denom, r.pos⟩))
+
+/-- `sampleable_char` can be specialized into customized `sampleable char` instances.
+
+The resulting instance has `1 / length` chances of making an unrestricted choice of characters
+and it otherwise chooses a character from `characters` with uniform probabilities.  -/
+def sampleable_char (length : nat) (characters : string) : sampleable char :=
+{ sample := do { x ← choose_nat 0 length dec_trivial,
+                 if x.val = 0 then do
+                   n ← sample ℕ,
+                   pure $ char.of_nat n
+                 else do
+                   i ← choose_nat 0 (characters.length - 1) dec_trivial,
+                   pure (characters.mk_iterator.nextn i).curr },
+  shrink := λ _, lazy_list.nil }
+
+instance : sampleable char :=
+sampleable_char 3 " 0123abcABC:,;`\\/"
+
+variables {α}
+
+/-- implementation of `sampleable (list α)` -/
+def list.shrink' (shrink_a : α → lazy_list α) : list α → lazy_list (list α)
+| [] := lazy_list.nil
+| (x :: xs) :=
+  let ys := list.shrink' xs in
+  interleave ys $ lazy_list.lseq (::) ((shrink_a x).append (lazy_list.singleton x)) (lazy_list.cons [] ys)
+
+/-- `list.shrink_with shrink_f xs` shrinks `xs` by deleting various items of the list
+and shrinking others (using `shrink_f`). `lseq` is being used to interleave the
+resulting shrunken lists to put smaller lists earlier in the results. -/
+def list.shrink_with (shrink_a : α → lazy_list α) (xs : list α) : lazy_list (list α) :=
+(list.shrink' shrink_a xs).init
+
+instance sampleable_list [sampleable α] : sampleable (list α) :=
+{ sample := list_of (sample α),
+  shrink := list.shrink_with shrink  }
+
+instance sampleable_prop : sampleable Prop :=
+{ sample := do { x ← choose_any bool,
+               return ↑x },
+  shrink := λ _, lazy_list.nil }
+
+instance sampleable_string : sampleable string :=
+{ sample := do { x ← list_of (sample char), pure x.as_string },
+  shrink := λ s, (shrink s.to_list).map list.as_string }
+
+/-- implementation of `sampleable (tree α)` -/
+def tree.sample (sample : gen α) : ℕ → gen (tree α) | n :=
+if h : n > 0
+then have n / 2 < n, from div_lt_self h (by norm_num),
+     tree.node <$> sample <*> tree.sample (n / 2) <*> tree.sample (n / 2)
+else pure tree.nil
+
+/-- `tree.shrink_with shrink_f t` shrinks `xs` by using subtrees, shrinking them,
+shrinking the contents and recombining the results into bigger trees. -/
+def tree.shrink_with (shrink_a : α → lazy_list α) : tree α → lazy_list (tree α)
+| tree.nil := lazy_list.nil
+| (tree.node x t₀ t₁) :=
+-- here, we drop the last tree of the interleaved lists because it is assumed
+-- to be the full tree, i.e., not a shrunken tree.
+lazy_list.init $ interleave_all [(tree.shrink_with t₀).append (lazy_list.singleton t₀),
+                                 (tree.shrink_with t₁).append (lazy_list.singleton t₁),
+                                 lazy_list.lseq id (lazy_list.lseq tree.node (shrink_a x) (tree.shrink_with t₀)) (tree.shrink_with t₁) ]
+
+instance sampleable_tree [sampleable α] : sampleable (tree α) :=
+{ sample := sized $ tree.sample (sample α),
+  shrink := tree.shrink_with shrink }
+
+setup_tactic_parser
+
+/--
+Print (at most) 10 samples of a given type to stdout for debugging.
+-/
+def print_samples (t : Type u) [sampleable t] [has_repr t] : io unit := do
+xs ← io.run_rand $ uliftable.down $
+  do { xs ← (list.range 10).mmap $ (sample t).run ∘ ulift.up,
+       pure ⟨xs.map repr⟩ },
+xs.mmap' io.put_str_ln
+
+/--
+`#sample my_type`, where `my_type` has an instance of `sampleable`, prints ten random
+values of type `my_type` of using an increasing size parameter.
+
+```lean
+#sample nat
+-- prints
+-- 0
+-- 0
+-- 2
+-- 24
+-- 64
+-- 76
+-- 5
+-- 132
+-- 8
+-- 449
+-- or some other sequence of numbers
+
+#sample list int
+-- prints
+-- []
+-- [1, 1]
+-- [-7, 9, -6]
+-- [36]
+-- [-500, 105, 260]
+-- [-290]
+-- [17, 156]
+-- [-2364, -7599, 661, -2411, -3576, 5517, -3823, -968]
+-- [-643]
+-- [11892, 16329, -15095, -15461]
+-- or whatever
+```
+-/
+@[user_command]
+meta def sample_cmd (_ : parse $ tk "#sample") : lean.parser unit :=
+do e ← texpr,
+   of_tactic $ do
+     e ← tactic.i_to_expr e,
+     print_samples ← tactic.mk_mapp ``print_samples [e,none,none],
+     sample ← tactic.eval_expr (io unit) print_samples,
+     tactic.unsafe_run_io sample
+
+end slim_check
diff --git a/src/testing/slim_check/testable.lean b/src/testing/slim_check/testable.lean
new file mode 100644
index 0000000000000..935f94d663355
--- /dev/null
+++ b/src/testing/slim_check/testable.lean
@@ -0,0 +1,580 @@
+/-
+Copyright (c) 2020 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Simon Hudon
+-/
+
+import testing.slim_check.sampleable
+
+/-!
+# `testable` Class
+
+Testable propositions have a procedure that can generate counter-examples
+together with a proof that they invalidate the proposition.
+
+This is a port of the Haskell QuickCheck library.
+
+## Creating Customized Instances
+
+The type classes `testable` and `sampleable` are the means by which
+`slim_check` creates samples and tests them. For instance, the proposition
+`∀ i j : ℕ, i ≤ j` has a `testable` instance because `ℕ` is sampleable
+and `i ≤ j` is decidable. Once `slim_check` finds the `testable`
+instance, it can start using the instance to repeatedly creating samples
+and checking whether they satisfy the property. This allows the
+user to create new instances and apply `slim_check` to new situations.
+
+### Polymorphism
+
+The property `testable.check (∀ (α : Type) (xs ys : list α), xs ++ ys
+= ys ++ xs)` shows us that type-polymorphic properties can be
+tested. `α` is instantiated with `ℤ` first and then tested as normal
+monomorphic properties.
+
+The monomorphisation limits the applicability of `slim_check` to
+polymorphic properties that can be stated about integers. The
+limitation may be lifted in the future but, for now, if
+one wishes to use a different type than `ℤ`, one has to refer to
+the desired type.
+
+### What do I do if I'm testing a property about my newly defined type?
+
+Let us consider a type made for a new formalization:
+
+```lean
+structure my_type :=
+(x y : ℕ)
+(h : x ≤ y)
+```
+
+How do we test a property about `my_type`? For instance, let us consider
+`testable.check $ ∀ a b : my_type, a.y ≤ b.x → a.x ≤ b.y`. Writing this
+property as is will give us an error because we do not have an instance
+of `sampleable my_type`. We can define one as follows:
+
+```lean
+instance : sampleable my_type :=
+{ sample := do
+  x ← sample ℕ,
+  xy_diff ← sample ℕ,
+  return { x := x, y := x + xy_diff, h := /- some proof -/ } }
+```
+
+We can see that the instance is very simple because our type is built
+up from other type that have `sampleable` instances. `sampleable` also
+has a `shrink` method but it is optional. We may want to implement one
+for ease of testing as:
+
+```lean
+/- ... -/
+  shrink := λ ⟨x,y,h⟩, (λ ⟨x,y⟩, { x := x, y := x + y, h := /- proof -/}) <$> shrink (x, y - x)
+}
+```
+
+Again, we take advantage of the fact that other types have useful
+`shrink` implementations, in this case `prod`.
+
+### Optimizing the sampling
+
+Some properties are guarded by a proposition. For instance, recall this
+example:
+
+```lean
+#eval testable.check (∀ x : ℕ, 2 ∣ x → x < 100)
+```
+
+When testing the above example, we generate a natural number, we check
+that it is even and test it if it is even or throw it away and start
+over otherwise. Statistically, we can expect half of our samples to be
+thrown away by such a filter. Sometimes, the filter is more
+restrictive. For instance we might need `x` to be a `prime`
+number. This would cause most of our samples to be discarded.
+
+We can help `slim_check` find good samples by providing specialized
+sampleable instances. Below, we show an instance for the subtype
+of even natural numbers. This means that, when producing
+a sample, it is forced to produce a proof that it is even.
+
+```lean
+instance {k : ℕ} [fact (0 < k)] : sampleable { x : ℕ // k ∣ x } :=
+{ sample := do { n ← sample ℕ, pure ⟨k*n, dvd_mul_right _ _⟩ },
+  shrink := λ ⟨x,h⟩, (λ y, ⟨k*y, dvd_mul_right _ _⟩) <$> shrink x }
+```
+
+Such instance will be preferred when testing a proposition of the shape
+`∀ x : T, p x → q`
+
+We can observe the effect by enabling tracing:
+
+```lean
+/- no specialized sampling -/
+#eval testable.check (∀ x : ℕ, 2 ∣ x → x < 100) { enable_tracing := tt }
+-- discard
+--  x := 1
+-- discard
+--  x := 41
+-- discard
+--  x := 3
+-- discard
+--  x := 5
+-- discard
+--  x := 5
+-- discard
+--  x := 197
+-- discard
+--  x := 469
+-- discard
+--  x := 9
+-- discard
+
+-- ===================
+-- Found problems!
+
+-- x := 552
+-- -------------------
+
+/- let us define a specialized sampling instance -/
+instance {k : ℕ} : sampleable { x : ℕ // k ∣ x } :=
+{ sample := do { n ← sample ℕ, pure ⟨k*n, dvd_mul_right _ _⟩ },
+  shrink := λ ⟨x,h⟩, (λ y, ⟨k*y, dvd_mul_right _ _⟩) <$> shrink x }
+
+#eval testable.check (∀ x : ℕ, 2 ∣ x → x < 100) { enable_tracing := tt }
+-- ===================
+-- Found problems!
+
+-- x := 358
+-- -------------------
+```
+
+## Main definitions
+  * `testable` class
+  * `testable.check`: a way to test a proposition using random examples
+
+## Tags
+
+random testing
+
+## References
+
+  * https://hackage.haskell.org/package/QuickCheck
+
+-/
+
+universes u v
+
+variables var var' : string
+variable α : Type u
+variable β : α → Prop
+variable f : Type → Prop
+
+namespace slim_check
+
+/-- Result of trying to disprove `p`
+
+The constructors are:
+  *  `success : (psum unit p) → test_result`
+     succeed when we find another example satisfying `p`
+     In `success h`, `h` is an optional proof of the proposition.
+     Without the proof, all we know is that we found one example
+     where `p` holds. With a proof, the one test was sufficient to
+     prove that `p` holds and we do not need to keep finding examples.
+   * `gave_up {} : ℕ → test_result`
+     give up when a well-formed example cannot be generated.
+     `gave_up n` tells us that `n` invalid examples were tried.
+     Above 100, we give up on the proposition and report that we
+     did not find a way to properly test it.
+   * `failure : ¬ p → (list string) → test_result`
+     a counter-example to `p`; the strings specify values for the relevant variables.
+     `failure h vs` also carries a proof that `p` does not hold. This way, we can
+     guarantee no false positive.
+-/
+@[derive inhabited]
+inductive test_result (p : Prop)
+| success : (psum unit p) → test_result
+| gave_up {} : ℕ → test_result
+| failure : ¬ p → (list string) → test_result
+
+/-- format a `test_result` as a string. -/
+def test_result.to_string {p} : test_result p → string
+| (test_result.success (psum.inl ())) := "success (without proof)"
+| (test_result.success (psum.inr h)) := "success (with proof)"
+| (test_result.gave_up n) := sformat!"gave up {n} times"
+| (test_result.failure a vs) := sformat!"failed {vs}"
+
+instance {p} : has_to_string (test_result p) := ⟨ test_result.to_string ⟩
+
+/-- `testable p` uses random examples to try to disprove `p`. -/
+class testable (p : Prop) :=
+(run [] (enable_tracing minimize : bool) : gen (test_result p))
+
+open list
+
+open test_result
+
+/-- applicative combinator proof carrying test results -/
+def combine {p q : Prop} : psum unit (p → q) → psum unit p → psum unit q
+| (psum.inr f) (psum.inr x) := psum.inr (f x)
+| _ _ := psum.inl ()
+
+/-- Combine the test result for properties `p` and `q` to create a test for their conjunction. -/
+def and_counter_example {p q : Prop} :
+  test_result p →
+  test_result q →
+  test_result (p ∧ q)
+| (failure Hce xs) _ := failure (λ h, Hce h.1) xs
+| _ (failure Hce xs) := failure (λ h, Hce h.2) xs
+| (success xs) (success ys) := success $ combine (combine (psum.inr and.intro) xs) ys
+| (gave_up n) (gave_up m) := gave_up $ n + m
+| (gave_up n) _ := gave_up n
+| _ (gave_up n) := gave_up n
+
+/-- Combine the test result for properties `p` and `q` to create a test for their disjunction -/
+def or_counter_example {p q : Prop} :
+  test_result p →
+  test_result q →
+  test_result (p ∨ q)
+| (failure Hce xs) (failure Hce' ys) := failure (λ h, or_iff_not_and_not.1 h ⟨Hce, Hce'⟩) (xs ++ ys)
+| (success xs) _ := success $ combine (psum.inr or.inl) xs
+| _ (success ys) := success $ combine (psum.inr or.inr) ys
+| (gave_up n) (gave_up m) := gave_up $ n + m
+| (gave_up n) _ := gave_up n
+| _ (gave_up n) := gave_up n
+
+/-- If `q → p`, then `¬ p → ¬ q` which means that testing `p` can allow us
+to find counter-examples to `q`. -/
+def convert_counter_example {p q : Prop}
+  (h : q → p) :
+  test_result p →
+  opt_param (psum unit (p → q)) (psum.inl ()) →
+  test_result q
+| (failure Hce xs) _ := failure (mt h Hce) xs
+| (success Hp) Hpq := success (combine Hpq Hp)
+| (gave_up n) _ := gave_up n
+
+/-- Test `q` by testing `p` and proving the equivalence between the two. -/
+def convert_counter_example' {p q : Prop}
+  (h : p ↔ q) (r : test_result p) :
+  test_result q :=
+convert_counter_example h.2 r (psum.inr h.1)
+
+/-- When we assign a value to a universally quantified variable,
+we record that value using this function so that our counter-examples
+can be informative. -/
+def add_to_counter_example (x : string) {p q : Prop}
+  (h : q → p) :
+  test_result p →
+  opt_param (psum unit (p → q)) (psum.inl ()) →
+  test_result q
+| (failure Hce xs) _ := failure (mt h Hce) $ x :: xs
+| r hpq := convert_counter_example h r hpq
+
+/-- Add some formatting to the information recorded by `add_to_counter_example`. -/
+def add_var_to_counter_example {γ : Type v} [has_to_string γ]
+  (var : string) (x : γ) {p q : Prop}
+  (h : q → p) : test_result p →
+  opt_param (psum unit (p → q)) (psum.inl ()) →
+  test_result q :=
+@add_to_counter_example (var ++ " := " ++ to_string x) _ _ h
+
+/-- Gadget used to introspect the name of bound variables.
+
+It is used with the `testable` typeclass so that
+`testable (named_binder "x" (∀ x, p x))` can use the variable name
+of `x` in error messages displayed to the user. If we find that instantiating
+the above quantifier with 3 falsifies it, we can print:
+
+```
+==============
+Problem found!
+==============
+x := 3
+```
+ -/
+@[simp, nolint unused_arguments]
+def named_binder (n : string) (p : Prop) : Prop := p
+
+/-- Is the given test result a failure? -/
+def is_failure {p} : test_result p → bool
+| (test_result.failure _ _) := tt
+| _ := ff
+
+instance and_testable (p q : Prop) [testable p] [testable q] :
+  testable (p ∧ q) :=
+⟨ λ tracing min, do
+   xp ← testable.run p tracing min,
+   xq ← testable.run q tracing min,
+   pure $ and_counter_example xp xq ⟩
+
+instance or_testable (p q : Prop) [testable p] [testable q] :
+  testable (p ∨ q) :=
+⟨ λ tracing min, do
+   xp ← testable.run p tracing min,
+   match xp with
+   | success (psum.inl h) := pure $ success (psum.inl h)
+   | success (psum.inr h) := pure $ success (psum.inr $ or.inl h)
+   | _ := do
+     xq ← testable.run q tracing min,
+     pure $ or_counter_example xp xq
+   end ⟩
+
+@[priority 1000]
+instance imp_dec_testable (p : Prop) [decidable p] (β : p → Prop)
+  [∀ h, testable (β h)] : testable (named_binder var $ Π h, β h) :=
+⟨ λ tracing min, do
+    if h : p
+    then (λ r, convert_counter_example ($ h) r (psum.inr $ λ q _, q)) <$> testable.run (β h) tracing min
+    else if tracing then  trace "discard" $ return $ gave_up 1
+    else return $ gave_up 1 ⟩
+
+@[priority 2000]
+instance all_types_testable [testable (f ℤ)] : testable (named_binder var $ Π x, f x) :=
+⟨ λ tracing min, do
+    r ← testable.run (f ℤ) tracing min,
+    return $ add_var_to_counter_example var "ℤ" ($ ℤ) r ⟩
+
+/-- Trace the value of sampled variables if the sample is discarded. -/
+def trace_if_giveup {p α β} [has_to_string α] (tracing_enabled : bool) (var : string) (val : α) :
+  test_result p → thunk β → β
+| (test_result.gave_up _) :=
+  if tracing_enabled then trace (sformat!" {var} := {val}")
+  else ($ ())
+| _ := ($ ())
+
+/-- testable instance for a property iterating over the element of a list -/
+@[priority 5000]
+instance test_forall_in_list
+  [∀ x, testable (β x)] [has_to_string α] :
+  Π xs : list α, testable (named_binder var $ ∀ x, named_binder var' $ x ∈ xs → β x)
+| [] := ⟨ λ tracing min, return $ success $ psum.inr (by { introv x h, cases h} ) ⟩
+| (x :: xs) :=
+⟨ λ tracing min, do
+    r ← testable.run (β x) tracing min,
+    trace_if_giveup tracing var x r $
+      match r with
+      | failure _ _ := return $ add_var_to_counter_example var x
+                                 (by { intro h, apply h, left, refl }) r
+      | success hp := do
+         rs ← @testable.run _ (test_forall_in_list xs) tracing min,
+         return $ convert_counter_example
+                                 (by { intros h i h',
+                                       apply h,
+                                       right, apply h' })
+                                 rs
+                                 (combine (psum.inr
+                                  $ by { intros j h, simp only [ball_cons,named_binder],
+                                         split ; assumption, } ) hp)
+      | gave_up n := do
+         rs ← @testable.run _ (test_forall_in_list xs) tracing min,
+         match rs with
+         | (success _) := return $ gave_up n
+         | (failure Hce xs) := return $ failure
+                      (by { simp only [ball_cons,named_binder],
+                            apply not_and_of_not_right _ Hce, }) xs
+         | (gave_up n') := return $ gave_up (n + n')
+         end
+      end ⟩
+
+/-- Test proposition `p` by randomly selecting one of the provided
+testable instances. -/
+def combine_testable (p : Prop)
+  (t : list $ testable p) (h : 0 < t.length) : testable p :=
+⟨ λ tracing min, have 0 < length (map (λ t, @testable.run _ t tracing min) t),
+    by { rw [length_map], apply h },
+  gen.one_of (list.map (λ t, @testable.run _ t tracing min) t) this ⟩
+
+/-- Once a property fails to hold on an example, look for smaller counter-examples
+to show the user. -/
+def minimize [∀ x, testable (β x)] (x : α) (r : test_result (β x)) : lazy_list α → gen (Σ x, test_result (β x))
+| lazy_list.nil := pure ⟨x,r⟩
+| (lazy_list.cons x xs) := do
+  ⟨r⟩ ← uliftable.up $ testable.run (β x) ff tt,
+     if is_failure r
+       then pure ⟨x, convert_counter_example id r (psum.inl ())⟩
+       else minimize $ xs ()
+
+@[priority 2000]
+instance exists_testable (p : Prop)
+  [testable (named_binder var (∀ x, named_binder var' $ β x → p))] :
+  testable (named_binder var' (named_binder var (∃ x, β x) → p)) :=
+⟨ λ tracing min, do
+    x ← testable.run (named_binder var (∀ x, named_binder var' $ β x → p)) tracing min,
+    pure $ convert_counter_example' exists_imp_distrib.symm x ⟩
+
+@[priority 5000]
+instance exists_testable' (xs : list α) (p : Prop)
+  [testable (named_binder var (∀ x, named_binder "H" $ x ∈ xs → named_binder var' (β x → p)))] :
+  testable (named_binder var' (named_binder var (∃ x ∈ xs, β x) → p)) :=
+⟨ λ tracing min, do
+    x ← testable.run (named_binder var (∀ x, named_binder "H" $ x ∈ xs → named_binder var' (β x → p))) tracing min,
+    pure $ convert_counter_example' (by simp) x ⟩
+
+/-- Test a universal property by creating a sample of the right type and instantiating the
+bound variable with it. -/
+instance var_testable [has_to_string α] [sampleable α] [∀ x, testable (β x)] : testable (named_binder var $ Π x : α, β x) :=
+⟨ λ tracing min, do
+   uliftable.adapt_down (sample α) $
+   λ x, do
+     r ← testable.run (β x) tracing ff,
+     uliftable.adapt_down (if is_failure r ∧ min
+                          then minimize _ _ x r (shrink x)
+                          else pure ⟨x,r⟩) $
+     λ ⟨x,r⟩, return (trace_if_giveup tracing var x r $ add_var_to_counter_example var x ($ x) r) ⟩
+
+@[priority 3000]
+instance unused_var_testable (β) [inhabited α] [testable β] : testable (named_binder var $ Π x : α, β) :=
+⟨ λ tracing min, do
+  r ← testable.run β tracing min,
+  pure $ convert_counter_example ($ default _) r (psum.inr $ λ x _, x) ⟩
+
+@[priority 2000]
+instance subtype_var_testable (p : α → Prop) [has_to_string α] [sampleable (subtype p)]
+  [∀ x, testable (β x)] :
+  testable (named_binder var $ Π x : α, named_binder var' $ p x → β x) :=
+⟨ λ tracing min,
+   do r ← @testable.run (∀ x : subtype p, β x.val) (slim_check.var_testable var _ _) tracing min,
+      pure $ convert_counter_example'
+        ⟨λ (h : ∀ x : subtype p, β x) x h', h ⟨x,h'⟩,
+         λ h ⟨x,h'⟩, h x h'⟩
+        r ⟩
+
+@[priority 100]
+instance decidable_testable (p : Prop) [decidable p] : testable p :=
+⟨ λ tracing min, return $ if h : p then success (psum.inr h) else failure h [] ⟩
+
+section io
+
+open nat
+variable {p : Prop}
+
+/-- Execute `cmd` and repeat every time the result is `gave_up` (at most
+`n` times). -/
+def retry (cmd : rand (test_result p)) : ℕ → rand (test_result p)
+| 0 := return $ gave_up 1
+| (succ n) := do
+r ← cmd,
+match r with
+| success hp := return $ success hp
+| (failure Hce xs) := return (failure Hce xs)
+| (gave_up _) := retry n
+end
+
+/-- Count the number of times the test procedure gave up. -/
+def give_up (x : ℕ) : test_result p → test_result p
+| (success (psum.inl ())) := gave_up x
+| (success (psum.inr p))  := success (psum.inr p)
+| (gave_up n) := gave_up (n+x)
+| (failure Hce xs) := failure Hce xs
+
+variable (p)
+
+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
+
+/-- 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)
+| r 0 := return r
+| r (succ n) :=
+do let size := (cfg.num_inst - n - 1) * cfg.max_size / cfg.num_inst,
+   x ← retry ( (testable.run p cfg.enable_tracing tt).run ⟨ size ⟩) 10,
+   match x with
+   | (success (psum.inl ())) := testable.run_suite_aux r n
+   | (success (psum.inr Hp)) := return $ success (psum.inr Hp)
+   | (failure Hce xs) := return (failure Hce xs)
+   | (gave_up g) := testable.run_suite_aux (give_up g r) n
+   end
+
+/-- Try to find a counter-example of `p`. -/
+def testable.run_suite (cfg : slim_check_cfg := {}) : rand (test_result p) :=
+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)
+
+namespace tactic
+
+open tactic expr
+
+/-!
+## Decorations
+
+Instances of `testable` use `named_binder` as a decoration on
+propositions in order to access the name of bound variables, as in
+`named_binder "x" (forall x, x < y)`.  This helps the
+`testable` instances create useful error messages where variables
+are matched with values that falsify a given proposition.
+
+The following functions help support the gadget so that the user does
+not have to put them in themselves.
+-/
+
+/-- `add_existential_decorations p` adds `a `named_binder` annotation at the
+root of `p` if `p` is an existential quantification. -/
+meta def add_existential_decorations : expr → expr
+| e@`(@Exists %%α %%(lam n bi d b)) :=
+  let n := to_string n in
+  const ``named_binder [] (`(n) : expr) e
+| e := e
+
+/-- Traverse the syntax of a proposition to find universal quantifiers
+and existential quantifiers and add `named_binder` annotations next to
+them. -/
+meta def add_decorations : expr → expr | e :=
+e.replace $ λ e _,
+  match e with
+  | (pi n bi d b) :=
+    let n := to_string n in
+    some $ const ``named_binder [] (`(n) : expr)
+      (pi n bi (add_existential_decorations d) (add_decorations b))
+  | e := none
+  end
+
+/-- `decorations_of p` is used as a hint to `mk_decorations` to specify
+that the goal should be satisfied with a proposition equivalent to `p`
+with added annotations. -/
+@[reducible, nolint unused_arguments]
+def decorations_of (p : Prop) := Prop
+
+/-- In a goal of the shape `⊢ tactic.decorations_of p`, `mk_decoration` examines
+the syntax of `p` and add `named_binder` around universal quantifications and
+existential quantifications to improve error messages.
+
+This tool can be used in the declaration of a function as follows:
+
+```lean
+def foo (p : Prop) (p' : tactic.decorations_of p . mk_decorations) [testable p'] : ...
+```
+
+`p` is the parameter given by the user, `p'` is an equivalent proposition where
+the quantifiers are annotated with `named_binder`.
+-/
+meta def mk_decorations : tactic unit := do
+`(tactic.decorations_of %%p) ← target,
+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),
+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
+| (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
+end
+
+end io
+
+end slim_check