-- # Software Tools for Discrete Mathematics
module Stdm04Induction where

import Data.List
import Stdm03Recursion
import Test.QuickCheck

-- # Chapter 4.  Induction

-- Induction proves that a property P(x) holds for every element of a set.
-- ∀ x ∈ N | P(x)
-- For all x in the net N of natural numbers, the predicate property P is true.
-- Along with list comprehenions, there are four relevant haskell functions:

-- | FOR ALL ∀ with a predicate: all
-- >>> setForAllPredicate
-- True
setForAllPredicate = all (== True) [True, True]

-- | FOR ALL ∀ where the default predicate is a boolean: and
-- >>> setForAllBool
-- True
setForAllBool = and [True, True]

-- | THERE EXISTS ∃ with a predicate: any
-- >>> setThereExistsPredicate
-- True
setThereExistsPredicate = any (== True) [False, True]

-- | THERE EXISTS ∃ where the default predicate is a boolean: or
-- >>> setThereExistsBool
-- True
setThereExistsBool = or [False, True]

-- Theorem 5. ----------------------------------------------
-- Let P(x) be a predicate property that is either true or false,
-- for every element of the set N of natural numbers.
-- If P(0) is true, and P(n) → P(n + 1) holds for all n ≥ 0,
-- then ∀ x ∈ N | P(x) is true.

-- Theorem 6. ----------------------------------------------
-- ∀ x ∈ N | ∑ i for i in n = (n * (n + 1)) `div` 2

-- | 4.2 Proof of sum of natural numbers
-- >>> sumNats 10
-- 55
sumNats :: Integer -> Integer
sumNats n = (n * (n + 1)) `div` 2

-- Theorem 7. ----------------------------------------------
-- ∀ x ∈ N | ∏ i for i in n = fact n

-- | 4.3 Factorial proof
-- >>> factorial 5
-- 120
fact :: Integer -> Integer
fact 0 = 1
fact n = n * fact (n - 1)

-- Theorem 8. ----------------------------------------------
-- ∀ x ∈ N | equals x x = True
-- This is valid Haskell, but it won't ever finish.
equal = and [x == x | x <- [1 ..]]

-- | We can't prove an infinite set by example:
-- >>> equalInsufficient
-- [True,True,True,True,True,True,True,True,True,True]
equalInsufficient = take 10 [x == x | x <- [1 ..]]

-- | Proof base case: equals.1
-- >>> equal1
-- True
equal1 = equals Zero Zero

-- | Assume inductive case: equals2
-- >>> take 10 [equal2 x | x <- infinitePeanos]
-- [True,True,True,True,True,True,True,True,True,True]
equal2 x = equals x x

-- | Inductive case 1. Mirrors the implementation of equals itself
-- >>> equal3
-- True
equal3 = equals (Succ Zero) (Succ Zero) == equals Zero Zero

-- | Inductive case n.
-- >>> take 10 [equal4 x | x <- infinitePeanos]
-- [True,True,True,True,True,True,True,True,True,True]
equal4 x = equals (Succ x) (Succ x) == equals x x

-- Theorem 9. ----------------------------------------------
-- ∀ x ∈ N | sub (add x y) = y
-- This is valid Haskell, but it won't ever finish.
-- We can't prove an infinite set by example:
subZero = and [sub (add x y) x == y | x <- infinitePeanos, y <- infinitePeanos]

-- | Proof base case:
-- >>> take 10 [subZero1 y | y <- infinitePeanos]
-- [True,True,True,True,True,True,True,True,True,True]
subZero1 y = sub (add Zero y) Zero == y

-- | Inductive case 1
-- >>> take 10 [subZero2 y | y <- infinitePeanos]
-- [True,True,True,True,True,True,True,True,True,True]
subZero2 y = sub (add (Succ Zero) y) (Succ Zero) == sub (add Zero y) Zero

-- | Inductive case n
-- >>> take 10 [subZero3 x y | x <- infinitePeanos, y <- infinitePeanos]
-- [True,True,True,True,True,True,True,True,True,True]
subZero3 x y = sub (add (Succ x) y) (Succ x) == sub (add Zero y) x

-- Theorem 10. ----------------------------------------------
-- ∀ x ∈ N | add x (add x y) = add (add x y) z
-- This is valid Haskell, but it won't ever finish.
-- We can't prove an infinite set by example:
associative =
  and
    [ add x (add y z) == add (add x y) z
      | x <- infinitePeanos,
        y <- infinitePeanos,
        z <- infinitePeanos
    ]

-- | Proof base case
-- >>> take 10 [associative1 y z | y <- infinitePeanos, z <- infinitePeanos]
-- [True,True,True,True,True,True,True,True,True,True]
associative1 y z = add Zero (add y z) == add (add Zero y) z

