QuickChick - Leonidas Lampropoulos

Stream: Lean Together 2024

[Mario Carneiro]

Just mentioning it for people who are wondering whether lean has an equivalent of QuickChick: mathlib provides a slim_check tactic, which is based on the same generation and minimization framework (I believe this is ultimately from a Haskell property testing framework called QuickCheck).

The features which were demoed today which I think aren't there in lean:

• the DecOpt typeclass and the ability to derive it for arbitrary types
• deriving a semidecision procedure for inductive propositions
• the ability to generate elements of an inductive satisfying a property (as opposed to just generating randomly and seeing if they satisfy the property)

[Adam Topaz]

During the question in this lecture the speaker (who seems to not be on this zulip) mentioned that there were a number of papers about generating data subject to some constraints, presumably in coq. Does anyone know what papers this was referring to, and where I can find them?

[Alex Vlasov]

Adam Topaz said:

During the question in this lecture the speaker (who seems to not be on this zulip) mentioned that there were a number of papers about generating data subject to some constraints, presumably in coq. Does anyone know what papers this was referring to, and where I can find them?

I'd suggest that you look at the Related Work section of the corresponding paper. It refers to several such papers, e.g.
https://arxiv.org/pdf/1607.05443.pdf but there are others

[Eric Wieser]

the ability to generate elements of an inductive satisfying a property (as opposed to just generating randomly and seeing if they satisfy the property)

I think slim_check can be trained to do this for specific types; for instance, we have something for injective functions from natural numbers

[Mario Carneiro]

Does that work with separate assumptions f : Nat -> Nat and Injective f?

[David Thrane Christiansen]

Another thing they've done in QuickChick is to provide some interesting semantics for property-based testing that allow verification of the testing

[David Thrane Christiansen]

The mutant feature is also a great way to validate your spec and make sure it does a good job

[Eric Wieser]

Mario Carneiro said:

Does that work with separate assumptions f : Nat -> Nat and Injective f?

Yes

[Eric Wieser]

Though it probably only works if the binders are adjacent

[David Thrane Christiansen]

SlimCheck could also use a new RNG, like SplitMix - IIRC it uses the one from the old Haskell prelude, which has poor statistical properties

[Eric Wieser]

On the subject of slimcheck; it would be great if someone could review lean4#3090, which leads to minor improvements in the #sample command