Weird quickcheck fail

[Emanon42]

I am using GHC i 7.10.3 on Ubuntu 16.04 LTS, here is my code:

type Name = String
data Prop = Var Name
          | F
          | T
          | Not Prop
          | Prop :|: Prop
          | Prop :&: Prop
          | Prop :->: Prop
          | Prop :<->: Prop
          deriving (Eq, Ord)

instance Show Prop where
    show  =  showProp

instance Arbitrary Prop where
    arbitrary  =  sized prop
        where
          prop n | n <= 0     =  atom
                 | otherwise  =  oneof [ atom
                                       , liftM Not subform
                                       , liftM2 (:|:) subform subform
                                       , liftM2 (:&:) subform subform
                                       , liftM2 (:->:) subform subform
                                       , liftM2 (:<->:) subform' subform'
                                       ]
                 where
                   atom = oneof [liftM Var (elements ["P", "Q", "R", "S"]),
                                   elements [F,T]]
                   subform  =  prop (n `div` 2)
                   subform' =  prop (n `div` 4)

subformulas :: Prop -> [Prop]
subformulas F = [F]
subformulas T = [T]
subformulas (Var x) = [Var x]
subformulas (Not x) = nub $ (Not x) : subformulas x
subformulas (x :&: y) = nub $ (x :&: y) : subformulas x ++ subformulas y
subformulas (x :|: y) = nub $ (x :|: y) : subformulas x ++ subformulas y
subformulas (x :->: y) = nub $ (x :->: y) : subformulas x ++ subformulas y
subformulas (x :<->: y) = nub $ (x :<->: y) : subformulas x ++ subformulas y

-- check for negation normal form
isImplies :: Prop -> Bool
isImplies (_:->:_) = True
isImplies _ = False

isNestedNega :: Prop -> Bool
isNestedNega (Not (Var _)) = False
isNestedNega (Not _) = True
isNestedNega _ = False

isEquiv :: Prop -> Bool
isEquiv (_:<->:_) = True
isEquiv _ = False

isNNF :: Prop -> Bool
isNNF prop = null [x | x <- subformulas prop, isEquiv x || isImplies x || isNestedNega x]

-- convert to negation normal form
isVar :: Prop -> Bool
isVar (Var _) = True
isVar _ = False

isNegation :: Prop -> Bool
isNegation (Not (Var _)) = True
isNegation _ = False

toNNF :: Prop -> Prop
toNNF (Not (Not x)) = toNNF x
toNNF (Not (x :&: y)) = toNNF (Not (toNNF x)) :|: toNNF (Not (toNNF y))
toNNF (Not (x :|: y)) = toNNF (Not (toNNF x)) :&: toNNF (Not (toNNF y))
toNNF (Not x) = Not (toNNF x)
toNNF (x :->: y) = toNNF (Not x) :|: toNNF y
toNNF (x :<->: y) = toNNF (toNNF x :->: toNNF y) :&: toNNF (toNNF y :->: toNNF x)
toNNF x@(y :|: z) | (isVar y || isNegation y || y == T || y == F) &&
                    (isVar z || isNegation z || z == T || z == F)
                    = x
                  | otherwise = toNNF y :|: toNNF z
toNNF x@(y :&: z) | (isVar y || isNegation y || y == T || y == F) &&
                    (isVar z || isNegation z || z == T || z == F)
                    = x
                  | otherwise = toNNF y :&: toNNF z
toNNF x | isVar x || isNegation x || x == T || x == F = x
        | otherwise = toNNF x

-- check if result of toNNF is in neg. normal form
prop_NNF1 :: Prop -> Bool
prop_NNF1 p  =  isNNF (toNNF p)

[nick8325]

It seems your property is false:

> quickCheck prop_NNF1 
*** Failed! Falsifiable (after 3 tests):  
Var "S" :<->: T
> isNNF $ toNNF $ Var "S" :<->: T
False

I am using deriving Show because you didn't include the code for showProp; maybe showProp is printing the counterexample in a misleading way?

[nick8325]

Ah, I see! In the counterexample (S<->T), the T is not Var "T" but the constructor T :)

[Emanon42]

This is my showProp

showProp :: Prop -> String
showProp (Var x)        =  x
showProp (F)            =  "F"
showProp (T)            =  "T"
showProp (Not p)        =  "(~" ++ showProp p ++ ")"
showProp (p :|: q)      =  "(" ++ showProp p ++ "|" ++ showProp q ++ ")"
showProp (p :&: q)      =  "(" ++ showProp p ++ "&" ++ showProp q ++ ")"
showProp (p :->: q)     =  "(" ++ showProp p ++ "->" ++ showProp q ++ ")"
showProp (p :<->: q)    =  "(" ++ showProp p ++ "<->" ++ showProp q ++ ")"

Yes you are correct.

[Emanon42]

Thank you! I know how to solve it.