feat(testing): property based testing (basics) (#3915)

Add `gen` monad, `sampleable` and `testable` type classes

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

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

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