module Sol02 where

import HL01GS
import HL02TAMO

-- 2.13 Theorem 2.12 p48/59

-- ¬> ≡ ⊥; ¬⊥ ≡ >
tst1a = not True <=> False

tst1b = not False <=> True

-- P ⇒ ⊥ ≡ ¬P
tst2 = logEquiv1 (\p -> p ==> False) (\p -> not p)

-- P ∨ > ≡ >; P ∧ ⊥ ≡ ⊥ (dominance laws)
tst3a = logEquiv1 (\p -> p || True) (const True)

tst3b = logEquiv1 (\p -> p && False) (const False)

-- P ∨ ⊥ ≡ P ; P ∧ > ≡ P (identity laws)
tst4a = logEquiv1 (\p -> p || False) id

tst4b = logEquiv1 (\p -> p && True) id

-- P ∨ ¬P ≡ > (law of excluded middle)
tst5 = logEquiv1 excluded_middle (const True)

-- P ∧ ¬P ≡ ⊥ (contradiction)
tst6 = logEquiv1 (\p -> p && not p) (const False)

-- The implementation uses excluded_middle; this is defined in Chapter 2 as a name for the function
-- (\ p -> p || not p). const k is the function which gives value k for any argument.
-- Note that the implementation of tst4a and tst4b makes clear why P ∨ ⊥ ≡ P and P ∧ > ≡ P are called laws of identity.

-- 2.15 A propositional contradiction is a formula that yields false for every combination of truth values for its proposition letters. Write Haskell definitions of contradiction tests for propositional functions with one, two and three variables.
contrad1 :: (Bool -> Bool) -> Bool
contrad1 bf = not (bf True) && not (bf False)

contrad2 :: (Bool -> Bool -> Bool) -> Bool
contrad2 bf = and [not (bf p q) | p <- [True, False], q <- [True, False]]

contrad3 :: (Bool -> Bool -> Bool -> Bool) -> Bool
contrad3 bf =
  and [not (bf p q r) | p <- [True, False], q <- [True, False], r <- [True, False]]

-- 2.51 Define a function unique :: (a -> Bool) -> [a] -> Bool that gives True for unique p xs just in case there is exactly one object among xs that satisfies p.
unique :: (a -> Bool) -> [a] -> Bool
unique p xs = length (filter p xs) == 1

-- 2.52 Define a function parity :: [Bool] -> Bool that gives True for parity xs just in case an even number of the xss equals True.
parity :: [Bool] -> Bool
parity [] = True
parity (x : xs) = x /= (parity xs)

-- 2.53 Define a function evenNR :: (a -> Bool) -> [a] -> Bool that gives True for evenNR p xs just in case an even number of the xss have property p. (Use the parity function from the previous exercise.)
evenNR :: (a -> Bool) -> [a] -> Bool
evenNR p = parity . map p

-- Alternative solution:
evenNR' :: (a -> Bool) -> [a] -> Bool
evenNR' p xs = even (length (filter p xs))