forAll package:sbv

A universal symbolic variable, used in building quantified constraints. The name attached via the symbol is used during skolemization. It names the corresponding argument to the skolem-functions within the scope of this quantifier.

Pushing a universal through conjunction. We have:

>>> forallConjunction @Integer (uninterpret "p") (uninterpret "q")
Lemma: forallConjunction                Q.E.D.
[Proven] forallConjunction :: Bool

We cannot push a universal through a disjunction. We have:

>>> forallDisjunctionNot @Integer (uninterpret "p") (uninterpret "q") `catch` (\(_ :: SomeException) -> pure ())
Lemma: forallConjunctionNot
*** Failed to prove forallConjunctionNot.
Falsifiable. Counter-example:
p :: Integer -> Bool
p 2 = True
p 1 = False
p _ = True

q :: Integer -> Bool
q 2 = False
q 1 = True
q _ = True

Note how p assigns two selected values to True and everything else to False, while q does the exact opposite. So, there is no common value that satisfies both, providing a counter-example. (It's not clear why the solver finds a model with two distinct values, as one would have sufficed. But it is still a valud model.)

Exactly n universal symbolic variables, used in in building quantified constraints. The name attached will be prefixed in front of _1, _2, ..., _n to form the names of the variables.