    -----------------------------------------------------------------------------
    -- |
    -- 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

    -----------------------------------------------------------------------------
    -- * 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 f :: 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 f :: 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
    $ \x :: SBool
    x y :: SBool
    y z :: 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 "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
    $ \x :: SBool
    x y :: SBool
    y z :: 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 "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 f :: SBool -> SBool -> SBool -> SBool
    f y :: SBool
    y z :: 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
    $ \y :: SBool
    y z :: 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 "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 f :: SBool -> SBool -> SBool -> SBool
    f y :: SBool
    y z :: 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
    $ \y :: SBool
    y z :: 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 "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 f :: SBool -> SBool -> SBool -> SBool
    f y :: SBool
    y z :: 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
    $ \y :: SBool
    y z :: 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 "f"
            f' :: SBool -> SBool -> SBool
    f' = (SBool -> SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
    existential SBool -> SBool -> SBool -> SBool
    f