Discrete Math Using a Computer: Section 6.6 Solutions

DiscreteMathComputer06-6.hs

{- Discrete Math Using a Computer
   Chapter 6: Propositional Logic
   Section 6.6 - Proof Checking by Computer

   In this section, STDM's proof checker is used to verify some proofs
-}

import Stdm
--------------------------------------------------------------------------------
-- Theorem 55: |- Q => ((P ^ R) => (R ^ Q))
theorem55 :: Theorem
theorem55 = Theorem [] (Imp Q (Imp (And P R) (And R Q)))
-- [] is because we have no assumptions (nothing to the left of \vdash)

-- To check this theorem, we use check_proof :: Theorem -> Proof -> IO ()

{- Proof:
- Assume P ^ R, by and elimination, we have R
- By introducing and, we have Q ^ R
- We have a sequent: (P ^ R), Q => R ^ Q
- By introducing imply, we have Q |- (P ^ R => R ^ Q
- By introducing imply, we have |- Q => (P ^ R) => (R ^ Q)
-}

proof55 :: Proof
proof55 = ImpI (ImpI (AndI ((AndER (Assume (And P R)) R),
                           Assume Q)
                     (And R Q))
               (Imp (And P R) (And R Q)))
         (Imp Q (Imp (And P R) (And R Q)))
         
-- > check_proof theorem55 proof55
-- The proof is valid         

invalidProof55 :: Proof
invalidProof55 = ImpI (ImpI (AndI (Assume Q,
                                   (AndER (Assume (And P R))
                                           R))
                                   (And R Q)) -- mistake we should have And Q R
                       (Imp (And P R) (And R Q)))
                 (Imp Q (Imp (And P R) (And R Q)))
                       
-- check_proof theorem55 invalidProof55
-- *** The proof is NOT valid ***
-- Reported errors:
--  .AndI: the conclusion (And R Q) is not the logical And of the assumption (Q) with the assumption (R)

--------------------------------------------------------------------------------
-- Exercise 22: Replace R ^ Q below {^I} line with Q ^ R. This fixes Invalid 
-- And-Introduction error but introduces another error into the proof.

-- (a) edit proof 2 to reflect this change, call it proof3
exProof55 :: Proof
exProof55 = ImpI (ImpI (AndI (Assume Q,
                              (AndER (Assume (And P R))
                               R))
                        (And Q R)) -- the change they want us to make
                  (Imp (And P R) (And R Q)))
            (Imp Q (Imp (And P R) (And R Q)))

-- (b) the problem is that we're still referring to (And R Q) below
-- we need to replace all that. but then we end up proving the "wrong"
-- theorem. To bad we aren't yet aware of commutativity of And

-- (c) Does the proof checker point out the same error?
-- check_proof theorem55 exProof55
-- *** The proof is NOT valid ***
-- Reported errors:
--  .ImpI: the conclusion in (Imp (And P R) (And R Q)) doesn't match the conclusion above line (And Q R)

-- YES


--------------------------------------------------------------------------------
-- Ex 23: Represent logical expressions as "Prop" a datatype in Stdm

-- P
ex23a = P

-- Q v False
ex23b = Or Q FALSE

-- Q -> (P -> (P ^ Q)
ex23c = Imp Q (Imp P (And P Q))

-- P ^ (~Q)
ex23d = And P (Not Q)

-- ~P -> Q
ex23e = Imp (Not P) Q

-- (P ^ ~Q) v (~P ^ Q) -> (P v Q)
ex23f = Imp (Or (And P (Not Q))
                (And (Not P) Q))
            (Or P Q)

--------------------------------------------------------------------------------
-- Ex 24: Convert back to mathematical notation

-- And P Q 
-- P ^ Q

-- Imply (Not P) (Or R S) 
-- ~P => R v S

-- Equ (Imply P Q) (Or (Not P) Q)
-- P => Q <=> ~P ^ Q