1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
|
-----------------------------------------------------------------------------
-- |
-- 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 = 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
|
