sbv-9.1: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellSafe-Inferred
LanguageHaskell2010

Documentation.SBV.Examples.Puzzles.Drinker

Description

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.

Synopsis

Documentation

data P Source #

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

Instances

Instances details
Data P Source # 
Instance details

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 Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Drinker

Show P Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Drinker

Methods

showsPrec :: Int -> P -> ShowS #

show :: P -> String #

showList :: [P] -> ShowS #

SymVal P Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Drinker

HasKind P Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Drinker

SatModel P Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Drinker

Methods

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

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

type SP = SBV P Source #

Symbolic version of the type P.

d :: SP -> SBool Source #

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

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

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

>>> drinker2
Q.E.D.