{-# LANGUAGE FlexibleInstances #-}

module HL02TAMO where

-- Implication / Therefore / if
infix 1 ==>

-- |
-- >>> False ==> False
-- True

-- |
-- >>> False ==> True
-- True

-- |
-- >>> True ==> False
-- False

-- |
-- >>> True ==> True
-- True
(==>) :: Bool -> Bool -> Bool
x ==> y = (not x) || y

-- Equivalence / If and only if
infix 1 <=>

-- |
-- >>> True <=> True
-- True

-- |
-- >>> True <=> False
-- False

-- |
-- >>> False <=> False
-- True

-- |
-- >>> False <=> True
-- False
(<=>) :: Bool -> Bool -> Bool
x <=> y = x == y

-- Exclusive or
infixr 2 <+>

-- |
-- >>> False <+> False
-- False

-- |
-- >>> False <+> True
-- True

-- |
-- >>> True <+> False
-- True

-- |
-- >>> True <+> True
-- False
(<+>) :: Bool -> Bool -> Bool
x <+> y = x /= y

-- Examples:
p = True

q = False

-- |
-- >>> formula1
-- False
formula1 = (not p) && (p ==> q) <=> not (q && (not p))

-- | To prove a statement true, we can brute force check all combinations of True and False:
-- >>> formula2 True True
-- False

-- |
-- >>> formula2 True False
-- False

-- |
-- >>> formula2 False True
-- False

-- |
-- >>> formula2 False False
-- True
formula2 p q = ((not p) && (p ==> q) <=> not (q && (not p)))

-- | This checks any boolean formula (bf) which takes one value, for example:
-- >>> valid1 excluded_middle
-- True
valid1 :: (Bool -> Bool) -> Bool
valid1 bf = (bf True) && (bf False)

excluded_middle :: Bool -> Bool
excluded_middle p = p || not p

-- | This checks any logical proposition with two values, for example:
-- >>> valid2 form1
-- True

-- |
-- >>> valid2 form2
-- False
valid2 :: (Bool -> Bool -> Bool) -> Bool
valid2 bf =
  (bf True True)
    && (bf True False)
    && (bf False True)
    && (bf False False)

form1 p q = p ==> (q ==> p)

form2 p q = (p ==> q) ==> p

-- | This checks any logical statement with three values, for example:
-- >>>
valid3 :: (Bool -> Bool -> Bool -> Bool) -> Bool
valid3 bf =
  and
    [ bf p q r | p <- [True, False], q <- [True, False], r <- [True, False]
    ]

-- | This checks any logical statement with four values, for example:
-- >>>
valid4 :: (Bool -> Bool -> Bool -> Bool -> Bool) -> Bool
valid4 bf =
  and
    [ bf p q r s | p <- [True, False], q <- [True, False], r <- [True, False], s <- [True, False]
    ]

-- | Logical equivalence of boolean formuae with one input can be tested as follows:
-- >>> logEquiv1 bfBasic1a bfBasic1b
-- True
logEquiv1 :: (Bool -> Bool) -> (Bool -> Bool) -> Bool
logEquiv1 bf1 bf2 =
  (bf1 True <=> bf2 True) && (bf1 False <=> bf2 False)

bfBasic1a :: (Bool -> Bool)
bfBasic1a b = b || not b

bfBasic1b :: (Bool -> Bool)
bfBasic1b b = not b || b

-- | Logical equivalence of boolean formuae with two inputs can be tested as follows:
-- >>> logEquiv2 formula3 formula4
-- True

-- | Logical equivalence of boolean formuae with two inputs can be tested as follows:
-- >>> logEquiv2 formula3 formula5
-- False

-- | Wrapping it up with a validity check:
-- >>> valid2 formula5
-- True
logEquiv2 ::
  (Bool -> Bool -> Bool) ->
  (Bool -> Bool -> Bool) ->
  Bool
logEquiv2 bf1 bf2 =
  and
    [ (bf1 p q) <=> (bf2 p q) | p <- [True, False], q <- [True, False]
    ]

formula3 p q = p

formula4 p q = (p <+> q) <+> q

formula5 p q = p <=> ((p <+> q) <+> q)

-- | Logical equivalence of boolean formuae with three inputs can be tested as follows:
-- >>>
logEquiv3 ::
  (Bool -> Bool -> Bool -> Bool) ->
  (Bool -> Bool -> Bool -> Bool) ->
  Bool
logEquiv3 bf1 bf2 =
  and
    [ (bf1 p q r) <=> (bf2 p q r) | p <- [True, False], q <- [True, False], r <- [True, False]
    ]

-- For defining equivalence laws (Theorem 2.10).
-- Show mathy definition in book (page 45/56) next to code:

class TF p where
  valid :: p -> Bool
  lequiv :: p -> p -> Bool

instance TF Bool where
  valid = id
  lequiv f g = f == g

instance (TF p) => TF (Bool -> p) where
  valid f = valid (f True) && valid (f False)
  lequiv f g =
    (f True) `lequiv` (g True)
      && (f False) `lequiv` (g False)

-- Law of double negation
-- P 𠪪P
test1 = lequiv id (\p -> not (not p))

-- Laws of idempotence
-- P ∧ P ≡ P
-- P ∨ P ≡ P
test2a = lequiv id (\p -> p && p)

test2b = lequiv id (\p -> p || p)

-- (P ⇒ Q) ≡ ¬P ∨ Q
-- ¬(P ⇒ Q) ≡ P ∧ ¬Q
test3a = lequiv (\p q -> p ==> q) (\p q -> not p || q)

test3b = lequiv (\p q -> not (p ==> q)) (\p q -> p && not q)

-- Laws of contraposition
-- (¬P ⇒ ¬Q) ≡ (Q ⇒ P )
-- (P ⇒ ¬Q) ≡ (Q ⇒ ¬P )
-- (¬P ⇒ Q) ≡ (¬Q ⇒ P )
test4a = lequiv (\p q -> not p ==> not q) (\p q -> q ==> p)

test4b = lequiv (\p q -> p ==> not q) (\p q -> q ==> not p)

test4c = lequiv (\p q -> not p ==> q) (\p q -> not q ==> p)

-- (P ⇔ Q) ≡ ((P ⇒ Q) ∧ (Q ⇒ P )) ≡ ((P ∧ Q) ∨ (¬P ∧ ¬Q))
test5a =
  lequiv
    (\p q -> p <=> q)
    (\p q -> (p ==> q) && (q ==> p))

test5b =
  lequiv
    (\p q -> p <=> q)
    (\p q -> (p && q) || (not p && not q))

-- Laws of commutativity
-- P ∧ Q ≡ Q ∧ P
-- P ∨ Q ≡ Q ∨ P
test6a = lequiv (\p q -> p && q) (\p q -> q && p)

test6b = lequiv (\p q -> p || q) (\p q -> q || p)

-- DeMorgan laws
-- ¬(P ∧ Q) ≡ ¬P ∨ ¬Q
-- ¬(P ∨ Q) ≡ ¬P ∧ ¬Q
test7a =
  lequiv
    (\p q -> not (p && q))
    (\p q -> not p || not q)

test7b =
  lequiv
    (\p q -> not (p || q))
    (\p q -> not p && not q)

-- Laws of associativity
-- P ∧ (Q ∧ R) ≡ (P ∧ Q) ∧ R
-- P ∨ (Q ∨ R) ≡ (P ∨ Q) ∨ R
test8a =
  lequiv
    (\p q r -> p && (q && r))
    (\p q r -> (p && q) && r)

test8b =
  lequiv
    (\p q r -> p || (q || r))
    (\p q r -> (p || q) || r)

-- Distribution laws
-- P ∧ (Q ∨ R) ≡ (P ∧ Q) ∨ (P ∧ R)
-- P ∨ (Q ∧ R) ≡ (P ∨ Q) ∧ (P ∨ R)
test9a =
  lequiv
    (\p q r -> p && (q || r))
    (\p q r -> (p && q) || (p && r))

test9b =
  lequiv
    (\p q r -> p || (q && r))
    (\p q r -> (p || q) && (p || r))

-- Proof-related code (not for logic section):
square1 :: Integer -> Integer
square1 x = x ^ 2

square2 :: Integer -> Integer
square2 = \x -> x ^ 2

m1 :: Integer -> Integer -> Integer
m1 = \x -> \y -> x * y

m2 :: Integer -> Integer -> Integer
m2 = \x y -> x * y

solveQdr :: (Float, Float, Float) -> (Float, Float)
solveQdr = \(a, b, c) ->
  if a == 0
    then error "not quadratic"
    else
      let d = b ^ 2 - 4 * a * c
       in if d < 0
            then error "no real solutions"
            else
              ( (-b + sqrt d) / 2 * a,
                (-b - sqrt d) / 2 * a
              )

every, some :: [a] -> (a -> Bool) -> Bool
every xs p = all p xs
some xs p = any p xs