    -----------------------------------------------------------------------------
    -- |
    -- 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)
    -- @
    -----------------------------------------------------------------------------

    {-# 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 = String -> SP -> SBool
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "D"

    -- | Formulate the drinkers paradox, if some one is drinking, then everyone is!
    --
    -- >>> drinker
    -- Q.E.D.
    drinker :: IO ThmResult
    drinker :: IO ThmResult
    drinker = (Exists Any P -> Forall Any P -> SBool) -> IO ThmResult
    forall a. Provable a => a -> IO ThmResult
    prove ((Exists Any P -> Forall Any P -> SBool) -> IO ThmResult)
    -> (Exists Any P -> Forall Any P -> SBool) -> IO ThmResult
    forall a b. (a -> b) -> a -> b
    $ \(Exists SP
    x) (Forall SP
    y) -> SP -> SBool
    d SP
    x SBool -> SBool -> SBool
    .=> SP -> SBool
    d SP
    y