-----------------------------------------------------------------------------
-- |
-- 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 :: SP -> SBool
d = 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 = forall a. Provable a => a -> IO ThmResult
prove forall a b. (a -> b) -> a -> b
$ do SP
x <- forall a. SymVal a => String -> Symbolic (SBV a)
sbvExists String
"x"
                      SP
y <- forall a. SymVal a => String -> Symbolic (SBV a)
sbvForall String
"y"

                      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SP -> SBool
d SP
x SBool -> SBool -> SBool
.=> SP -> SBool
d SP
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 = forall a. Provable a => a -> IO ThmResult
prove forall a b. (a -> b) -> a -> b
$ forall a. Provable a => [String] -> a -> SymbolicT IO SBool
existential [String
"x"] forall a b. (a -> b) -> a -> b
$ \SP
x ->
                     forall a. Provable a => [String] -> a -> SymbolicT IO SBool
universal [String
"y"] forall a b. (a -> b) -> a -> b
$ \SP
y ->
                        SP -> SBool
d SP
x SBool -> SBool -> SBool
.=> SP -> SBool
d SP
y