content: -----------------------------------------------------------------------------
  -- |
  -- 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 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.
  mkSymbolic [''Rabbit]
  
  -- | Identify those rabbits that are greedy. Note that we leave the predicate uninterpreted.
  greedy :: SRabbit -> SBool
  greedy = uninterpret "greedy"
  
  -- | Identify those rabbits that are black. Note that we leave the predicate uninterpreted.
  black :: SRabbit -> SBool
  black = uninterpret "black"
  
  -- | Identify those rabbits that are old. Note that we leave the predicate uninterpreted.
  old :: SRabbit -> SBool
  old = uninterpret "old"
  
  -- | Express the puzzle.
  rabbits :: Predicate
  rabbits = do -- All rabbits that are not greedy are black
               constrain $ \(Forall x) -> sNot (greedy x) .=> black  x
  
               -- No old rabbits are free from greediness
               constrain $ \(Forall x) -> old x .=> greedy x
  
               -- There is at least one non-greedy rabbit
               constrain $ \(Exists x) -> sNot (greedy x)
  
               -- Therefore, there must be a black rabbit that's not old:
               pure $ quantifiedBool $ \(Exists x) -> black x .&& sNot (old x)
  
  -- | Prove the claim. We have:
  --
  -- >>> rabbitsAreOK
  -- Q.E.D.
  rabbitsAreOK :: IO ThmResult
  rabbitsAreOK = prove rabbits
  