    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Uninterpreted.Deduce
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Demonstrates uninterpreted sorts and how they can be used for deduction.
    -- This example is inspired by the discussion at <http://stackoverflow.com/questions/10635783/using-axioms-for-deductions-in-z3>,
    -- essentially showing how to show the required deduction using SBV.
    -----------------------------------------------------------------------------

    {-# LANGUAGE DeriveAnyClass     #-}
    {-# LANGUAGE DeriveDataTypeable #-}
    {-# LANGUAGE StandaloneDeriving #-}
    {-# LANGUAGE TemplateHaskell    #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Uninterpreted.Deduce where

    import Data.SBV

    -- we will have our own "uninterpreted" functions corresponding
    -- to not/or/and, so hide their Prelude counterparts.
    import Prelude hiding (not, or, and)

    -----------------------------------------------------------------------------
    -- * Representing uninterpreted booleans
    -----------------------------------------------------------------------------

    -- | The uninterpreted sort 'B', corresponding to the carrier.
    data B

    -- | Make this sort uninterpreted. This splice will automatically introduce
    -- the type 'SB' into the environment, as a synonym for 'SBV' 'B'.
    mkUninterpretedSort ''B

    -----------------------------------------------------------------------------
    -- * Uninterpreted connectives over 'B'
    -----------------------------------------------------------------------------

    -- | Uninterpreted logical connective 'and'
    and :: SB -> SB -> SB
    and :: SB -> SB -> SB
    and = String -> SB -> SB -> SB
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "AND"

    -- | Uninterpreted logical connective 'or'
    or :: SB -> SB -> SB
    or :: SB -> SB -> SB
    or  = String -> SB -> SB -> SB
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "OR"

    -- | Uninterpreted logical connective 'not'
    not :: SB -> SB
    not :: SB -> SB
    not = String -> SB -> SB
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "NOT"

    -----------------------------------------------------------------------------
    -- * Demonstrated deduction
    -----------------------------------------------------------------------------

    -- | Proves the equivalence @NOT (p OR (q AND r)) == (NOT p AND NOT q) OR (NOT p AND NOT r)@,
    -- following from the axioms we have specified above. We have:
    --
    -- >>> test
    -- Q.E.D.
    test :: IO ThmResult
    test :: IO ThmResult
    test = SymbolicT IO SBool -> IO ThmResult
    forall a. Provable a => a -> IO ThmResult
    prove (SymbolicT IO SBool -> IO ThmResult)
    -> SymbolicT IO SBool -> IO ThmResult
    forall a b. (a -> b) -> a -> b
    $ do (Forall Any B -> Forall Any B -> Forall Any B -> SBool)
    -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain ((Forall Any B -> Forall Any B -> Forall Any B -> SBool)
     -> SymbolicT IO ())
    -> (Forall Any B -> Forall Any B -> Forall Any B -> SBool)
    -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \(Forall SB
    p) (Forall SB
    q) (Forall SB
    r) -> (SB
    p SB -> SB -> SB
    `or` SB
    q) SB -> SB -> SB
    `and` (SB
    p SB -> SB -> SB
    `or` SB
    r) SB -> SB -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SB
    p SB -> SB -> SB
    `or` (SB
    q SB -> SB -> SB
    `and` SB
    r)
                      (Forall Any B -> Forall Any B -> SBool) -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain ((Forall Any B -> Forall Any B -> SBool) -> SymbolicT IO ())
    -> (Forall Any B -> Forall Any B -> SBool) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \(Forall SB
    p) (Forall SB
    q)            -> SB -> SB
    not (SB
    p SB -> SB -> SB
    `or` SB
    q) SB -> SB -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SB -> SB
    not SB
    p SB -> SB -> SB
    `and` SB -> SB
    not SB
    q
                      (Forall Any B -> SBool) -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain ((Forall Any B -> SBool) -> SymbolicT IO ())
    -> (Forall Any B -> SBool) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \(Forall SB
    p)                       -> SB -> SB
    not (SB -> SB
    not SB
    p) SB -> SB -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SB
    p
                      SB
    p <- String -> Symbolic SB
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    "p"
                      SB
    q <- String -> Symbolic SB
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    "q"
                      SB
    r <- String -> Symbolic SB
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    "r"
                      SBool -> SymbolicT IO SBool
    forall a. a -> SymbolicT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
    forall a b. (a -> b) -> a -> b
    $   SB -> SB
    not (SB
    p SB -> SB -> SB
    `or` (SB
    q SB -> SB -> SB
    `and` SB
    r))
                             SB -> SB -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== (SB -> SB
    not SB
    p SB -> SB -> SB
    `and` SB -> SB
    not SB
    q) SB -> SB -> SB
    `or` (SB -> SB
    not SB
    p SB -> SB -> SB
    `and` SB -> SB
    not SB
    r)

    -- Hlint gets confused and thinks the use of @not@ above is from the prelude. Sigh.
    {- HLint ignore test "Redundant not" -}