-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.KnuckleDragger.Basics
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Some basic KD usage.
-----------------------------------------------------------------------------

{-# LANGUAGE CPP                #-}
{-# LANGUAGE DataKinds          #-}
{-# LANGUAGE DeriveAnyClass     #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE TemplateHaskell    #-}
{-# LANGUAGE TypeAbstractions   #-}
{-# LANGUAGE StandaloneDeriving #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.KnuckleDragger.Basics where

import Data.SBV
import Data.SBV.Tools.KnuckleDragger

#ifndef HADDOCK
-- $setup
-- >>> -- For doctest purposes only:
-- >>> :set -XScopedTypeVariables
-- >>> import Control.Exception
#endif

-- | @sTrue@ is provable.
--
-- We have:
--
-- >>> trueIsProvable
-- Lemma: true                             Q.E.D.
-- [Proven] true
trueIsProvable :: IO Proof
trueIsProvable :: IO Proof
trueIsProvable = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ String -> SBool -> [Proof] -> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"true" SBool
sTrue []

-- | @sFalse@ isn't provable.
--
-- We have:
--
-- >>> falseIsn'tProvable `catch` (\(_ :: SomeException) -> pure ())
-- Lemma: sFalse
-- *** Failed to prove sFalse.
-- Falsifiable
falseIsn'tProvable :: IO ()
falseIsn'tProvable :: IO ()
falseIsn'tProvable = KD () -> IO ()
forall a. KD a -> IO a
runKD (KD () -> IO ()) -> KD () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        _won'tGoThrough <- String -> SBool -> [Proof] -> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"sFalse" SBool
sFalse []
        pure ()

-- | Basic quantification example: For every integer, there's a larger integer.
--
-- We have:
-- >>> largerIntegerExists
-- Lemma: largerIntegerExists              Q.E.D.
-- [Proven] largerIntegerExists
largerIntegerExists :: IO Proof
largerIntegerExists :: IO Proof
largerIntegerExists = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ String
-> (Forall "x" Integer -> Exists "y" Integer -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"largerIntegerExists"
                                    (\(Forall @"x" SBV Integer
x) (Exists @"y" SBV Integer
y) -> SBV Integer
x SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< (SBV Integer
y :: SInteger))
                                    []

-- | Use an uninterpreted type for the domain
data T
mkUninterpretedSort ''T

-- | Pushing a universal through conjunction. We have:
--
-- >>> forallConjunction
-- Lemma: forallConjunction                Q.E.D.
-- [Proven] forallConjunction
forallConjunction :: IO Proof
forallConjunction :: IO Proof
forallConjunction = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
    let p, q :: ST -> SBool
        p :: ST -> SBool
p = String -> ST -> SBool
forall a. SMTDefinable a => String -> a
uninterpret String
"p"
        q :: ST -> SBool
q = String -> ST -> SBool
forall a. SMTDefinable a => String -> a
uninterpret String
"q"

        qb :: (Forall "x" T -> SBool) -> SBool
qb = (Forall "x" T -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool

    String -> SBool -> [Proof] -> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"forallConjunction"
           (      ((Forall "x" T -> SBool) -> SBool
qb (\(Forall @"x" ST
x) -> ST -> SBool
p ST
x) SBool -> SBool -> SBool
.&& (Forall "x" T -> SBool) -> SBool
qb (\(Forall @"x" ST
x) -> ST -> SBool
q ST
x))
            SBool -> SBool -> SBool
.<=> -----------------------------------------------------------------
                          (Forall "x" T -> SBool) -> SBool
qb (\(Forall @"x" ST
x) -> ST -> SBool
p ST
x SBool -> SBool -> SBool
.&& ST -> SBool
q ST
x)
           )
           []

-- | Pushing an existential through disjunction. We have:
--
-- >>> existsDisjunction
-- Lemma: existsDisjunction                Q.E.D.
-- [Proven] existsDisjunction
existsDisjunction :: IO Proof
existsDisjunction :: IO Proof
existsDisjunction = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
    let p, q :: ST -> SBool
        p :: ST -> SBool
p = String -> ST -> SBool
forall a. SMTDefinable a => String -> a
uninterpret String
"p"
        q :: ST -> SBool
q = String -> ST -> SBool
forall a. SMTDefinable a => String -> a
uninterpret String
"q"

        qb :: (Exists "x" T -> SBool) -> SBool
qb = (Exists "x" T -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool

    String -> SBool -> [Proof] -> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"existsDisjunction"
           (      ((Exists "x" T -> SBool) -> SBool
qb (\(Exists @"x" ST
x) -> ST -> SBool
p ST
x) SBool -> SBool -> SBool
.|| (Exists "x" T -> SBool) -> SBool
qb (\(Exists @"x" ST
x) -> ST -> SBool
q ST
x))
            SBool -> SBool -> SBool
.<=> -----------------------------------------------------------------
                          (Exists "x" T -> SBool) -> SBool
qb (\(Exists @"x" ST
x) -> ST -> SBool
p ST
x SBool -> SBool -> SBool
.|| ST -> SBool
q ST
x)
           )
           []

-- | 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
-- <BLANKLINE>
--   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.)
forallDisjunctionNot :: IO ()
forallDisjunctionNot :: IO ()
forallDisjunctionNot = KD () -> IO ()
forall a. KD a -> IO a
runKD (KD () -> IO ()) -> KD () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    let p, q :: ST -> SBool
        p :: ST -> SBool
p = String -> ST -> SBool
forall a. SMTDefinable a => String -> a
uninterpret String
"p"
        q :: ST -> SBool
q = String -> ST -> SBool
forall a. SMTDefinable a => String -> a
uninterpret String
"q"

        qb :: (Forall "x" T -> SBool) -> SBool
qb = (Forall "x" T -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool

    -- This won't prove!
    _won'tGoThrough <- String -> SBool -> [Proof] -> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"forallConjunctionNot"
                             (      ((Forall "x" T -> SBool) -> SBool
qb (\(Forall @"x" ST
x) -> ST -> SBool
p ST
x) SBool -> SBool -> SBool
.|| (Forall "x" T -> SBool) -> SBool
qb (\(Forall @"x" ST
x) -> ST -> SBool
q ST
x))
                              SBool -> SBool -> SBool
.<=> -----------------------------------------------------------------
                                              (Forall "x" T -> SBool) -> SBool
qb (\(Forall @"x" ST
x) -> ST -> SBool
p ST
x SBool -> SBool -> SBool
.|| ST -> SBool
q ST
x)
                             )
                             []

    pure ()

-- | 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
-- <BLANKLINE>
--   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.
existsConjunctionNot :: IO ()
existsConjunctionNot :: IO ()
existsConjunctionNot = KD () -> IO ()
forall a. KD a -> IO a
runKD (KD () -> IO ()) -> KD () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    let p, q :: ST -> SBool
        p :: ST -> SBool
p = String -> ST -> SBool
forall a. SMTDefinable a => String -> a
uninterpret String
"p"
        q :: ST -> SBool
q = String -> ST -> SBool
forall a. SMTDefinable a => String -> a
uninterpret String
"q"

        qb :: (Exists "x" T -> SBool) -> SBool
qb = (Exists "x" T -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool

    _wont'GoThrough <- String -> SBool -> [Proof] -> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"existsConjunctionNot"
                             (      ((Exists "x" T -> SBool) -> SBool
qb (\(Exists @"x" ST
x) -> ST -> SBool
p ST
x) SBool -> SBool -> SBool
.&& (Exists "x" T -> SBool) -> SBool
qb (\(Exists @"x" ST
x) -> ST -> SBool
q ST
x))
                              SBool -> SBool -> SBool
.<=> -----------------------------------------------------------------
                                              (Exists "x" T -> SBool) -> SBool
qb (\(Exists @"x" ST
x) -> ST -> SBool
p ST
x SBool -> SBool -> SBool
.&& ST -> SBool
q ST
x)
                             )
                            []

    pure ()