Unexpected prove/forSome interaction

[kfl]

It seem that forSome is behaving strangely with respect to prove.

For instance, I'd expect the following prop1 and prop2 to be equivalent:

prop1 = sNot <$> (forSome_ $ \ (n :: SInteger) -> (n .== 0))
prop2 = (forAll_ $ \ (n :: SInteger) -> sNot(n .== 0))

However, when I try to prove them I get:

λ> prove prop1
Q.E.D.
λ> prove prop2
Falsifiable. Counter-example:
  s0 = 0 :: Integer

Why is it possible to prove prop1? The documentation doesn't seem to offer any clues.

[LeventErkok]

Unfortunately prop1 doesn't mean what you'd think it means in SBV. The sNot does not distribute over the forSome_, instead it essentially becomes:

prop1 = forSome_ $ \ (n :: SInteger) -> sNot (n .== 0)

which is, of course, a theorem. The "flipping" of the quantifier is not done, and indeed there is no way to really handle this within SBV, under the current design. (That is, a different design could've handled it; but long-ago made design choices on how quantifiers are handled in SBV does not allow for this sort of manipulation.)

So, strictly speaking this is a "usability" bug, because what looks like should be an obvious translation isn't what actually happens. Meaning: SBV as it stands will never support the kind of transformation you want, though I wish it was smart enough to detect it and reject it instead of silently going and doing the most confusing thing.

You'll also find that this is true for any sort of quantifier manipulation in SBV. It has a very limited understanding of them. In particular, it assumes all the given formulae has all the quantifiers pulled to the top (i.e., in prenex form), and also there are no "outside" operations done, i.e., you start with the quantifiers and the formula is completely done after them. (Your call to sNot wrapping around the forSome_ violates this assumption.)

While this is not something that will be fixed in SBV, I'll keep this ticket open as a "usability bug," and perhaps one day SBV will be smart enough to detect these cases and reject them properly as they are not really supported.

[LeventErkok]

@kfl

Also see #256 for a related issue.

Note that the documentation does mention this, but I'd agree that unless you know exactly what it's saying it might be hard to decipher: https://hackage.haskell.org/package/sbv-8.17/docs/Data-SBV.html#g:40, replicated below:

A note on reasoning in the presence of quantifiers

Note that SBV allows reasoning with quantifiers: Inputs can be existentially or universally quantified. Predicates can be built with arbitrary nesting of such quantifiers as well. However, SBV always assumes that the input is in prenex-normal form: http://en.wikipedia.org/wiki/Prenex_normal_form. That is, all the input declarations are treated as happening at the beginning of a predicate, followed by the actual formula. Unfortunately, the way predicates are written can be misleading at times, since symbolic inputs can be created at arbitrary points; interleaving them with other code. The rule is simple, however: All inputs are assumed at the top, in the order declared, regardless of their quantifiers. SBV will apply skolemization to get rid of existentials before sending predicates to backend solvers. However, if you do want nested quantification, you will manually have to first convert to prenex-normal form (which produces an equisatisfiable but not necessarily equivalent formula), and code that explicitly in SBV. See http://github.com/LeventErkok/sbv/issues/256 for a detailed discussion of this issue.

[kfl]

Thank you for the reply (and for SBV which is a great library).

I had just found the note on quantifiers in the documentation.

Perhaps an interim usability patch could be to link to the above mentioned note in the documentation for forSome and forAll?

[LeventErkok]

Sure.. Please file a PR and I'd be happy to merge!

[LeventErkok]

@kfl

Not sure if this is still relevant to you. But the latest release of SBV has proper support for quantifiers. The old way of dealing with quantifiers is completely removed. The current implementation (I hope!) is much easier to use and much more expressive.

For instance, your example is now coded like this:

Prelude Data.SBV> prop1 = qNot $ \(Exists n) -> n .== (0 :: SInteger)
Prelude Data.SBV> prop2 = \(Forall n) -> sNot (n .== (0 :: SInteger))
Prelude Data.SBV> prove prop1
Falsifiable
Prelude Data.SBV> prove prop2
Falsifiable

and as you'd expect, these are both not theorems.
The new facility can also do skolemization, which I suspect you might be interested in:

Prelude Data.SBV> :set -XDataKinds
Prelude Data.SBV> let q = \(Forall @"x" x) (Exists @"y" y) -> y .== (x+1::SInteger)
Prelude Data.SBV> sat q
Satisfiable
Prelude Data.SBV> sat $ skolemize q
Satisfiable. Model:
  y :: Integer -> Integer
  y x = 1 + x

There are some further examples in https://hackage.haskell.org/package/sbv-10.1/docs/Documentation-SBV-Examples-Misc-FirstOrderLogic.html

Let me know if you give this a try and have any feedback regarding usage/further examples etc.