-- | Inductive case 1
-- >>> take 10 [associative2 y z | y <- infinitePeanos, z <- infinitePeanos]
-- [True,True,True,True,True,True,True,True,True,True]
associative2 y z = add (Succ Zero) (add y z) == add (add (Succ Zero) y) z

-- | Inductive case n
-- >>> take 10 [associative3 x y z | x <- infinitePeanos, y <- infinitePeanos, z <- infinitePeanos]
-- [True,True,True,True,True,True,True,True,True,True]
associative3 x y z = add (Succ x) (add y z) == add (add (Succ x) y) z

-- Theorem 11. ----------------------------------------------
-- ∀ x ∈ N | add x Zero = x
-- This is valid Haskell, but it won't ever finish.
-- We can't prove an infinite set by example:
addZero = and [add x Zero == x | x <- infinitePeanos]

-- | Base case
-- >>> addZero1
-- True
addZero1 = add Zero Zero == Zero

-- | Inductive case 1
-- >>> addZero2
-- True
addZero2 = add (Succ Zero) Zero == Succ Zero

-- | Inductive case n.
-- >>> take 10 [addZero3 x | x <- infinitePeanos]
-- [True,True,True,True,True,True,True,True,True,True]
addZero3 x = add (Succ x) Zero == Succ x

-- Theorem 12. ----------------------------------------------
-- ∀ x ∈ N | add (Succ x) y = add x (Succ y)
-- This is valid Haskell, but it won't ever finish.
-- We can't prove an infinite set by example:
addSucc = and [add (Succ x) y == add x (Succ y) | x <- infinitePeanos, y <- infinitePeanos]

-- | Base case
-- >>> take 10 [addSucc1 y | y <- infinitePeanos]
-- [True,True,True,True,True,True,True,True,True,True]
addSucc1 y = add (Succ Zero) y == add Zero (Succ y)

-- | Inductive case 1
-- >>> take 10 [addSucc2 y | y <- infinitePeanos]
-- [True,True,True,True,True,True,True,True,True,True]
addSucc2 y = add (Succ (Succ Zero)) y == add (Succ Zero) (Succ y)

-- | Inductive case n
-- >>> take 10 [addSucc3 x y | x <- infinitePeanos, y <- infinitePeanos]
-- [True,True,True,True,True,True,True,True,True,True]
addSucc3 x y = add (Succ (Succ x)) y == add (Succ x) (Succ y)

-- Theorem 13. ----------------------------------------------
-- ∀ x ∈ N | add x y = add y x
-- This is valid Haskell, but it won't ever finish.
-- We can't prove an infinite set by example:
commutative = and [add x y == add x y | x <- infinitePeanos, y <- infinitePeanos]

-- | Base case
-- >>> take 10 [commutative1 y | y <- infinitePeanos]
-- [True,True,True,True,True,True,True,True,True,True]
commutative1 y = add Zero y == add y Zero

-- | Inductive case 1
-- >>> take 10 [commutative2 y | y <- infinitePeanos]
-- [True,True,True,True,True,True,True,True,True,True]
commutative2 y = add (Succ Zero) y == add y (Succ Zero)

-- | Inductive case n
-- >>> take 10 [commutative3 x y | x <- infinitePeanos, y <- infinitePeanos]
-- [True,True,True,True,True,True,True,True,True,True]
commutative3 x y = add (Succ x) y == add y (Succ x)

-- Theorem 14. ----------------------------------------------
-- Principle of list induction.
-- Suppose P(xs) is a predicate property on a list of some type [a].
-- Suppose that P([]) is true (base case).
-- Suppose that P(xs) holds for arbitrary xs :: [a],
-- then P(x : xs) also holds for arbitrary x :: a.
-- Then, P(xs) holds for every list xs that has infinite length.

-- | Bulit in: sum
-- >>> sumL [1,2,3,4]
-- 10
sumL :: (Num a) => [a] -> a
sumL [] = 0
sumL (x : xs) = x + sumL xs

-- Theorem 15. ----------------------------------------------
-- This is valid Haskell, but needs proving.
-- We can't prove an infinite set by example:
sumCons :: (Num a, Eq a) => [a] -> [a] -> Bool
sumCons xs ys = sum (xs ++ ys) == sum xs + sum ys

-- | Base case
-- >>> quickCheck sumCons
-- +++ OK, passed 100 tests.
sumCons1 :: [Int] -> Bool
sumCons1 ys = sum ([] ++ ys) == sum [] + sum ys

-- | Inductive case
-- >>> quickCheck sumCons2
-- +++ OK, passed 100 tests.
sumCons2 :: [Int] -> [Int] -> Bool
sumCons2 [] ys = sum ([] ++ ys) == sum [] + sum ys
sumCons2 (x : xs) ys = sum ((x : xs) ++ ys) == sum (x : xs) + sum ys

