Discrete Math Using a Computer: Chapter 6 Review Exercises Solutions

DiscreteMathComputer06-Review.hs

{- Discrete Math Using a Computer
   Chapter 6: Propositional Logic
  Review Exercise
-}

import Stdm

--------------------------------------------------------------------------------
-- Exercise 34: Prove A ^ ~A |- False

ex34 :: Theorem
ex34 = Theorem [And P (Not P)] FALSE

{- Proof in natural deduction style
   A and Not A
   A and (A -> False)
   A, A -> False   by And Elimination
   False by Modus Ponens
-}

-- TODO: Problems on Natural Deduction

--------------------------------------------------------------------------------
-- Exercise 44: Use Inference Rules to calculate the value of False -> True

{-  False -> True
    False -> (False -> False)
    TODO: Now what?
-}

--------------------------------------------------------------------------------
-- Exercise 45 : What are the truth values of the following?
--               Write list comprehension to calculate values to check work.

logicExpr1 :: Bool -> Bool -> Bool
logicExpr1 a b = a /\ b \/ a <=> a

{- Claim: logicExpr1 is a Tautology 
   Proof is by cases, using Boolean Algebra
   Assume a is True
    Then, (a ^ b) v a becomes True because P v True is always True
   Assume a is False
    Then, (a ^ b) v a becomes (False ^ b) v False = False v False = False

   In both cases, we see that (a ^ b) v a <=> a
-}

truthTable2 :: (Bool -> Bool -> Bool) -> [(Bool, Bool, Bool)]
truthTable2 f = [(x, y, f x y) | x <- [True, False], y <- [True, False]]

-- *Main> truthTable2 logicExpr1
-- [(True,True,True),(True,False,True),(False,True,True),(False,False,True)]

logicExpr2 a b = (a \/ b) /\ b <=> a /\ b

