    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Puzzles.Rabbits
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- A puzzle, attributed to Lewis Caroll:
    --
    --   - All rabbits, that are not greedy, are black
    --   - No old rabbits are free from greediness
    --   - Therefore: Some black rabbits are not old
    --
    -- What's implicit here is that there is a rabbit that must be not-greedy;
    -- which we add to our constraints.
    -----------------------------------------------------------------------------
    {-# LANGUAGE DeriveAnyClass     #-}
    {-# LANGUAGE DeriveDataTypeable #-}
    {-# LANGUAGE StandaloneDeriving #-}
    {-# LANGUAGE TemplateHaskell    #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Puzzles.Rabbits where

    import Data.SBV

    -- | A universe of rabbits
    data Rabbit

    -- | Make rabbits symbolically available.
    mkUninterpretedSort ''Rabbit

    -- | Identify those rabbits that are greedy. Note that we leave the predicate uninterpreted.
    greedy :: SRabbit -> SBool
    greedy :: SRabbit -> SBool
    greedy = String -> SRabbit -> SBool
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "greedy"

    -- | Identify those rabbits that are black. Note that we leave the predicate uninterpreted.
    black :: SRabbit -> SBool
    black :: SRabbit -> SBool
    black = String -> SRabbit -> SBool
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "black"

    -- | Identify those rabbits that are old. Note that we leave the predicate uninterpreted.
    old :: SRabbit -> SBool
    old :: SRabbit -> SBool
    old = String -> SRabbit -> SBool
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "old"

    -- | Express the puzzle.
    rabbits :: Predicate
    rabbits :: Predicate
    rabbits = do -- All rabbits that are not greedy are black
                 (Forall Any Rabbit -> SBool) -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain ((Forall Any Rabbit -> SBool) -> SymbolicT IO ())
    -> (Forall Any Rabbit -> SBool) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \(Forall SRabbit
    x) -> SBool -> SBool
    sNot (SRabbit -> SBool
    greedy SRabbit
    x) SBool -> SBool -> SBool
    .=> SRabbit -> SBool
    black  SRabbit
    x

                 -- No old rabbits are free from greediness
                 (Forall Any Rabbit -> SBool) -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain ((Forall Any Rabbit -> SBool) -> SymbolicT IO ())
    -> (Forall Any Rabbit -> SBool) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \(Forall SRabbit
    x) -> SRabbit -> SBool
    old SRabbit
    x SBool -> SBool -> SBool
    .=> SRabbit -> SBool
    greedy SRabbit
    x

                 -- There is at least one non-greedy rabbit
                 (Exists Any Rabbit -> SBool) -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain ((Exists Any Rabbit -> SBool) -> SymbolicT IO ())
    -> (Exists Any Rabbit -> SBool) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \(Exists SRabbit
    x) -> SBool -> SBool
    sNot (SRabbit -> SBool
    greedy SRabbit
    x)

                 -- Therefore, there must be a black rabbit that's not old:
                 SBool -> Predicate
    forall a. a -> SymbolicT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SBool -> Predicate) -> SBool -> Predicate
    forall a b. (a -> b) -> a -> b
    $ (Exists Any Rabbit -> SBool) -> SBool
    forall a. QuantifiedBool a => a -> SBool
    quantifiedBool ((Exists Any Rabbit -> SBool) -> SBool)
    -> (Exists Any Rabbit -> SBool) -> SBool
    forall a b. (a -> b) -> a -> b
    $ \(Exists SRabbit
    x) -> SRabbit -> SBool
    black SRabbit
    x SBool -> SBool -> SBool
    .&& SBool -> SBool
    sNot (SRabbit -> SBool
    old SRabbit
    x)

    -- | Prove the claim. We have:
    --
    -- >>> rabbitsAreOK
    -- Q.E.D.
    rabbitsAreOK :: IO ThmResult
    rabbitsAreOK :: IO ThmResult
    rabbitsAreOK = Predicate -> IO ThmResult
    forall a. Provable a => a -> IO ThmResult
    prove Predicate
    rabbits