sTrue is provable.

We have:

>>> trueIsProvable
Lemma: true                             Q.E.D.
[Proven] true

sFalse isn't provable.

We have:

>>> falseIsn'tProvable `catch` (\(_ :: SomeException) -> pure ())
Lemma: sFalse
*** Failed to prove sFalse.
Falsifiable

Basic quantification example: For every integer, there's a larger integer.

We have: >>> largerIntegerExists Lemma: largerIntegerExists Q.E.D. [Proven] largerIntegerExists

Use an uninterpreted type for the domain

Symbolic version of the type T.

Pushing a universal through conjunction. We have:

>>> forallConjunction
Lemma: forallConjunction                Q.E.D.
[Proven] forallConjunction

Pushing an existential through disjunction. We have:

>>> existsDisjunction
Lemma: existsDisjunction                Q.E.D.
[Proven] existsDisjunction

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

>>> forallDisjunctionNot `catch` (\(_ :: SomeException) -> pure ())
Lemma: forallConjunctionNot
*** Failed to prove forallConjunctionNot.
Falsifiable. Counter-example:
  p :: T -> Bool
  p T_2 = True
  p T_0 = True
  p _   = False

  q :: T -> Bool
  q T_2 = False
  q T_0 = False
  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.)

We cannot push an existential through conjunction. We have:

>>> existsConjunctionNot `catch` (\(_ :: SomeException) -> pure ())
Lemma: existsConjunctionNot
*** Failed to prove existsConjunctionNot.
Falsifiable. Counter-example:
  p :: T -> Bool
  p T_1 = False
  p _   = True

  q :: T -> Bool
  q T_1 = True
  q _   = False

In this case, we again have a predicate That disagree at every point, providing a counter-example.

It's important to realize that KnuckleDragger proofs in SBV neither check nor guarantee that the functions we use are terminating. This is beyond the scope (and current capabilities) of what SBV can handle. That is, the proof is up-to-termination, i.e., any proof implicitly assumes all functions defined (or axiomatized) terminate for all possible inputs. If non-termination is possible, then the logic becomes inconsistent, i.e., we can prove arbitrary results.

Here is a simple example where we tell SBV that there is a function f with non terminating behavior. Using this, we can deduce False:

>>> noTerminationChecks
Axiom: bad
Lemma: noTerminationImpliesFalse
  Step: 1 (bad @ (n |-> 0 :: SInteger)) Q.E.D.
  Result:                               Q.E.D.
[Proven] noTerminationImpliesFalse