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