[Merged by Bors] - feat(slim_check): sampleable instance for generating functions and injective functions

[cipher1024]

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.

---

[robertylewis]

The tests look really nice, there are some interesting features added here. But I'll admit that again I find this PR very difficult to review. I don't have a sense of what al the high-level additions are.

From the new tests, it's clear there are new testable instances that let slim_check work on Prop goals and function properties, which is great, and I see instances that add this (and a module doc specifically about functions). Are these features independent or related? I also see instances about functors -- is that part of these features? Another feature that doesn't appear in the tests? Are there other added features?

Basically, this is 1300 lines where my only guidance for reviewing is "new subtype instances of sampleable" and some tests. Besides my minor comments the code looks stylistically fine. And again the tests look great, having slim_check work on prop logic goals is really nice. But I don't know how to say much about the code as a whole because I can't separate the changes from the new features or the new features from each other.

Are all the changes here too intertwined to separate them? Ideally, there would be a PR that just adds the prop logic functionality (and tests), one that adds the function instances (and tests), etc.

[cipher1024]

The bulk of this PR is to allow me to generate samples of pi types. Because pi types mostly cannot have has_to_string and has_repr instances and cannot be deconstructed, I created the sampleable_ext class where every instance also has a proxy type. For a function, the proxy type is a table that will hold the entries of the function. That table can be printed and shrunk and makes pi types sampleable. The sampleable class remains and is a simpler class to instantiate if you don't need the whole proxy type business.

sampleable_functor is a simple way to define sampleable instances for collections like list. If you have a list of functions, the sampleable_ext instance will be chosen for that. Otherwise, it will go with sampleable instances.

[robertylewis]

@cipher1024 I'm sorry, I just don't know how to review this properly. There are too many changes in too many different places, and I don't have a good sense of what single goal the PR is trying to accomplish.

Do you promise that every new feature is documented and has multiple tests? If so: if you can address my couple comments here and change the PR title to show what features have been added, you can merge. But please, really try to split these PRs up as much as you can. If code needs to be refactored for a new feature to work, you can do the refactoring in one PR and the new feature in another. If two features are related but not the same, they should be two different PRs. I can't look at a diff this size and figure out myself the reasons for the changes.

bors d+

[bors]

✌️ cipher1024 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[cipher1024]

@robertylewis I promise all I did was tested and motivated by the tests I wrote. I take your point however and will try to break things up a bit more. Now that the basics for slim_check are in mathlib, I think it should get easier

[cipher1024]

And without further ado, I'm now going to merge it. Thanks @robertylewis !

bors r+

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests