-----------------------------------------------------------------------------
-- |
-- Module      :  Data.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>
-----------------------------------------------------------------------------

module Data.SBV.Examples.Uninterpreted.Shannon where

import Data.SBV

-----------------------------------------------------------------------------
-- * 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 f = f true

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

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

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

-- | Alternative form of Shannon's expansion over the first argument of a function. We have:
--
-- >>> shannon2
-- Q.E.D.
shannon2 :: IO ThmResult
shannon2 = prove $ \x y z -> f x y z .== ((x ||| neg f y z) &&& (bnot x ||| pos f y z))
 where f :: Ternary
       f = uninterpret "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 f y z = pos f y z <+> neg f y 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 = prove $ \y z -> bnot (f' y z) <=> pos f y z .== neg f y z
  where f :: Ternary
        f  = uninterpret "f"
        f' = derivative 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 f y z = pos f y z &&& neg f y 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 = prove $ \y z -> f' y z ==> pos f y z &&& neg f y z
  where f :: Ternary
        f  = uninterpret "f"
        f' = universal 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 f y z = pos f y z ||| neg f y 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 = prove $ \y z -> f' y z ==> pos f y z ||| neg f y z
  where f :: Ternary
        f  = uninterpret "f"
        f' = existential f