1 Induction

-- # 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

module HL07IAR where

import Data.List
import HL04STAL (display)

sumOdds' :: Integer -> Integer
sumOdds' n = sum [2 * k - 1 | k <- [1 .. n]]

sumOdds :: Integer -> Integer
sumOdds n = n ^ 2

sumEvens' :: Integer -> Integer
sumEvens' n = sum [2 * k | k <- [1 .. n]]

sumEvens :: Integer -> Integer
sumEvens n = n * (n + 1)

sumInts :: Integer -> Integer
sumInts n = (n * (n + 1)) `div` 2

sumSquares' :: Integer -> Integer
sumSquares' n = sum [k ^ 2 | k <- [1 .. n]]

sumSquares :: Integer -> Integer
sumSquares n = (n * (n + 1) * (2 * n + 1)) `div` 6

sumCubes' :: Integer -> Integer
sumCubes' n = sum [k ^ 3 | k <- [1 .. n]]

sumCubes :: Integer -> Integer
sumCubes n = (n * (n + 1) `div` 2) ^ 2

-- Z is Zero
-- S is Successor
data Natural = Z | S Natural
  deriving (Eq, Show)

plus m Z = m
plus m (S n) = S (plus m n)

m `mult` Z = Z
m `mult` (S n) = (m `mult` n) `plus` m

expn m Z = (S Z)
expn m (S n) = (expn m n) `mult` m

leq Z _ = True
leq (S _) Z = False
leq (S m) (S n) = leq m n

geq m n = leq n m

gt m n = not (leq m n)

lt m n = gt n m

foldn :: (a -> a) -> a -> Natural -> a
foldn h c Z = c
foldn h c (S n) = h (foldn h c n)

exclaim :: Natural -> String
exclaim = foldn ('!' :) []

bittest :: [Int] -> Bool
bittest [] = True
bittest [0] = True
bittest (1 : xs) = bittest xs
bittest (0 : 1 : xs) = bittest xs
bittest _ = False

fib 0 = 0
fib 1 = 1
fib n = fib (n - 1) + fib (n - 2)

fib' n = fib2 0 1 n
  where
    fib2 a b 0 = a
    fib2 a b n = fib2 b (a + b) (n - 1)

data BinTree = L | N BinTree BinTree deriving (Show)

makeBinTree :: Integer -> BinTree
makeBinTree 0 = L
makeBinTree n = N (makeBinTree (n - 1)) (makeBinTree (n - 1))

count :: BinTree -> Integer
count L = 1
count (N t1 t2) = 1 + count t1 + count t2

depth :: BinTree -> Integer
depth L = 0
depth (N t1 t2) = (max (depth t1) (depth t2)) + 1

balanced :: BinTree -> Bool
balanced L = True
balanced (N t1 t2) =
  (balanced t1)
    && (balanced t2)
    && depth t1 == depth t2

data Tree = Lf | Nd Int Tree Tree deriving (Show)

data Tr a = Nil | T a (Tr a) (Tr a) deriving (Eq, Show)

type Dict = Tr (String, String)

split :: [a] -> ([a], a, [a])
split xs = (ys1, y, ys2)
  where
    ys1 = take n xs
    (y : ys2) = drop n xs
    n = length xs `div` 2

data LeafTree a
  = Leaf a
  | Node (LeafTree a) (LeafTree a)
  deriving (Show)

ltree :: LeafTree String
ltree =
  Node
    (Leaf "I")
    ( Node
        (Leaf "love")
        (Leaf "you")
    )

data Rose a = Bud a | Br [Rose a] deriving (Eq, Show)

rose = Br [Bud 1, Br [Bud 2, Bud 3, Br [Bud 4, Bud 5, Bud 6]]]

len [] = 0
len (x : xs) = 1 + len xs

cat :: [a] -> [a] -> [a]
cat [] ys = ys
cat (x : xs) ys = x : (cat xs ys)

add :: [Natural] -> Natural
add = foldr plus Z

