-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Puzzles.Drinker
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- 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.
-----------------------------------------------------------------------------

{-# LANGUAGE DeriveAnyClass     #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell    #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Puzzles.Drinker where

import Data.SBV

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

-- | Make 'P' an uninterpreted sort, introducing the type 'SP' for its symbolic version
mkUninterpretedSort ''P

-- | 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.)
d :: SP -> SBool
d :: SBV P -> SBool
d = String -> SBV P -> SBool
forall a. Uninterpreted a => String -> a
uninterpret String
"D"

-- | Monadic formulation. In this style, we use the 'sbvExists' and 'sbvForall' constructs to create
-- our quantified variables. We have:
--
-- >>> drinker1
-- Q.E.D.
drinker1 :: IO ThmResult
drinker1 :: IO ThmResult
drinker1 = SymbolicT IO SBool -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (SymbolicT IO SBool -> IO ThmResult)
-> SymbolicT IO SBool -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ do SBV P
x <- String -> Symbolic (SBV P)
forall a. SymVal a => String -> Symbolic (SBV a)
sbvExists String
"x"
                      SBV P
y <- String -> Symbolic (SBV P)
forall a. SymVal a => String -> Symbolic (SBV a)
sbvForall String
"y"

                      SBool -> SymbolicT IO SBool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SBV P -> SBool
d SBV P
x SBool -> SBool -> SBool
.=> SBV P -> SBool
d SBV P
y

-- | Expression level formulation. In this style, we use the 'existential' and 'universal' functions instead.
-- We have:
--
-- >>> drinker2
-- Q.E.D.
drinker2 :: IO ThmResult
drinker2 :: IO ThmResult
drinker2 = SymbolicT IO SBool -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (SymbolicT IO SBool -> IO ThmResult)
-> SymbolicT IO SBool -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ [String] -> (SBV P -> SymbolicT IO SBool) -> SymbolicT IO SBool
forall a. Provable a => [String] -> a -> SymbolicT IO SBool
existential [String
"x"] ((SBV P -> SymbolicT IO SBool) -> SymbolicT IO SBool)
-> (SBV P -> SymbolicT IO SBool) -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ \SBV P
x ->
                     [String] -> (SBV P -> SBool) -> SymbolicT IO SBool
forall a. Provable a => [String] -> a -> SymbolicT IO SBool
universal [String
"y"] ((SBV P -> SBool) -> SymbolicT IO SBool)
-> (SBV P -> SBool) -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ \SBV P
y ->
                        SBV P -> SBool
d SBV P
x SBool -> SBool -> SBool
.=> SBV P -> SBool
d SBV P
y