自动派生SBV中记录上的谓词的可证明性

Question

我所处的情况是，我有一个数据类型，比如

data X = X {foo :: SInteger, bar :: SInteger}

我想证明，例如

forAll_ $ \x -> foo x + bar x .== bar x + foo x

使用haskell的sbv。这不能编译，因为X -> SBool不是可证明的实例。我可以让它成为一个实例，例如

instance (Provable p) => Provable (X -> p) where
  forAll_ k = forAll_ $ \foo bar -> forAll_ $ k $ X foo bar
  forAll (s : ss) k =
    forAll ["foo " ++ s, "bar " ++ s] $ \foo bar -> forAll ss $ k $ X foo bar
  forAll [] k = forAll_ k
  -- and similarly `forSome_` and `forSome`

但这很繁琐且容易出错(例如，在应该使用forAll的情况下使用forSome )。有没有办法自动为我的类型派生Provable？

Answer 1

它至少可以减少出错的可能性：

onX :: (((SInteger, SInteger) -> a) -> b) -> ((X -> a) -> b)
onX f g = f (g . uncurry X)

instance Provable p => Provable (X -> p) where
    forAll_  = onX forAll_
    forSome_ = onX forSome_
    forAll   = onX . forAll
    forSome  = onX . forSome

还有一个可泛化的模式，以防SBV现有的最多7元组的实例是不够的。

data Y = Y {a, b, c, d, e, f, g, h, i, j :: SInteger}
-- don't try to write the types of these, you will wear out your keyboard
fmap10 = fmap . fmap . fmap . fmap . fmap . fmap . fmap . fmap . fmap . fmap
onY f g = f (fmap10 g Y)

instance Provable p => Provable (Y -> p) where
    forAll_  = onY forAll_
    forSome_ = onY forSome_
    forAll   = onY . forAll
    forSome  = onY . forSome

不过，还是很单调乏味。

Answer 2

如果你真的想在lambda表达式中直接使用量词，Daniel的回答是“尽善尽美”。但是，我强烈建议为您的类型定义一个free变体，而不是创建一个Provable实例：

freeX :: Symbolic X
freeX = do f <- free_
           b <- free_
           return $ X f b

现在您可以像这样使用它：

test = prove $ do x <- freeX
                  return $ foo x + bar x .== bar x + foo x

这更容易使用，并且与约束很好地结合在一起。例如，如果您的数据类型具有两个组件都为正的额外约束，并且第一个组件大于第二个组件，则可以这样编写freeX：

freeX :: Symbolic X
freeX = do f <- free_
           b <- free_
           constrain $ f .> b
           constrain $ b .> 0
           return $ X f b

请注意，这将在prove和sat上下文中正常工作，因为free知道如何在每种情况下正确运行。

我认为这更具可读性，也更易于使用，尽管它会迫使您使用do-notation。您还可以创建一个接受名称的版本，如下所示：

freeX :: String -> Symbolic X
freeX nm = do f <- free $ nm ++ "_foo"
              b <- free $ nm ++ "_bar"
              constrain $ f .> b
              constrain $ b .> 0
              return $ X f b

test = prove $ do x <- freeX "x"
                  return $ foo x + bar x .== bar x * foo x

现在我们得到：

*Main> test
Falsifiable. Counter-example:
  x_foo = 3 :: Integer
  x_bar = 1 :: Integer

您还可以通过SBV使X“可解析”。在本例中，完整代码如下所示：

data X = X {foo :: SInteger, bar :: SInteger} deriving Show

freeX :: Symbolic X
freeX = do f <- free_
           b <- free_
           return $ X f b

instance SatModel X where
  parseCWs xs = do (x, ys) <- parseCWs xs
                   (y, zs) <- parseCWs ys
                   return $ (X (literal x) (literal y), zs)

下面的测试演示了：

test :: IO (Maybe X)
test = extractModel `fmap` (prove $ do
                x <- freeX
                return $ foo x + bar x .== bar x * foo x)

我们有：

*Main> test >>= print
Just (X {foo = -4 :: SInteger, bar = -5 :: SInteger})

现在，您可以采用反例，并根据需要对其进行后处理。