mlt :: [Natural] -> Natural
mlt = foldr mult (S Z)

ln :: [a] -> Natural
ln = foldr (\_ n -> S n) Z

rev :: [a] -> [a]
rev = foldl (\xs x -> x : xs) []

rev' :: [a] -> [a]
rev' = foldr (\x xs -> xs ++ [x]) []

data Peg = A | B | C

type Tower = ([Int], [Int], [Int])

move :: Peg -> Peg -> Tower -> Tower
move A B (x : xs, ys, zs) = (xs, x : ys, zs)
move B A (xs, y : ys, zs) = (y : xs, ys, zs)
move A C (x : xs, ys, zs) = (xs, ys, x : zs)
move C A (xs, ys, z : zs) = (z : xs, ys, zs)
move B C (xs, y : ys, zs) = (xs, ys, y : zs)
move C B (xs, ys, z : zs) = (xs, z : ys, zs)

transfer :: Peg -> Peg -> Peg -> Int -> Tower -> [Tower]
transfer _ _ _ 0 tower = [tower]
transfer p q r n tower =
  transfer p r q (n - 1) tower
    ++ transfer r q p (n - 1) (move p q tower')
  where
    tower' = last (transfer p r q (n - 1) tower)

hanoi :: Int -> [Tower]
hanoi n = transfer A C B n ([1 .. n], [], [])

check :: Int -> Tower -> Bool
check 0 t = t == ([], [], [])
check n (xs, ys, zs)
  | xs /= [] && last xs == n = check (n - 1) (init xs, zs, ys)
  | zs /= [] && last zs == n = check (n - 1) (ys, xs, init zs)
  | otherwise = False

maxT :: Tower -> Int
maxT (xs, ys, zs) = foldr max 0 (xs ++ ys ++ zs)

checkT :: Tower -> Bool
checkT t = check (maxT t) t

parity :: Tower -> (Int, Int, Int)
parity (xs, ys, zs) = par (xs ++ [n + 1], ys ++ [n], zs ++ [n + 1])
  where
    n = maxT (xs, ys, zs)
    par (x : xs, y : ys, z : zs) = (mod x 2, mod y 2, mod z 2)

target :: Tower -> Peg
target t@(xs, ys, zs)
  | parity t == (0, 1, 1) = A
  | parity t == (1, 0, 1) = B
  | parity t == (1, 1, 0) = C

move1 :: Tower -> Tower
move1 t@(1 : _, ys, zs) = move A (target t) t
move1 t@(xs, 1 : _, zs) = move B (target t) t
move1 t@(xs, ys, 1 : _) = move C (target t) t

move2 :: Tower -> Tower
move2 t@(1 : xs, [], zs) = move C B t
move2 t@(1 : xs, ys, []) = move B C t
move2 t@(1 : xs, ys, zs) = if ys < zs then move B C t else move C B t
move2 t@([], 1 : ys, zs) = move C A t
move2 t@(xs, 1 : ys, []) = move A C t
move2 t@(xs, 1 : ys, zs) = if xs < zs then move A C t else move C A t
move2 t@([], ys, 1 : zs) = move B A t
move2 t@(xs, [], 1 : zs) = move A B t
move2 t@(xs, ys, 1 : zs) = if xs < ys then move A B t else move B A t

done :: Tower -> Bool
done ([], [], _) = True
done (xs, ys, zs) = False

transfer1, transfer2 :: Tower -> [Tower]
transfer1 t = t : transfer2 (move1 t)
transfer2 t = if done t then [t] else t : transfer1 (move2 t)

hanoi' :: Int -> [Tower]
hanoi' n = transfer1 ([1 .. n], [], [])

zazen :: [Tower]
zazen = hanoi' 64

hanoiCount :: Int -> Integer -> Tower
hanoiCount n k
  | k < 0 = error "argument negative"
  | k > 2 ^ n - 1 = error "argument not in range"
  | k == 0 = ([1 .. n], [], [])
  | k == 2 ^ n - 1 = ([], [], [1 .. n])
  | k < 2 ^ (n - 1) = (xs ++ [n], zs, ys)
  | k >= 2 ^ (n - 1) = (ys', xs', zs' ++ [n])
  where
    (xs, ys, zs) = hanoiCount (n - 1) k
    (xs', ys', zs') = hanoiCount (n - 1) (k - 2 ^ (n - 1))

toTower :: Integer -> Tower
toTower n = hanoiCount k m
  where
    n' = fromInteger (n + 1)
    k = truncate (logBase 2 n')
    m = truncate (n' - 2 ^ k)

data Form = P Int | Conj Form Form | Disj Form Form | Neg Form

instance Show Form where
  show (P i) = 'P' : show i
  show (Conj f1 f2) = "(" ++ show f1 ++ " & " ++ show f2 ++ ")"
  show (Disj f1 f2) = "(" ++ show f1 ++ " v " ++ show f2 ++ ")"
  show (Neg f) = "~" ++ show f

subforms :: Form -> [Form]
subforms (P n) = [(P n)]
subforms (Conj f1 f2) = (Conj f1 f2) : (subforms f1 ++ subforms f2)
subforms (Disj f1 f2) = (Disj f1 f2) : (subforms f1 ++ subforms f2)
subforms (Neg f) = (Neg f) : (subforms f)

ccount :: Form -> Int
ccount (P n) = 0
ccount (Conj f1 f2) = 1 + (ccount f1) + (ccount f2)
ccount (Disj f1 f2) = 1 + (ccount f1) + (ccount f2)
ccount (Neg f) = 1 + (ccount f)

acount :: Form -> Int
acount (P n) = 1
acount (Conj f1 f2) = (acount f1) + (acount f2)
acount (Disj f1 f2) = (acount f1) + (acount f2)
acount (Neg f) = acount f

module Sol7 where

import Data.List
import HL07IAR

-- | 7.14
-- >>>
subtr :: Natural -> Natural -> Natural
subtr Z _ = Z
subtr m Z = m
subtr (S m) (S n) = subtr m n

-- | 7.15
-- >>>
qrm :: Natural -> Natural -> (Natural, Natural)
qrm m n
  | gt n m = (Z, m)
  | otherwise = (S (fst qr), snd qr)
  where
    qr = qrm (subtr m n) n

quotient :: Natural -> Natural -> Natural
quotient m n = fst (qrm m n)

remainder :: Natural -> Natural -> Natural
remainder m n = snd (qrm m n)

-- | 7.16
-- >>>
pre :: Natural -> Natural
pre Z = Z
pre (S n) = n

subtr2 :: Natural -> Natural -> Natural
subtr2 = foldn pre

-- Did Haskell uset to allow this math on the left of = ?

-- | 7.20
-- >>>
--
-- catalan :: Integer -> Integer
-- catalan 0 = 1
-- catalan (n + 1) = sum [(catalan i) * (catalan (n - i)) | i <- [0 .. n]]

-- | 7.25
-- >>>
--
-- data TernTree = L' | N' TernTree TernTree TernTree deriving (Show)
--
-- makeTernTree :: Integer -> TernTree
-- makeTernTree 0 = L'
-- makeTernTree (n + 1) = N' (makeTernTree n) (makeTernTree n) (makeTernTree n)
--
-- count3 :: TernTree -> Integer
-- count3 L' = 1
-- count3 (N' t1 t2 t3) = 1 + count3 t1 + count3 t2 + count3 t3

-- | 7.28
-- >>>
insertTree :: Int -> Tree -> Tree
insertTree n Lf = (Nd n Lf Lf)
insertTree n t@(Nd m left right)
  | m < n = Nd m left (insertTree n right)
  | m > n = Nd m (insertTree n left) right
  | otherwise = t

-- | 7.29
-- >>>
list2tree :: [Int] -> Tree
list2tree [] = Lf
list2tree (n : ns) = insertTree n (list2tree ns)

tree2list :: Tree -> [Int]
tree2list Lf = []
tree2list (Nd n left right) = tree2list left ++ [n] ++ tree2list right

-- | 7.30
-- >>>
inTree :: Int -> Tree -> Bool
inTree n Lf = False
inTree n (Nd m left right)
  | n == m = True
  | n < m = inTree n left
  | n > m = inTree n right

-- | 7.31
-- >>>
mergeTrees :: Tree -> Tree -> Tree
mergeTrees t1 t2 = foldr insertTree t2 (tree2list t1)

-- | 7.32
findDepth :: Int -> Tree -> Int
findDepth _ Lf = -1
findDepth n (Nd m left right)
  | n == m = 0
  | n < m = if d1 == -1 then -1 else d1 + 1
  | n > m = if d2 == -1 then -1 else d2 + 1
  where
    d1 = findDepth n left
    d2 = findDepth n right

-- | 7.33
mapT :: (a -> b) -> Tr a -> Tr b
mapT f Nil = Nil
mapT f (T x left right) = T (f x) (mapT f left) (mapT f right)

-- | 7.34
foldT :: (a -> b -> b -> b) -> b -> (Tr a) -> b
foldT h c Nil = c
foldT h c (T x left right) = h x (foldT h c left) (foldT h c right)

-- | 7.35
preorderT, inorderT, postorderT :: Tr a -> [a]
preorderT = foldT preLists []
  where
    preLists x ys zs = (x : ys) ++ zs
inorderT = foldT inLists []
  where
    inLists x ys zs = ys ++ [x] ++ zs
postorderT = foldT postLists []
  where
    postLists x ys zs = ys ++ zs ++ [x]

-- | 7.36
orderedT :: (Ord a) => Tr a -> Bool
orderedT tree = ordered (inorderT tree)
  where
    ordered xs = (sort (nub xs) == xs)

-- | 7.37
lookupD :: String -> Dict -> [String]
lookupD _ Nil = []
lookupD x (T (v, w) left right)
  | x == v = [w]
  | x < v = lookupD x left
  | otherwise = lookupD x right

-- | 7.38
buildTree :: [a] -> Tr a
buildTree [] = Nil
buildTree xs = T m (buildTree left) (buildTree right)
  where
    (left, m, right) = split xs

-- | 7.39
mapLT :: (a -> b) -> LeafTree a -> LeafTree b
mapLT f (Leaf x) = Leaf (f x)
mapLT f (Node left right) = Node (mapLT f left) (mapLT f right)

-- | 7.40
reflect :: LeafTree a -> LeafTree a
reflect (Leaf x) = Leaf x
reflect (Node left right) = Node (reflect right) (reflect left)

-- | 7.42
mapR :: (a -> b) -> Rose a -> Rose b
mapR f (Bud x) = Bud (f x)
mapR f (Br roses) = Br (map (mapR f) roses)

-- | 7.46
genUnion :: (Eq a) => [[a]] -> [a]
genUnion = foldr union []

genIntersect :: (Eq a) => [[a]] -> [a]
genIntersect = foldr1 intersect

-- | 7.47
insrt :: (Ord a) => a -> [a] -> [a]
insrt x [] = [x]
insrt x (y : ys) = if x <= y then (x : y : ys) else y : (insrt x ys)

srt :: (Ord a) => [a] -> [a]
srt = foldr insrt []

-- | 7.51
ln' :: [a] -> Natural
ln' = foldl (\n _ -> S n) Z

-- Skipped those about Tower of Hanoi

module Nats where

import Data.Ratio

data Natural = Z | S Natural deriving (Eq, Show)

instance Ord Natural where
  compare Z Z = EQ
  compare Z _ = LT
  compare _ Z = GT
  compare (S m) (S n) = compare m n

instance Enum Natural where
  succ = S
  pred Z = Z
  pred (S n) = n
  toEnum = fromIntegral
  fromEnum = foldn succ 0
  enumFrom n = map toEnum [(fromEnum n) ..]

instance Num Natural where
  (+) = foldn succ
  (*) = \m -> foldn (+ m) Z
  (-) = foldn pred
  abs = id
  signum Z = Z
  signum n = (S Z)
  fromInteger n
    | n < 0 = error "no negative naturals"
    | n == 0 = Z
    | otherwise = S (fromInteger (n - 1))

foldn :: (a -> a) -> a -> Natural -> a
foldn h c Z = c
foldn h c (S n) = h (foldn h c n)

instance Real Natural where toRational x = toInteger x % 1

instance Integral Natural where
  quotRem n d
    | d > n = (Z, n)
    | otherwise = (S q, r)
    where
      (q, r) = quotRem (n - d) d
  toInteger = foldn succ 0

module HL08WWN where

import Data.Char
import Data.Complex
import Data.List
import Data.Ratio
import Nats

binary :: (Integral a) => a -> [Int]
binary x = reverse (bits x)
  where
    bits 0 = [0]
    bits 1 = [1]
    bits n = fromIntegral (rem n 2) : bits (quot n 2)

showDigits :: [Int] -> String
showDigits = map intToDigit

bin :: (Integral a) => a -> String
bin = showDigits . binary

coprime :: Integer -> Integer -> Bool
coprime m n = (gcd m n) == 1

gcde :: (Integral a) => a -> a -> (a, a, a)
gcde a b
  | a == 0 && b == 0 = error "gcd undefined"
  | a < 0 || b < 0 = error "gcd undefined"
  | a == 0 = (b, 0, 1)
  | b == 0 = (a, 1, 0)
  | a > b =
      let (k, r) = quotRem a b
          (d, x, y) = gcde b r
       in (d, y, x - k * y)
  | otherwise =
      let (k, r) = quotRem b a
          (d, x, y) = gcde a r
       in (d, x - k * y, y)

data Sgn = P | N deriving (Eq, Show)

type MyInt = (Sgn, Natural)

myplus :: MyInt -> MyInt -> MyInt
myplus (s1, m) (s2, n)
  | s1 == s2 = (s1, m + n)
  | s1 == P && n <= m = (P, m - n)
  | s1 == P && n > m = (N, n - m)
  | otherwise = myplus (s2, n) (s1, m)

type NatPair = (Natural, Natural)

plus1 :: NatPair -> NatPair -> NatPair
plus1 (m1, m2) (n1, n2) = (m1 + n1, m2 + n2)

subtr1 :: NatPair -> NatPair -> NatPair
subtr1 (m1, m2) (n1, n2) = plus1 (m1, m2) (n2, n1)

mult1 :: NatPair -> NatPair -> NatPair
mult1 (m1, m2) (n1, n2) = (m1 * n1 + m2 * n2, m1 * n2 + m2 * n1)

eq1 :: NatPair -> NatPair -> Bool
eq1 (m1, m2) (n1, n2) = (m1 + n2) == (m2 + n1)

reduce1 :: NatPair -> NatPair
reduce1 (m1, Z) = (m1, Z)
reduce1 (Z, m2) = (Z, m2)
reduce1 (S m1, S m2) = reduce1 (m1, m2)

decExpand :: Rational -> [Integer]
decExpand x
  | x < 0 = error "negative argument"
  | r == 0 = [q]
  | otherwise = q : decExpand ((r * 10) % d)
  where
    (q, r) = quotRem n d
    n = numerator x
    d = denominator x

decForm :: Rational -> (Integer, [Int], [Int])
decForm x
  | x < 0 = error "negative argument"
  | otherwise = (q, ys, zs)
  where
    (q, r) = quotRem n d
    n = numerator x
    d = denominator x
    (ys, zs) = decF (r * 10) d []

decF :: Integer -> Integer -> [(Int, Integer)] -> ([Int], [Int])
decF n d xs
  | r == 0 = (reverse (q : (map fst xs)), [])
  | elem (q, r) xs = (ys, zs)
  | otherwise = decF (r * 10) d ((q, r) : xs)
  where
    (q', r) = quotRem n d
    q = fromIntegral q'
    xs' = reverse xs
    Just k = elemIndex (q, r) xs'
    (ys, zs) = splitAt k (map fst xs')

mechanicsRule :: Rational -> Rational -> Rational
mechanicsRule p x = (1 % 2) * (x + (p * (recip x)))

mechanics :: Rational -> Rational -> [Rational]
mechanics p x = iterate (mechanicsRule p) x

sqrtM :: Rational -> [Rational]
sqrtM p
  | p < 0 = error "negative argument"
  | otherwise = mechanics p s
  where
    s = if xs == [] then 1 else last xs
    xs = takeWhile (\m -> m ^ 2 <= p) [1 ..]

approximate :: Rational -> [Rational] -> Rational
approximate eps (x : y : zs)
  | abs (y - x) < eps = y
  | otherwise = approximate eps (y : zs)

apprx :: [Rational] -> Rational
apprx = approximate (1 / 10 ^ 6)

mySqrt :: Rational -> Rational
mySqrt p = apprx (sqrtM p)

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

-- TODO: add all the solutions to corresponding files

module HL10COR where

import Polynomials
import PowerSeries
import System.Random (mkStdGen, randomRs)

default (Integer, Rational, Double)

ones = 1 : ones

nats = 0 : map (+ 1) nats

odds = 1 : map (+ 2) odds

theOnes = iterate id 1

theNats = iterate (+ 1) 0

theOdds = iterate (+ 2) 1

theNats1 = 0 : zipWith (+) ones theNats1

theFibs = 0 : 1 : zipWith (+) theFibs (tail theFibs)

pr (x1 : x2 : x3 : xs) = x1 * x3 - x2 * x2 : pr (x2 : x3 : xs)

sieve :: [Integer] -> [Integer]
sieve (0 : xs) = sieve xs
sieve (n : xs) = n : sieve (mark xs 1 n)
  where
    mark (y : ys) k m
      | k == m = 0 : (mark ys 1 m)
      | otherwise = y : (mark ys (k + 1) m)

sieve' :: [Integer] -> [Integer]
sieve' (n : xs) = n : sieve' (filter (\m -> (rem m n) /= 0) xs)

primes' :: [Integer]
primes' = sieve' [2 ..]

randomInts :: Int -> Int -> [Int]
randomInts bound seed =
  tail (randomRs (0, bound) (mkStdGen seed))

type Process = [Int] -> [String]

start :: Process -> Int -> Int -> [String]
start process bound seed = process (randomInts bound seed)

clock :: Process
clock (0 : xs) = "tick" : clock xs
clock (1 : xs) = "crack" : []

vending, vending1, vending2, vending3 :: Process
vending (0 : xs) = "coin" : vending1 xs
vending (1 : xs) = vending xs
vending1 (0 : xs) = "coin" : vending2 xs
vending1 (1 : xs) = "water" : vending xs
vending2 (0 : xs) = "coin" : vending3 xs
vending2 (1 : xs) = "beer" : vending xs
vending3 (0 : xs) = "moneyback" : vending xs
vending3 (1 : xs) = vending3 xs

ptd :: Process
ptd = ptd0 0

ptd0 :: Int -> Process
ptd0 0 (0 : xs) = ptd0 0 xs
ptd0 i (0 : xs) = ("return " ++ show i ++ " euro") : ptd0 0 xs
ptd0 i (1 : xs) = "1 euro" : ptd0 (i + 1) xs
ptd0 i (2 : xs) = "2 euro" : ptd0 (i + 2) xs
ptd0 0 (3 : xs) = ptd0 0 xs
ptd0 i (3 : xs) = ("ticket " ++ show (i * 20) ++ " min") : ptd0 0 xs

actions = user [0, 0, 1] responses

responses = vending actions

user acts ~(r : s : p : resps) = acts ++ user (proc [r, s, p]) resps

proc ["coin", "coin", "beer"] = [0, 0, 1]

approx :: Integer -> [a] -> [a]
approx n []
  | n <= 0 = undefined
  | otherwise = []
approx n (x : xs) = x : approx (n - 1) xs

o2e :: (Num a) => [a] -> [a]
o2e [] = []
o2e (f : fs) = f : o2e (deriv (f : fs))

e2o :: (Ord a, Fractional a) => [a] -> [a]
e2o [] = []
e2o (f : fs) = [f] + (int (e2o (fs)))

module Sol10 where

import HL10COR

-- | 10.1 Write a corecursive definition that generates the even natural numbers.
-- >>> take 5 evens
-- [0,2,4,6,8]
evens = 0 : map (+ 2) evens

-- | 10.2 Use iterate to define the infinite stream of even natural numbers.
-- >>> take 5 theEvens
-- [0,2,4,6,8]
theEvens = iterate (+ 2) 0

-- | 10.3 Thue-Morse sequence
-- >>> take 100 thue
-- "0110100110010110100101100110100110010110011010010110100110010110100101100110100101101001100101100110"
swap "" = ""
swap ('1' : xs) = '0' : swap xs
swap ('0' : xs) = '1' : swap xs

morse xs = xs ++ morse (xs ++ swap xs)

thue = '0' : morse "1"

-- | 10.5 How would you implement a generator for streams of 0’s and 1’s with, in the long run, a proportion of 0’s and 1’s of 2 to 1?
-- >>>
random001s :: Int -> [Int]
random001s i = map (`mod` 2) (randomInts 2 i)

-- | 10.10 Vending machine from text
-- >>>
vend, vend1, vend2, vend3, vend4 :: Process
vend (0 : xs) = "coin" : vend1 xs
vend (1 : xs) = "coin" : vend4 xs
vend1 (0 : xs) = "coin" : vend2 xs
vend1 (1 : xs) = vend1 xs
vend2 (0 : xs) = "beer" : vend xs
vend2 (1 : xs) = "coin" : vend3 xs
vend3 (0 : xs) = "moneyback" : vend xs
vend3 (1 : xs) = vend3 xs
vend4 (0 : xs) = "water" : vend xs
vend4 (1 : xs) = vend4 xs

module HL11FAIS where

natpairs = [(x, z - x) | z <- [0 ..], x <- [0 .. z]]

rationals = [(n, m) | (n, m) <- natpairs, m /= 0, gcd n m == 1]

diagonal :: (Integer -> [Bool]) -> Integer -> Bool
diagonal f n = not ((f n) !! (fromInteger n))

f :: Integer -> [Bool]
f 0 = cycle [False]
f (n + 1) = True : f n

module Sol11 where

import HL11FAIS

-- | 11.17
ball :: Int -> [[Int]]
ball n = ballgame [n]

ballgame :: [Int] -> [[Int]]
ballgame xs
  | all (== 1) xs = [xs]
  | otherwise = xs : ballgame (reduce xs)
  where
    reduce (1 : ys) = 1 : reduce ys
    reduce (n : ys) = (n - 1) : (n - 1) : ys

-- | 11.79 The function pair is nothing but the function j defined in Theorem 11.52. Here it is (to check that it is the inverse of natpairs, you can use map pair natpairs):
pair (n, m) = (n + m) * (n + m + 1) `div` 2 + n

-- | 11.79 First, we need code for enumerating N2 , N3 , . . . , as lists:
natpairs2 = [(x, toInt z - x) | z <- [0 ..], x <- [0 .. z]]

natlist 0 = [[n] | n <- [0 ..]]
natlist k = [n : (natlist (k - 1) !! m) | (n, m) <- natpairs2]

natstar = [] : [natlist n !! m | (n, m) <- natpairs2]