#!/usr/bin/runghc

module EquationalReasoning where

-- Equational reasoning with functions

-- | We can use substitution to reason here:
-- >>> func1 3
-- 5
func1 :: Integer -> Integer
func1 z = 8 - z

-- | We can use substitution to reason using both funcs:
-- >>> func2 3 4
-- 20
func2 :: Integer -> Integer -> Integer
func2 x y = (2 + x) * func1 y

-- Equational reasoning with lists
-- Proofs upcoming in Induction lectures.

xs = [1, 2, 3]

ys = [3, 4, 5]

-- | Theorem 1
-- >>> theoremOne
-- True
theoremOne = length (xs ++ ys) == length xs + length ys

-- This is a function that adds 5 to a number.
f :: Int -> Int
f = (+) 5

-- | This is a home-made version of the `map` in Prelude.
-- >>> myMap f xs
-- [6,7,8]
myMap :: (a -> b) -> [a] -> [b]
myMap _ [] = []
myMap f (x : xs) = f x : myMap f xs

-- The real version is available by default in the default haskell Prelude.
-- https://hackage.haskell.org/package/base-4.21.0.0/docs/Prelude.html#v:map
-- https://hackage.haskell.org/package/ghc-internal-9.1201.0/docs/src/GHC.Internal.Base.html#map

-- | Theorem 2
-- >>> theoremTwo
-- True
theoremTwo = length (map f xs) == length xs

-- | Theorem 3
-- >>> theoremThree
-- True
theoremThree = map f (xs ++ ys) == map f xs ++ map f ys

-- | Theorem 4. See lecture notes for two proofs of this one.
-- >>> theoremFour
-- True
theoremFour = length (map f (xs ++ ys)) == length xs + length ys