{- (I thought logicExpr2 would always have the value of b, but that's not correct.
    So I'll just generate the truth table)
    
  | a | b | a v b | LHS = (a v b) ^ b | RHS = (a ^ b) | LHS <==> RHS |
  | T | T | T     | T                 | T             | T            |
  | T | F | T     | F                 | F             | T            |
  | F | T | T     | T                 | F             | F            |
  | F | F | F     | F                 | F             | T            |

-}

-- *Main> truthTable2 logicExpr2
-- [(True,True,True),(True,False,True),(False,True,False),(False,False,True)]

--------------------------------------------------------------------------------
-- Exercise 46: Work out values and check with list comprehension

truthTable3 f = [(x, y, z, f x y z) | x <- [True, False], y <- [True, False], z <- [True, False]]

logicExpr3 :: Bool -> Bool -> Bool -> Bool
logicExpr3 a b c= (a /\ b) \/ (a /\ c) ==> a \/ c

{- 
Claim: logicExpr3 is a tautology.
Proof is by cases on 'a'

Case: a is True
    Left Side: (True ^ b) v (True ^ c)
             = b v c
    Right Side: True v c
             = True

    Since P => True is True for any value of P (when P is true, we get True => True, 
    when P is false, we get False => True, both of which are True)
    The statement is a tautology in the case that a is True

Case: a is False
    Left Side: (False ^ b) v (False ^ c)
            = False v False
            = False

    Right Side: (a v c)
             = False v c
             = c

    Since False => c is True regardless of the value of c (recall "contradiction" from natural logic)
    The statement is a Tautology in the case that a is False

logicExpr3 is a tautology in each individual case, so it is a tautology.

Proof by Truth Table

| a | b | c | a ^ b | a ^ c | LHS = (a ^ b) v (a ^ c) | RHS = (a v c) | LHS => RHS |
| T | T | T | T     | T     | T                       | T             | T          |
| T | T | F | T     | F     | T                       | T             | T          |
| T | F | T | F     | T     | T                       | T             | T          |
| T | F | F | F     | F     | F                       | T             | T          |
| F | T | T | F     | F     | F                       | T             | T          |
| F | T | F | F     | F     | F                       | F             | T          |
| F | F | T | F     | F     | F                       | T             | T          |
| F | F | F | F     | F     | F                       | F             | T          |

So, the statement is a tautology.

*Main> truthTable3 logicExpr3
[(True,True,True,True),(True,True,False,True),(True,False,True,True),(True,False,False,True),(False,True,True,True),(False,True,False,True),(False,False,True,True),(False,False,False,True)]

*Main> all (\ (_, _, _, x) -> x == True) $ truthTable3 logicExpr3
True
-}

logicExpr4 a b c = (a /\ (b \/ c)) \/ (a \/ c) ==> a \/ c

{- Claim: The Statement is a tautology.
   Proof is by cases on "a"

   Assume a is true
     Left side: (a ^ (b v c)) v (a v c) 
              = (True ^ (b v c)) v (True v c)
              = (b v c) v True
              = True
     Right side: a v c
              = True v c
              = True
     Since, True ==> True is True, the statement is a tautology whenever a is True

   Assume a is false
     Left side: (a ^ (b v c)) v (a v c)
              = (False ^ (b v c)) v (False v c)
              = False v c
              = c
     Right side: a v c
               = False v c
               = c
     Obviously, c ==> c, so the statement is a tautology when a is False
     (If unconvinced by "obviously", do proof by cases on c: False -> False is True,
      True -> True is True. So works)

   Since the statement is a tautology in each individual case, it is a tautology.

Mechanical proof:
*Main> all (\ (_, _, _, x) -> x == True) $ truthTable3 logicExpr4
True

-}

--------------------------------------------------------------------------------
-- Exercise 47: Using the logic datatype below, define a function distribute that
--   rewrites an expression using the distributive law
--   and a function demorgan that does the same for demorgan's laws.

-- The logic datatype as they define it conflicts with the Prop datatype in Stdm
-- and for no good reason! I'll just define my function over Prop

                    
demorgan :: Prop -> Prop
demorgan (Not (And p q)) = Or (Not p) (Not q)
demorgan (Not (Or p q)) = And (Not p) (Not q)
demorgan x = x

distribute :: Prop -> Prop
distribute (And p (Or  q r)) = Or (And p q) (And q r)
distribute (Or  p (And q r)) = And (Or p q) (Or q r)

--------------------------------------------------------------------------------
-- Exercise 48: Prove using Boolean Algebra:
-- (C ^ A ^ B) v C = C ^ (C v (A ^ B))

{- 
Proof is by cases on C
Case: C is True
  Left Side: (True ^ A ^ B) v True = True
  Right Side: True ^ (True v (A ^ B)) = True v (A ^ B) = True
  
  So the equality holds for this case.

Case: C is False
  Left Side: (False ^ A ^ B) v False = False v False = False
  Right Side: False ^ (False v (A ^ B)) = False

  So the equality holds in this case as well.
-}

-- verification by computer

ex48 a b c = ((c /\ a) /\ b) \/ c <=> c /\ (c \/ (a /\ b))

-- *Main> all (\ (_, _, _, x) -> x == True) (truthTable3 ex48)
-- True

--------------------------------------------------------------------------------
-- Exercise 49: Prove that:
--              C v (A ^ (B v C)) = ((C v A) ^ C) v A ^ B

{- Proof is by cases on C
Case: C is True
 Left Side: True v (A ^ (B v True)) = True
 Right Side: ((True v A) ^ True) v (A ^ B)
             = (True ^ True) v (A ^ B)
             = True v (A ^ B)
             = True
  so the equality holds when C is True

Case: C is False
 Left Side: False v (A ^ (B v False)) = A ^ (B v False) = A ^ B
 Right Side: ((False v A) ^ False) v A ^ B = False v (A ^ B) = A ^ B

 So the equality holds when C is False


So the equality holds in both cases.
-}

-- verification by computer:

ex49 a b c = c \/ (a /\ (b \/ c)) <=> ((c \/ a) /\ c) \/ (a /\ b)

-- *Main> all (\ (_, _, _, x) -> x == True) (truthTable3 ex49)
-- True