-- Theorem prover (section 2.6) - fixed version module TheoremProver2 where import QuickCheck import List import Monad newtype Name = Name String deriving (Eq, Show) data Form = Var Name | Form :& Form | Not Form deriving (Eq, Show) names :: Form -> [Name] names (Var v) = [v] names (p :& q) = names p `union` names q names (Not p) = names p data Valuation = Val { falses :: [Name], trues :: [Name] } deriving (Eq, Show) nothing :: Valuation nothing = Val { falses = [], trues = [] } tableau :: Form -> Valuation -> [Valuation] tableau (Var v) val | v `elem` trues val = [val] | v `elem` falses val = [] | otherwise = [val {trues = v:trues val}] tableau (Not (Var v)) val | v `elem` trues val = [] | v `elem` falses val = [val] | otherwise = [val {falses = v:falses val}] tableau (p :& q) val = [valpq | valp <- tableau p val, valpq <- tableau q valp] tableau (Not (p :& q)) val = tableau (Not p) val ++ tableau (p :& Not q) val tableau (Not (Not p)) val = tableau p val models :: Form -> [Valuation] models p = tableau p nothing instance Arbitrary Name where arbitrary = sized \$ \n -> do c <- elements (take (n+1) ['a'..'z']) return (Name [c]) valuationOver :: [Name] -> Gen Valuation valuationOver ns = do bs <- vector (length ns) return (Val { falses = [ n | (n,False) <- ns `zip` bs ], trues = [ n | (n,True ) <- ns `zip` bs ] }) -- A not-very-intelligent answer to Exercise 2.6 - try to improve it, -- particularly to reduce the percentage of trivial tests of prop_Complete instance Arbitrary Form where arbitrary = sized arbForm arbForm 0 = liftM Var arbitrary arbForm n | n > 0 = frequency [(1,liftM Var arbitrary), (1,liftM2 (:&) subForm subForm), (1,liftM Not subForm)] where subForm = arbForm (n `div` 2) -- Note that there's an error in the definition on page 35 - it talks about -- "trues v" and "falses v". (|=) :: Valuation -> Form -> Bool val |= Var v | v `elem` trues val = True | v `elem` falses val = False | otherwise = error "undefined variable" val |= (p :& q) = (val |= p) && (val |= q) val |= Not p = not (val |= p) totalise :: Valuation -> Valuation -> Valuation val `totalise` ext = Val { falses = falses val ++ (falses ext \\ defined), trues = trues val ++ (trues ext \\ defined) } where defined = falses val ++ trues val prop_Sound :: Form -> Property prop_Sound p = forAll (valuationOver (names p)) \$ \ext -> all (\val -> (val `totalise` ext) |= p) (models p) covers :: Valuation -> Valuation -> Bool val `covers` val' = falses val `subset` falses val' && trues val `subset` trues val' where xs `subset` ys = all (`elem` ys) xs -- note typo in definition on page 37 - valuationsOver instead of valuationOver prop_Complete :: Form -> Property prop_Complete p = forAll (valuationOver (names p)) \$ \val -> val |= p ==> trivial (length (names p) <=2) (any (\val' -> val' `covers` val) (models p)) -- definition on page 38 doesn't typecheck prop_Exclusive :: Form -> Bool prop_Exclusive p = not (or [ val `covers` val' | val <- ms, val' <- ms \\ [val] ]) where ms = models p