Fancy (classical) propositional logic checker

PropCheck.hs

{-# LANGUAGE TypeFamilies #-}

import Control.Applicative
import Data.Functor.Compose


------------------------------------------------------------------------
-- Preliminaries

(-->) :: Bool -> Bool -> Bool
a --> b = not a || b
infixr 1 -->

(|-) :: [Bool] -> Bool -> Bool
as |- b = and as --> b
infixr 0 |-

type Table = [([Bool], Bool)]

type Check = Compose [] ((,) [Bool])


------------------------------------------------------------------------
-- The algorithm

class Checkable a where
    check_ :: Check a -> Check Bool

instance Checkable Bool where
    check_ = id

instance (bool ~ Bool, Checkable a) => Checkable (bool -> a) where
    check_ = check_ . (<*> tests)
      where
        tests = Compose [([False], False), ([True], True)]

truthTable :: Checkable a => a -> Table
truthTable = getCompose . check_ . pure


------------------------------------------------------------------------
-- Output

check :: Checkable a => a -> IO ()
check f = putStrLn $ case failures of
    [] -> "Passed " ++ show (length results) ++ " tests!\n"
    _ -> "*** FAILED ***\nCounterexamples:\n"
            ++ showTable failures
  where
    results = truthTable f
    failures = filter (not . snd) results

showTable :: Table -> String
showTable = unlines . map (("    " ++) . showRow)
  where
    showRow (as, b) = unwords $ map showBool as ++ ["->", showBool b]
    showBool x = if x then "T" else "F"


------------------------------------------------------------------------
-- Examples

-- Modus ponens
modusPonens a b = [a --> b, a] |- b

-- One of De Morgan's laws
deMorgan a b = [not (a && b)] |- not a || not b

-- Denying the antecedent
fallacy1 a b = [a --> b, not a] |- not b

-- Affirming a disjunct
fallacy2 a b = [a || b, a] |- not b

-- Question 1(d)
kitty c f = [f --> c, not f --> not c, f || c] |- f && c
politics a g l n = [a || g, a --> not l, not n --> g] |- not (l && n)

main :: IO ()
main = do
    check' "Modus ponens" modusPonens
    check' "De Morgan" deMorgan
    check' "Denying the antecedent" fallacy1
    check' "Affirming a disjunct" fallacy2
    check' "My pet cat is both fluffy and cute" kitty
    check' "Labour and National can't both win" politics
  where
    check' name f = do
        putStrLn $ "[" ++ name ++ "]"
        check f