Is there a "there exists" quantifier in QuickCheck?

Question

There is the forAll quantifier that returns a property which checks if all test cases pass. Is there a way to define a "there exists" quantifier that returns a property which checks it at least one test case passes?

Answer 1

Testing existence by enumeration would be more reliable: SmallCheck, LeanCheck, FEAT.

If you must use random generation there are some indirect ways in QuickCheck.

---

expectFailure seems like a good candidate for negation. However it isn't quite it, as it isn't involutive so you must negate the property in other ways, like not, if your property is in fact boolean.

exists :: Gen a -> (a -> Bool) -> Property
exists gen prop = once $ expectFailure (forAll gen (not . prop))

This counts crashing as a failure though, which thus makes the test pass even though you might not expect it.

---

Existential quantification is kind of a disjunction, and QuickCheck has disjoin. Just make a huge enough disjunction.

exists :: Gen a -> (a -> Property) -> Property
exists gen prop = once $ disjoin $ replicate 10000 $ forAll gen prop

But you get spammed with counterexamples when no good example is found. Maybe it is better to rewrite the logic of forAll yourself to avoid the call to counterexample.

---

More simply you can always write your own property as a generator to get the proper quantification.

exists :: Gen a -> (a -> Bool) -> Property
exists gen prop = property (exists' 1000 gen prop)

exists' :: Int -> Gen a -> (a -> Bool) -> Gen Bool
exists' 0 _ _ = return False
exists' n gen prop = do
  a <- gen
  if prop a
    then return True
    else exists' (n - 1) gen prop

Doing this manually also has the property that if prop unexpectedly crashes, it is immediately reported as a failure, as opposed to the previous methods.

---

EDIT

So if you only have a (a -> Property) instead of (a -> Bool) it seems much trickier to achieve a good result, because it's non-trivial to check whether a property succeeded. A proper way would be to mess with the internals of QuickCheck, probably something similar to disjoin. Here is a quick hack

• Use mapResult to silence the output of disjoin when no (counter)example was found.

• Override the size parameter because if your witnesses are non-trivial, they will not be found if the size is too small or too large.

import Test.QuickCheck
import Test.QuickCheck.Property as P

-- Retry n times.
exists :: Testable prop => Int -> Gen a -> (a -> prop) -> Property
exists n gen prop =
  mapResult (\r -> r {P.reason = "No witness found.", P.callbacks = []}) $
  once $
  disjoin $
  replicate n $ do
    a <- gen
    return (prop a)

main = quickCheck $ exists 100
  (resize 5 arbitrary)
  (\x -> (x :: Integer) == 2)

Answer 2

I don't know if something like this exist in QuickCheck. Also not convinced it would be helpful, but that's another matter. Since we have:

∃ x . P x <=> ¬ ¬ ∃ x . P x <=> ¬ ∀ x . ¬ P x

I suppose you could set it up so your test-case tests the negation and if it fails it means you have your existential. HTH.