-- Theorem 16. ----------------------------------------------
-- This is valid Haskell, but needs proving.
-- We can't prove an infinite set by example:
lenCons :: (Num a, Eq a) => [a] -> [a] -> Bool
lenCons xs ys = length (xs ++ ys) == length xs + length ys

-- Theorem 17. ----------------------------------------------
-- This is valid Haskell, but needs proving.
-- We can't prove an infinite set by example:
lenMap :: (a -> b) -> [a] -> Bool
lenMap f xs = length (map f xs) == length xs

-- | Base case
-- >>> lenMap1 (+1) []
-- True

-- | Inductive case example
-- >>> lenMap1 (+ 1) [1,2]
-- True
lenMap1 :: (Int -> Int) -> [Int] -> Bool
lenMap1 f [] = length (map f []) == length []
lenMap1 f (x : xs) = length (map f (x : xs)) == length (x : xs)

-- Theorem 18. ----------------------------------------------
-- This is valid Haskell, but needs proving.
-- We can't prove an infinite set by example:

-- | Base case
-- >>> mapCons (+ 1) [] []
-- True

-- | Inductive case example
-- >>> mapCons (+ 1) [1,2] [3,4]
-- True
mapCons :: (Eq b) => (a -> b) -> [a] -> [a] -> Bool
mapCons f [] ys = map f ([] ++ ys) == map f [] ++ map f ys
mapCons f xs [] = map f (xs ++ []) == map f xs ++ map f []
mapCons f xs ys = map f (xs ++ ys) == map f xs ++ map f ys

-- Theorem 19. ----------------------------------------------

-- | Base case
-- >>> mapComposition (+ 2) (* 2) []
-- True

-- | Inductive case example
-- >>> mapComposition (+ 2) (* 2) [1,2]
-- True
mapComposition :: (Eq c) => (b -> c) -> (a -> b) -> [a] -> Bool
mapComposition f g [] = (map f . map g) [] == map (f . g) []
mapComposition f g xs = (map f . map g) xs == map (f . g) xs

-- Theorem 20. ----------------------------------------------

-- | Base case
-- >>> sumMap []
-- True

-- | Inductive case example
-- >>> sumMap [1]
-- True
sumMap :: (Num a, Eq a) => [a] -> Bool
sumMap [] = sum (map (1 +) []) == genericLength [] + sum []
sumMap xs = sum (map (1 +) xs) == genericLength xs + sum xs

-- Theorem 21. ----------------------------------------------

-- | Base case
-- >>> foldCons []
-- True

-- | Inductive case example
-- >>> foldCons [1]
-- True
foldCons :: (Eq a) => [a] -> Bool
foldCons (x : xs) = foldr (:) [] (x : xs) == (x : xs)
foldCons xs = foldr (:) [] xs == xs

-- Theorem 22. ----------------------------------------------

-- | Base case
-- >>> mapConcat (1 +) []
-- True

-- | Inductive case example
-- >>> mapConcat (1 +) [[1,2],[3,4]]
-- True
mapConcat :: (Eq b) => (a -> b) -> [[a]] -> Bool
mapConcat f (xs : xss) = map f (concat (xs : xss)) == concat (map (map f) (xs : xss))
mapConcat f xss = map f (concat xss) == concat (map (map f) xss)

-- Theorem 23. ----------------------------------------------

-- | Example
-- >>> lengthConcat [1,2,3] [3,4,5,6]
-- True
lengthConcat :: [a] -> [a] -> Bool
lengthConcat xs (y : ys) = length (xs ++ (y : ys)) == 1 + length xs + length ys

-- Equality of functions and function composition.

-- Intensional equality: f and g are equal if their definitions are identical.

-- Extensional equality: f and g are equal if they have:
-- the same type a → b and
-- f x = g x for all well-typed arguments where x :: a
-- ∀ x :: a | f x = gx

-- | Demonstrating id function
-- >>> id 5
-- 5

-- | Demonstrating id function
-- >>> id False
-- False

-- Theorem 24. ----------------------------------------------

-- | Base case
-- >>> foldrCons []
-- True

-- | Inductive case example
-- >>> foldrCons [1,2,3]
-- True
foldrCons :: (Eq a) => [a] -> Bool
foldrCons x = foldr (:) [] x == id x

-- Theorem 25. ----------------------------------------------
-- Almost the as Theorem 22.
mapConcatF :: (Eq b) => (a -> b) -> [[a]] -> Bool
mapConcatF f xxs = (map f . concat) xxs == concat (map (map f) xxs)

-- Theorem 26. ----------------------------------------------
-- Word problem in book

-- Theorem 27. ----------------------------------------------

-- | Base case
-- >>> reverseId []
-- True

-- | Inductive case example
-- >>> reverseId [1,2,3]
-- True
reverseId :: (Eq a) => [a] -> Bool
reverseId xs = (reverse . reverse) xs == id xs