-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Uninterpreted.Shannon
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Proves (instances of) Shannon's expansion theorem and other relevant
-- facts.  See: <http://en.wikipedia.org/wiki/Shannon's_expansion>
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Uninterpreted.Shannon where

import Data.SBV hiding (universal, existential)

-----------------------------------------------------------------------------
-- * Boolean functions
-----------------------------------------------------------------------------

-- | A ternary boolean function
type Ternary = SBool -> SBool -> SBool -> SBool

-- | A binary boolean function
type Binary = SBool -> SBool-> SBool

-----------------------------------------------------------------------------
-- * Shannon cofactors
-----------------------------------------------------------------------------

-- | Positive Shannon cofactor of a boolean function, with
-- respect to its first argument
pos :: (SBool -> a) -> a
pos :: (SBool -> a) -> a
pos SBool -> a
f = SBool -> a
f SBool
sTrue

-- | Negative Shannon cofactor of a boolean function, with
-- respect to its first argument
neg :: (SBool -> a) -> a
neg :: (SBool -> a) -> a
neg SBool -> a
f = SBool -> a
f SBool
sFalse

-----------------------------------------------------------------------------
-- * Shannon expansion theorem
-----------------------------------------------------------------------------

-- | Shannon's expansion over the first argument of a function. We have:
--
-- >>> shannon
-- Q.E.D.
shannon :: IO ThmResult
shannon :: IO ThmResult
shannon = (SBool -> SBool -> SBool -> SBool) -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove ((SBool -> SBool -> SBool -> SBool) -> IO ThmResult)
-> (SBool -> SBool -> SBool -> SBool) -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ \SBool
x SBool
y SBool
z -> SBool -> SBool -> SBool -> SBool
f SBool
x SBool
y SBool
z SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBool
x SBool -> SBool -> SBool
.&& (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
pos SBool -> SBool -> SBool -> SBool
f SBool
y SBool
z SBool -> SBool -> SBool
.|| SBool -> SBool
sNot SBool
x SBool -> SBool -> SBool
.&& (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
neg SBool -> SBool -> SBool -> SBool
f SBool
y SBool
z)
 where f :: Ternary
       f :: SBool -> SBool -> SBool -> SBool
f = String -> SBool -> SBool -> SBool -> SBool
forall a. Uninterpreted a => String -> a
uninterpret String
"f"

-- | Alternative form of Shannon's expansion over the first argument of a function. We have:
--
-- >>> shannon2
-- Q.E.D.
shannon2 :: IO ThmResult
shannon2 :: IO ThmResult
shannon2 = (SBool -> SBool -> SBool -> SBool) -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove ((SBool -> SBool -> SBool -> SBool) -> IO ThmResult)
-> (SBool -> SBool -> SBool -> SBool) -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ \SBool
x SBool
y SBool
z -> SBool -> SBool -> SBool -> SBool
f SBool
x SBool
y SBool
z SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== ((SBool
x SBool -> SBool -> SBool
.|| (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
neg SBool -> SBool -> SBool -> SBool
f SBool
y SBool
z) SBool -> SBool -> SBool
.&& (SBool -> SBool
sNot SBool
x SBool -> SBool -> SBool
.|| (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
pos SBool -> SBool -> SBool -> SBool
f SBool
y SBool
z))
 where f :: Ternary
       f :: SBool -> SBool -> SBool -> SBool
f = String -> SBool -> SBool -> SBool -> SBool
forall a. Uninterpreted a => String -> a
uninterpret String
"f"

-----------------------------------------------------------------------------
-- * Derivatives
-----------------------------------------------------------------------------

-- | Computing the derivative of a boolean function (boolean difference).
-- Defined as exclusive-or of Shannon cofactors with respect to that
-- variable.
derivative :: Ternary -> Binary
derivative :: (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
derivative SBool -> SBool -> SBool -> SBool
f SBool
y SBool
z = (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
pos SBool -> SBool -> SBool -> SBool
f SBool
y SBool
z SBool -> SBool -> SBool
.<+> (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
neg SBool -> SBool -> SBool -> SBool
f SBool
y SBool
z

-- | The no-wiggle theorem: If the derivative of a function with respect to
-- a variable is constant False, then that variable does not "wiggle" the
-- function; i.e., any changes to it won't affect the result of the function.
-- In fact, we have an equivalence: The variable only changes the
-- result of the function iff the derivative with respect to it is not False:
--
-- >>> noWiggle
-- Q.E.D.
noWiggle :: IO ThmResult
noWiggle :: IO ThmResult
noWiggle = (SBool -> SBool -> SBool) -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove ((SBool -> SBool -> SBool) -> IO ThmResult)
-> (SBool -> SBool -> SBool) -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ \SBool
y SBool
z -> SBool -> SBool
sNot (SBool -> SBool -> SBool
f' SBool
y SBool
z) SBool -> SBool -> SBool
.<=> (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
pos SBool -> SBool -> SBool -> SBool
f SBool
y SBool
z SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
neg SBool -> SBool -> SBool -> SBool
f SBool
y SBool
z
  where f :: Ternary
        f :: SBool -> SBool -> SBool -> SBool
f  = String -> SBool -> SBool -> SBool -> SBool
forall a. Uninterpreted a => String -> a
uninterpret String
"f"
        f' :: SBool -> SBool -> SBool
f' = (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
derivative SBool -> SBool -> SBool -> SBool
f

-----------------------------------------------------------------------------
-- * Universal quantification
-----------------------------------------------------------------------------

-- | Universal quantification of a boolean function with respect to a variable.
-- Simply defined as the conjunction of the Shannon cofactors.
universal :: Ternary -> Binary
universal :: (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
universal SBool -> SBool -> SBool -> SBool
f SBool
y SBool
z = (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
pos SBool -> SBool -> SBool -> SBool
f SBool
y SBool
z SBool -> SBool -> SBool
.&& (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
neg SBool -> SBool -> SBool -> SBool
f SBool
y SBool
z

-- | Show that universal quantification is really meaningful: That is, if the universal
-- quantification with respect to a variable is True, then both cofactors are true for
-- those arguments. Of course, this is a trivial theorem if you think about it for a
-- moment, or you can just let SBV prove it for you:
--
-- >>> univOK
-- Q.E.D.
univOK :: IO ThmResult
univOK :: IO ThmResult
univOK = (SBool -> SBool -> SBool) -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove ((SBool -> SBool -> SBool) -> IO ThmResult)
-> (SBool -> SBool -> SBool) -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ \SBool
y SBool
z -> SBool -> SBool -> SBool
f' SBool
y SBool
z SBool -> SBool -> SBool
.=> (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
pos SBool -> SBool -> SBool -> SBool
f SBool
y SBool
z SBool -> SBool -> SBool
.&& (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
neg SBool -> SBool -> SBool -> SBool
f SBool
y SBool
z
  where f :: Ternary
        f :: SBool -> SBool -> SBool -> SBool
f  = String -> SBool -> SBool -> SBool -> SBool
forall a. Uninterpreted a => String -> a
uninterpret String
"f"
        f' :: SBool -> SBool -> SBool
f' = (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
universal SBool -> SBool -> SBool -> SBool
f

-----------------------------------------------------------------------------
-- * Existential quantification
-----------------------------------------------------------------------------

-- | Existential quantification of a boolean function with respect to a variable.
-- Simply defined as the conjunction of the Shannon cofactors.
existential :: Ternary -> Binary
existential :: (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
existential SBool -> SBool -> SBool -> SBool
f SBool
y SBool
z = (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
pos SBool -> SBool -> SBool -> SBool
f SBool
y SBool
z SBool -> SBool -> SBool
.|| (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
neg SBool -> SBool -> SBool -> SBool
f SBool
y SBool
z

-- | Show that existential quantification is really meaningful: That is, if the existential
-- quantification with respect to a variable is True, then one of the cofactors must be true for
-- those arguments. Again, this is a trivial theorem if you think about it for a moment, but
-- we will just let SBV prove it:
--
-- >>> existsOK
-- Q.E.D.
existsOK :: IO ThmResult
existsOK :: IO ThmResult
existsOK = (SBool -> SBool -> SBool) -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove ((SBool -> SBool -> SBool) -> IO ThmResult)
-> (SBool -> SBool -> SBool) -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ \SBool
y SBool
z -> SBool -> SBool -> SBool
f' SBool
y SBool
z SBool -> SBool -> SBool
.=> (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
pos SBool -> SBool -> SBool -> SBool
f SBool
y SBool
z SBool -> SBool -> SBool
.|| (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
neg SBool -> SBool -> SBool -> SBool
f SBool
y SBool
z
  where f :: Ternary
        f :: SBool -> SBool -> SBool -> SBool
f  = String -> SBool -> SBool -> SBool -> SBool
forall a. Uninterpreted a => String -> a
uninterpret String
"f"
        f' :: SBool -> SBool -> SBool
f' = (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
existential SBool -> SBool -> SBool -> SBool
f