slimcheck with definitions that contain quantifiers

Stream: new members

[Mark Aagaard]

I'm playing around with SlimCheck to learn how best to use it. Is SlimCheck able to generate tests for definitions that contain quantifiers over Nats? I am able to do Testable.check for expressions that contain quantifiers, but when I put the expression inside a definition, I get a "failed to synthesize Testable" error.

Is there a way to use Testable.check on definitions that contain quantifiers?

Here's a small example:

import Mathlib.Tactic
open SlimCheck

def q (n:ℕ) : Bool := n > 3

#eval Testable.check (∀ (n:ℕ), q n) -- this works and gives a counterexample

def q2 := ∀ (n:ℕ), n > 3 -- now put the quantifier inside the def

#eval Testable.check q2 -- fails with "failed to synthesize Testable q2"

-mark

[Henrik Böving]

You need to make the definition an abbrev or define the testable instance yourself. That's just a consequence of how TC synthesis works

[Ruben Van de Velde]

Please also check #backticks

[Mark Aagaard]

Changing from def to abbrev didn't help. I'm still getting failed to synthesize Testable q2. Do I need to define a testable instance of q2? Is the best resource for this:

https://github.com/argumentcomputer/LSpec/blob/main/LSpec/Instances.lean

-mark

[Henrik Böving]

Ah I guess this is a bit unlucky because of the way that slim_check works internally with binders

[Henrik Böving]

I'd guess you have to define the instance yourself at this point rather unfortunately mhm

[Henrik Böving]

But this should be fixable in plausible