Documentation.SBV.Examples.Puzzles.Drinker

SBV proof of the drinker paradox: http://en.wikipedia.org/wiki/Drinker_paradox

Let P be the non-empty set of people in a bar. The theorem says if there is somebody drinking in the bar, then everybody is drinking in the bar. The general formulation is:

    ∃x : P. D(x) -> ∀y : P. D(y)

In SBV, quantifiers are allowed, but you need to put the formula into prenex normal form manually. See http://en.wikipedia.org/wiki/Prenex_normal_form for details. (Note that you do not need to do skolemization by hand, though SBV will do that for you automatically as well as it casts the problem into an SMT query.) If we transform the above to prenex form, we get:

    ∃x : P. ∀y : P. D(x) -> D(y)

In this file, we show two different ways of proving the above in SBV; one using the monadic style, and the other using the expression style.

Documentation

data P

Declare a carrier data-type in Haskell named P, representing all the people in a bar.

Instances

Data P

Defined in Documentation.SBV.Examples.Puzzles.Drinker

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> P -> c P

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c P

toConstr :: P -> Constr

dataTypeOf :: P -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c P)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c P)

gmapT :: (forall b. Data b => b -> b) -> P -> P

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> P -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> P -> r

gmapQ :: (forall d. Data d => d -> u) -> P -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> P -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> P -> m P

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> P -> m P

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> P -> m P

Read P

Defined in Documentation.SBV.Examples.Puzzles.Drinker

Methods

readsPrec :: Int -> ReadS P

readList :: ReadS [P]

readPrec :: ReadPrec P

readListPrec :: ReadPrec [P]

Show P

Defined in Documentation.SBV.Examples.Puzzles.Drinker

Methods

showsPrec :: Int -> P -> ShowS

show :: P -> String

showList :: [P] -> ShowS

HasKind P

Defined in Documentation.SBV.Examples.Puzzles.Drinker

Methods

kindOf :: P -> Kind

hasSign :: P -> Bool

intSizeOf :: P -> Int

isBoolean :: P -> Bool

isBounded :: P -> Bool

isReal :: P -> Bool

isFloat :: P -> Bool

isDouble :: P -> Bool

isRational :: P -> Bool

isFP :: P -> Bool

isUnbounded :: P -> Bool

isUserSort :: P -> Bool

isChar :: P -> Bool

isString :: P -> Bool

isList :: P -> Bool

isSet :: P -> Bool

isTuple :: P -> Bool

isMaybe :: P -> Bool

isEither :: P -> Bool

showType :: P -> String

SymVal P

Defined in Documentation.SBV.Examples.Puzzles.Drinker

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV P)

literal :: P -> SBV P

fromCV :: CV -> P

isConcretely :: SBV P -> (P -> Bool) -> Bool

sbvForall :: MonadSymbolic m => String -> m (SBV P)

sbvForall_ :: MonadSymbolic m => m (SBV P)

mkForallVars :: MonadSymbolic m => Int -> m [SBV P]

sbvExists :: MonadSymbolic m => String -> m (SBV P)

sbvExists_ :: MonadSymbolic m => m (SBV P)

mkExistVars :: MonadSymbolic m => Int -> m [SBV P]

free :: MonadSymbolic m => String -> m (SBV P)

free_ :: MonadSymbolic m => m (SBV P)

mkFreeVars :: MonadSymbolic m => Int -> m [SBV P]

symbolic :: MonadSymbolic m => String -> m (SBV P)

symbolics :: MonadSymbolic m => [String] -> m [SBV P]

unliteral :: SBV P -> Maybe P

isConcrete :: SBV P -> Bool

isSymbolic :: SBV P -> Bool

SatModel P

Defined in Documentation.SBV.Examples.Puzzles.Drinker

Methods

parseCVs :: [CV] -> Maybe (P, [CV])

cvtModel :: (P -> Maybe b) -> Maybe (P, [CV]) -> Maybe (b, [CV])

type SP = SBV P

Make P an uninterpreted sort, introducing the type SP for its symbolic version

d :: SP -> SBool

Declare the uninterpret function d, standing for drinking. For each person, this function assigns whether they are drinking; but is otherwise completely uninterpreted. (i.e., our theorem will be true for all such functions.)

drinker1 :: IO ThmResult

Monadic formulation. In this style, we use the sbvExists and sbvForall constructs to create our quantified variables. We have:

>>> drinker1
Q.E.D.

drinker2 :: IO ThmResult

Expression level formulation. In this style, we use the existential and universal functions instead. We have:

>>> drinker2
Q.E.D.