Randomized testing

Stream: new members

[Guilherme Espada]

Is there a way to (via randomized testing) check if a given lemma doesn't hold? This would be useful, for example, so I don't try to prove something that is unprovable.

[Kevin Buzzard]

tactic#slimcheck

[Kevin Buzzard]

hmm, apparently that's not a thing? There's definitely a tactic which does this.

[Guilherme Espada]

I was thinking of something similar to quickcheck yeah, but googling didn't yield much

[Anne Baanen]

You mean tactic#slim_check. A mistake I make often as well :)

[Anne Baanen]

Hmm, it has no tactic docs, so please see docs#tactic.interactive.slim_check instead.

[Yakov Pechersky]

But using it might be a little involved if you have to write sampleable instances for your types. It's not too difficult though. I'd suggest reading the slim_check and sampleable source.

[Guilherme Espada]

Exactly what I was looking for. Was hoping for automatic sampleable generation, but you can't have your cake and eat it too. Thanks!

[Yakov Pechersky]

Do you want to share your work case? In general, the tools to build a sampleable instance are pretty straightforward, and I'd be happy to contribute to making them easier.

[Yakov Pechersky]

There are already a ton of instances for your usual assortment of types and "type combinators"

[Guilherme Espada]

Sure: I have these inductive datatypes:

@[derive decidable_eq]
inductive ttype
| ty_func (l r:ttype): ttype
| ty_bool : ttype

@[derive decidable_eq]
inductive term
|t_var (idx:nat) : term
|t_abs (T:ttype) (t:term) : term
|t_app (t1 t2: term) : term
|t_true : term
|t_false : term
|t_if (cond l r: term): term

It seems to me that generating sampleable for trees like these could be fairly automated, even if the generated sampler might be somewhat inefficient or biased.

[Alex J. Best]

Making a derive handler for sampleable seems like the thing you want right?