[Merged by Bors] - feat(testing): property based testing (basics) #3915

cipher1024 · 2020-08-23T00:35:59Z

Add gen monad, sampleable and testable type classes

Taken from #2080

src/testing/slim_check/arbitrary.lean

src/testing/slim_check/testable.lean

robertylewis · 2020-08-23T13:28:31Z

A number of my comments on #2080 still apply here.

I'm also not a fan of the name arbitrary for this class, since arbitrary T is already used for the irreducible witness to an inhabited type T.

cipher1024 · 2020-08-23T17:52:45Z

I'm also not a fan of the name arbitrary for this class, since arbitrary T is already used for the irreducible witness to an inhabited type T.

What would you rename it to? Maybe sampleable?

robertylewis · 2020-08-25T17:48:06Z

Yes, sampleable sounds better (and more grammatical). arby can be come sample.

src/testing/slim_check/gen.lean

src/testing/slim_check/sampleable.lean

robertylewis · 2020-08-26T13:40:23Z

src/testing/slim_check/testable.lean

+  test_result q :=
+@add_to_counter_example (var ++ " := " ++ to_string x) _ _ h
+
+/-- gadget used to introspect the name of bound variables -/


Could you explain this more? I'm not seeing quickly what this gadget is doing.

src/testing/slim_check/testable.lean

robertylewis · 2020-08-26T13:48:15Z

src/testing/slim_check/testable.lean

+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


I'm still trying to sort out exactly what's going on with these decorations, but this seems odd to have in the tactic namespace. (Note that you're still in slim_check too. If you wanted mk_decorations in _root_.tactic, it isn't there right now.)

Basically, the instance testable (named_binder (some "x") (∀ x, p x)) generates samples for x and, when the test fails, adds x := 37 to the error message that will be printed to the user. testable is pure code and does not have access to the syntax tree (esp. the name of bound variables) of ∀ x, p x so we use a gadget to make the name "x" available.

src/testing/slim_check/testable.lean

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

src/tactic/slim_check.lean

semorrison

LGTM

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

semorrison · 2020-09-01T09:52:24Z

I think this looks great now! There's documentation on the tactic that starts from the beginning, and later documentation that explains how to use the advanced features.

Shall we merge?

digama0 · 2020-09-01T10:18:34Z

I agree, the new tactic.slim_check file looks great.

bors r+

robertylewis · 2020-09-01T10:22:48Z

I agree, the new tactic.slim_check file looks great.

bors r+

I agree, thanks Simon!

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

bors · 2020-09-01T10:34:45Z

Build failed:

Build mathlib

robertylewis · 2020-09-01T10:44:28Z

Ah, this needs to be updated for 3.19.0.

into slim-check-gen-arby

src/data/fin.lean

robertylewis · 2020-09-01T18:53:21Z

bors merge

bors · 2020-09-01T18:53:24Z

👎 Rejected by label

robertylewis · 2020-09-01T18:53:45Z

bors merge

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

bors · 2020-09-01T19:30:24Z

Pull request successfully merged into master.

Build succeeded:

cipher1024 · 2020-09-01T19:52:43Z

Thank you all! Next step: smart generators for functions and testing for monadic programs (separate PRs)

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

cipher1024 added 2 commits August 22, 2020 20:06

feat(testing): bringing in random property based testing

c059f88

apply lint advice

bf96fa9

cipher1024 added the awaiting-review The author would like community review of the PR label Aug 23, 2020