HASKELL PROOF BY MATHEMATICAL INDUCTION EXAMPLE 1

REVISED: Saturday, October 5, 2024

1. INTRODUCTION

This tutorial introduces using Haskell for proof by Mathematical Induction that an infinite equation's left-hand side (LHS) equals the right-hand side (RHS).

Recursive proofs are called induction. Mathematical Induction is a method of formal proof in which a statement is proved for one step in a process, and it is shown that if the statement holds for that step, it holds for the next. The beauty of induction is that it allows a theorem to be proven true where an infinite number of cases exist without exploring each case individually.

Step 1. Show that the statement is true for the initial lowest value of n, which is often n = 1.

Step 2. Assume that the statement is true for n = k.

Step 3. Use the assumption in "Step 2." to prove that the statement is true for n = k + 1.

Then it follows the statement must be true for all values of n.

2. GHCi RUN

GHCi, version 9.8.1: http://www.haskell.org/ghc/  :? for help
Prelude> :l mathematicalInduction
[1 of 1] Compiling Main             ( mathematicalInduction.hs, interpreted )
Ok, modules loaded: Main.
*Main> main

==========================================================

Prove: 2 + 4 + 6 +...+ (2*n) = n*(n+1) by mathematical induction.

Step 1: Show it is True for n = 1.

LHS = 2*n and RHS = n*(n+1).

LHS = 2 and RHS = 2.

LHS = RHS; therefore, it is True for n = 1.

==========================================================

Prove: 2 + 4 + 6 +...+ (2*n) = n*(n+1) by mathematical induction.

Step 2: Assume it is True for n = k.

That is: 2 + 4 + 6 +...+ (2*k) = k*(k+1).

==========================================================

Prove: 2 + 4 + 6 +...+ (2*n) = n*(n+1) by mathematical induction.

Step 3: Show it is True for n = k + 1.

That is: 2 + 4 + 6 +...+ (2 * k) + 2 * (k + 1) = (k + 1) * (k + 2).

LHS = 2 + 4 + 6 + ... + (2 * k) + 2 * (k + 1)
= k * (k + 1) + 2 * (k + 1)
= (k + 1) * ( (k * 1) + (2 * 1))
= (k + 1) * (k + 2) = RHS

Therefore, it is True for n = k + 1.

Therefore, the statement is True for n >= 1.

Q.E.D.

==========================================================

*Main>

3. HASKELL PROGRAM

The Haskell program is as follows:

-- C:\Users\Tinnel\Haskell2024\mathematicalInduction.hs

{-

LHS is the left-hand side of the = sign.
RHS is the right-hand side of the = sign.

Prove 2+4+6+...+(2*n) = n * (n+1) by mathematical induction.

Step 1. Show that the statement is true for the initial value of n = 1.

LHS = 2 * 1 = 2
RHS = 1 * (1 + 1) = 2

LHS == RHS

-}

import System.IO
import Data.List

l :: Num t => t
l = 1

r :: Num t => t
r = 1

lHs :: Num a => a -> a
lHs l = 2 * l

rHs :: Num a => a -> a
rHs r = r * (r + 1)

main :: IO ()
main = do {  putStrLn ""  -- putStrLn Has type I/O action.
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; putStrLn "Prove: 2 + 4 + 6 +...+ (2*n) = n*(n+1) by mathematical induction."
           ; putStrLn ""
           ; putStrLn "Step 1: Show it is True for n = 1."
           ; putStrLn ""
           ; putStrLn ("LHS = 2*n and " ++ "RHS = n*(n+1).")
           ; putStrLn ""
           ; let lS = show (lHs l)  -- Type converted from Integer z to String z.
           ; let rS = show (rHs r)  -- Type converted from Integer z to String z.
           ; putStrLn ("LHS = " ++ lS ++ " and RHS = " ++ rS ++ ".")
           ; putStrLn ""
           ; let i = if (lHs l == rHs r) then "True" else "False"
           ; putStrLn ("LHS = RHS; therefore, it is " ++ i ++ " for n = 1.")
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; putStrLn "Prove: 2 + 4 + 6 +...+ (2*n) = n*(n+1) by mathematical induction."
           ; putStrLn ""
           ; putStrLn "Step 2: Assume it is True for n = k."
           ; putStrLn ""
           ; putStrLn "That is: 2 + 4 + 6 +...+ (2*k) = k*(k+1)."
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; putStrLn "Prove: 2 + 4 + 6 +...+ (2*n) = n*(n+1) by mathematical induction."
           ; putStrLn ""
           ; putStrLn "Step 3: Show it is True for n = k + 1."
           ; putStrLn ""
           ; putStrLn "That is: 2 + 4 + 6 +...+ (2 * k) + 2 * (k + 1) = (k + 1) * (k + 2)."
           ; putStrLn ""
           ; putStrLn "LHS = 2 + 4 + 6 + ... + (2 * k) + 2 * (k + 1)"
           ; putStrLn ""
           ; putStrLn "= k * (k + 1) + 2 * (k + 1)"
           ; putStrLn ""
           ; putStrLn "= (k + 1) * ( (k * 1) + (2 * 1))"
           ; putStrLn ""
           ; putStrLn "= (k + 1) * (k + 2) = RHS"
           ; putStrLn ""
           ; putStrLn "Therefore, it is True for n = k + 1."
           ; putStrLn ""
           ; putStrLn "Therefore, the statement is True for n >= 1."
           ; putStrLn ""
           ; putStrLn "Q.E.D."
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
          }
--

4. CONCLUSION

Using Haskell and Mathematical Induction we have proven 2+4+6+...+(2*n) = n * (n+1).

5. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.

HASKELL AND YOUR AGE BY CHOCOLATE

REVISED: Saturday, October 5, 2024

1. INTRODUCTION

This tutorial is for having fun with Haskell.

2. HASKELL PROGRAM

The Haskell program is as follows:

-- C:\Users\Tinnel\Haskell2024\age.hs

import Data.List
import System.IO

main :: IO ()  -- Has type I/O action.
main = do {  putStrLn ""  -- putStrLn Has type I/O action.
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; putStrLn "CALCULATING YOUR AGE BY CHOCOLATE!"
           ; putStrLn ""
           ; putStrLn "First, type a positive integer from 1 to 10 indicating how"
           ; putStrLn "often you crave chocolate each week, then press Enter."
           ; cewS <- getLine -- getLine is a function, getLine :: IO String
           ; putStrLn ""
           ; let runTot1I = (read cewS)::Integer
           ; let runTot1S = show runTot1I
           ; putStrLn ("Running Total: " ++ runTot1S)
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; let cewI = (read cewS)::Integer
           ; let cewIx2I = cewI * 2
           ; let cewIx2S = show cewIx2I
           ; putStrLn ("Second, we multiply " ++ cewS ++ " by 2 which equals " ++ cewIx2S ++ ".")
           ; putStrLn ""
           ; let runTot2I = runTot1I * 2
           ; let runTot2S = show runTot2I
           ; putStrLn ("Running Total: " ++ runTot2S)
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; let cewIp5I = cewIx2I + 5
           ; let cewIp5S = show cewIp5I
           ; putStrLn ("Third, we add 5 to our running total which equals " ++ cewIp5S ++ ".")
           ; putStrLn ""
           ; let runTot3I = runTot2I + 5
           ; let runTot3S = show runTot3I
           ; putStrLn ("Running Total: " ++ runTot3S)
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; let cewIp5x50I = cewIp5I * 50
           ; let cewIp5x50S = show cewIp5x50I
           ; putStrLn ("Fourth, we multiply our running total by 50 which equals " ++ cewIp5x50S ++ ".")
           ; putStrLn ""
           ; let runTot4I = runTot3I * 50
           ; let runTot4S = show runTot4I
           ; putStrLn ("Running Total: " ++ runTot4S)
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; putStrLn "Fifth, type the current year date as a positive integer; e.g., 2017"
           ; putStrLn "then press Enter."
           ; yearS <- getLine -- getLine is a function, getLine :: IO String
           ; putStrLn ""
           ; putStrLn ("Running Total: " ++ runTot4S)
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; let yearI = (read yearS)::Integer
           ; let runTotI = cewIp5x50I + (yearI - 250)
           ; let runTotS = show runTotI
           ; putStrLn "Sixth, we subtract 250 from the current year; e.g., 2017 - 250 = 1767"
           ; putStrLn ("and add the result to our running total which equals " ++ runTotS ++ ".")
           ; putStrLn ""
           ; let runTot6I = runTot4I + (yearI - 250)
           ; let runTot6S = show runTot6I
           ; putStrLn ("Running Total: " ++ runTot6S)
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; putStrLn "Seventh, if you have not had your birthday this year type the integer 1."
           ; putStrLn "If you have had your birthday this year type zero; e.g., 0."
           ; putStrLn "Then press Enter."
           ; birthdayS <- getLine -- getLine is a function, getLine :: IO String
           ; putStrLn ""
           ; putStrLn ("Running Total: " ++ runTot6S)
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; let birthdayI = (read birthdayS)::Integer
           ; let runTotMI = (runTotI - birthdayI)
           ; let runTotMS = show runTotMI
           ; putStrLn "Eighth, we subtract 1 or 0 from the running total."
           ; putStrLn ""
           ; putStrLn ("Now our running total equals " ++ runTotMS ++ ".")
           ; putStrLn ""
           ; let runTot8I = (runTot6I - birthdayI)
           ; let runTot8S = show runTot8I
           ; putStrLn ("Running Total: " ++ runTot8S)
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; putStrLn "Ninth, type the year of your birth; e.g., 1992"
           ; putStrLn "then press Enter."
           ; birthYearS <- getLine -- getLine is a function, getLine :: IO String
           ; putStrLn ""
           ; putStrLn ("Running Total: " ++ runTot8S)
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; let birthYearI = (read birthYearS)::Integer
           ; let runTotBYI = (runTotMI - birthYearI)
           ; let runTotBYS = show runTotBYI
           ; putStrLn "Tenth, we subtract the year you were born from the running total."
           ; putStrLn ""
           ; putStrLn ("Now our running total equals " ++ runTotBYS ++ ".")
           ; putStrLn ""
           ; let runTot10I = (runTot8I - birthYearI)
           ; let runTot10S = show runTot10I
           ; putStrLn ("Running Total: " ++ runTot10S)
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; putStrLn "The running total's first two digits are how often you crave chocolate each week."
           ; putStrLn ""
           ; putStrLn "The last two digits of the running total are your Age By Chocolate."
           ; putStrLn ""
           ; putStrLn ("Running Total: " ++ runTot10S)
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
          }
--

3. GHCi RUN

GHCi, version 9.8.1: http://www.haskell.org/ghc/  :? for help
Prelude> :l age
[1 of 1] Compiling Main             ( age.hs, interpreted )
Ok, modules loaded: Main.

*Main> main
==========================================================

CALCULATING YOUR AGE BY CHOCOLATE!

First, type a positive integer from 1 to 10 indicating how
often you crave chocolate each week, then press Enter.
10

Running Total: 10

==========================================================

Second, we multiply 10 by 2 which equals 20.

Running Total: 20

==========================================================

Third, we add 5 to our running total which equals 25.

Running Total: 25

==========================================================

Fourth, we multiply our running total by 50 which equals 1250.

Running Total: 1250

==========================================================

Fifth, type the current year date as a positive integer; e.g., 2017
then press Enter.
2017

Running Total: 1250

==========================================================

Sixth, we subtract 250 from the current year; e.g., 2017 - 250 = 1767
and add the result to our running total which equals 3017.

Running Total: 3017

==========================================================

Seventh, if you have not had your birthday this year type the integer 1.
If you have had your birthday this year type zero; e.g., 0.
Then press Enter.
0

Running Total: 3017

==========================================================

Eighth, we subtract 1 or 0 from the running total.
Now our running total equals 3017.

Running Total: 3017

==========================================================

Ninth, type the year of your birth; e.g., 1992
then press Enter.
1992

Running Total: 3017

==========================================================

Tenth, we subtract the year you were born from the running total.
Now our running total equals 1025.

Running Total: 1025

==========================================================

The first two digits of the running total are how often you crave chocolate each week.
The last two digits of the running total are your Age By Chocolate.

Running Total: 1025

==========================================================
*Main>

4. CONCLUSION

You can have fun with Haskell.

5. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.

HASKELL PUBLIC KEY CRYPTOGRAPHY USING PRIME NUMBERS

REVISED: Monday, September 23, 2024

1. INTRODUCTION

Prime numbers are significant for Internet security.

For example, a Bank could start with two large prime numbers p1 and p2. The Bank computer multiplies p1 * p2 and the result is used to create a Public Key to encrypt a Customer credit card.

The Bank keeps p1 and p2 secret. Therefore, p1 and p2 are referred to as Secret Keys.

The Secret Keys must be kept secret because they will be used to decrypt the credit card transactions received by the Bank. Once successfully decrypted the credit card transaction will access the Customer's credit card bank balance and increase or decrease the Customer's credit card account.

Prime Factorization using a tree is one decryption method:

It starts by dividing the Public Key by its least prime factor.

The example shown below does a Prime Factorization of the Public Key into two prime numbers which equal the Secret Keys.

    21     -- Public Key
     /\
   3  7    -- Secret Keys are the unique Prime Factorization of the Public Key.

The above Public Key is a small number to make it easier to explain the relationship between the Public Key and the Secret Keys. In reality the Public Key would be a very large number that would take a very long time to determine the Prime Factorization even using a computer. Transactions would be completed before the Prime Factorizations would be computed.

2. HASKELL PROGRAM

The Haskell program is as follows:

-- C:\Users\Tinnel\Haskell2024\cryptography.hs

import Data.List
import System.IO

main :: IO ()  -- Has type I/O action.
main = do {  putStrLn ""  -- putStrLn Has type I/O action.
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; putStrLn "Pretend you are the Bank:"
           ; putStrLn ""
           ; putStrLn "Type a prime number for Secret Key p1 then press Enter."
           ; p1s <- getLine -- getLine is a function, getLine :: IO String
           ; putStrLn ""
           ; putStrLn "Type a prime number for Secret Key p2 then press Enter."
           ; p2s <- getLine
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; putStrLn ("The Secret Keys  p1 and p2 are " ++ p1s ++ " " ++ p2s ++ ".")
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; let p1 = (read p1s)::Integer
           ; let p2 = (read p2s)::Integer
           ; let c = p1 * p2
           ; let cS = show c
           ; putStrLn ("The Public Key is (p1 * p2) which equals " ++ cS ++ ".")
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; putStrLn "The Bank knows the Customer Secret Keys. Therefore,"
           ; putStrLn "the Bank decrypts the Customer Public Key with the Secret Keys."
           ; putStrLn ""
           ; putStrLn "For example, the Bank could compare the product of the Secret Keys with the credit card"
           ; putStrLn "transaction Public Key and if they equal the decryption is successful. Then the Bank can"
           ; putStrLn "process the credit card transaction to the correct Customer credit card account."
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
          }
--  

3. GHCi RUN

*Main> :l cryptography
[1 of 1] Compiling Main             ( cryptography.hs, interpreted )
Ok, modules loaded: Main.
*Main> main

=========================================================================

Pretend you are the Bank:

Type a prime number for Secret Key p1 then press Enter.
3

Type a prime number for Secret Key p2 then press Enter.
7

=========================================================================

The Secret Keys p1 and p2 are 3  7.

=========================================================================

The Public Key is  (p1 * p2) which equals 21.

=========================================================================

The Bank knows the Customer Secret Keys. Therefore,

the Bank decrypts the Customer Public Key with the Secret Keys.

For example, the Bank could compare the product of the Secret Keys with the credit card

transaction Public Key and if they equal the decryption is successful. Then the Bank can

process the credit card transaction to the correct Customer credit card account.

=========================================================================

*Main>

4. CONCLUSION

Using Secret Keys and a Public Key a Bank and a Customer can ensure secure credit card transactions.

5. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.

HASKELL TRIANGULAR NUMBER SEQUENCE

REVISED: Monday, September 23, 2024

1. INTRODUCTION

An equilateral triangle is a triangle with all three sides of equal length and all angles equal to 60°.

Triangular numbers
t n = (n * (n+1)) `div` 2
are the number of objects needed to form an equilateral triangle.

This tutorial shows a method for using Haskell to compute the Triangular Number Sequence of objects needed to form equilateral triangles:

1, 3, 6, 10, 15, 21, 28, 36, 45, 55, 66, 78, 91, 105, 120, 136, 153, 171, 190, 210, 231, 253, 276, 300, 325, 351, 378, 406, 435, 465, 496, 528, 561, 595, 630, 666, 703, 741, 780, 820, 861, 903, 946, 990, 1035, 1081, 1128, 1176, 1225, 1275, 1326, 1378, 1431...

2. HASKELL PROGRAM

A Haskell program used to compute the Triangular Number Sequence is as follows:

-- C:\Users\Tinnel\Haskell2024\triangularNS.hs

import Data.List
import System.IO

main :: IO ()  -- Has type I/O action.
main = do {  putStrLn ""  -- putStrLn Has type I/O action.
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; putStrLn "TRIANGULAR NUMBER SEQUENCE"
           ; putStrLn ""
           ; putStrLn "h = 1      2       3         4          5"
           ; putStrLn "      **     ***     ****     *****     ******"
           ; putStrLn "              ***   h****     *****     ******"
           ; putStrLn "                       ****     *****     ******"
           ; putStrLn "                       h+1     *****     ******"
           ; putStrLn "                                              ******"
           ; putStrLn ""
           ; putStrLn "The above rectangles are h high and h + 1 wide  and contain 2 equilateral triangles."
           ; putStrLn ""
           ; putStrLn "t h is the total stars in one equilateral triangle."
           ; putStrLn "t h = h * (h + 1) `div` 2"
           ; putStrLn ""
           ; putStrLn "For example"
           ; putStrLn "t 5 = 5 * (5 + 1) `div` 2"
           ; putStrLn "equals 15 stars in one equilateral triangle 5 stars high."
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; putStrLn "Type a positive integer representing an equilateral triangle with a height of h then press Enter."
           ; s <- getLine -- getLine is a function, getLine :: IO String
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; let h = (read s)::Integer
           ; putStrLn "The Triangular Number is:"
           ; putStrLn ""
           ; let z = fromIntegral(t h)
           ; print z
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
          }
--
-- Haskell has different functions for integer and 'fractional' division.
-- Int is not an instance of Fractional so you can't use (/) with Int.
-- t :: Fractional a => a -> a

t :: Integral a => a -> a
t h = h * (h + 1 )`div` 2

3. GHCi RUN

*Main> :l triangularNS
[1 of 1] Compiling Main             ( triangularNS.hs, interpreted )
Ok, modules loaded: Main.
*Main> main

=========================================================================

TRIANGULAR NUMBER SEQUENCE

h = 1      2       3        4          5
      **     ***     ****     *****     ******
              ***   h****     *****     ******
                       ****     *****     ******
                       h+1    *****     ******
                                             ******
The above rectangles are h high and h + 1 wide and contain 2 equilateral triangles.

t h is the total stars in one equilateral triangle.
t h = h * (h + 1) `div` 2

For example
t 5 = 5 * (5 + 1) `div` 2
equals 15 stars in one equilateral triangle 5 stars high.

=========================================================================

Type a positive integer representing an equilateral triangle with a height of h then press Enter.
5

=========================================================================

The Triangular Number is:
15

=========================================================================

*Main>

4. CONCLUSION

In this tutorial you have seen a basic approach for using Haskell to compute the Triangular Number Sequence.

5. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.

HASKELL TEST FOR PRIME NUMBER

REVISED: Monday, September 23, 2024

1. INTRODUCTION

The search is on for larger and larger prime numbers. This tutorial will show a method for testing large positive integers to see if they are prime numbers.

The largest explicitly known prime keeps growing. For example,  (2^32582657 - 1),  (2^43112609 - 1) and (2^74207281 - 1)  were recently discovered very large prime numbers. Methods for quickly testing to see if very large positive integers are prime numbers are important tools used in the search for larger prime numbers.

2. HASKELL PROGRAM

The Haskell program we will use in this tutorial to test a positive integer for prime is as follows:

-- C:\Users\Tinnel\Haskell2024\test.hs

import Data.List
import System.IO

main :: IO ()  -- Has type I/O action.
main = do {  putStrLn ""  -- putStrLn Has type I/O action.
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; putStrLn "Type a positive integer you want to test for prime then press Enter."
           ; s <- getLine -- getLine is a function, getLine :: IO String
           ; let n = (read s)::Integer
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
           ; let test = if (p n == 0 || m n == 0) && n /= 1
                        then "True"
                        else if (n == 2 || n == 3)
                             then "True"
                             else if (n == 0 || n == 1)
                                  then "False"
                                  else "False"
           ; putStrLn "QUESTION: True or False, is the number you entered a prime number?"
           ; putStrLn ""
           ; putStrLn ("ANSWER: " ++ test ++ ".")
           ; putStrLn ""
           ; putStrLn "=========================================================="
           ; putStrLn ""
          }

-- Adds 1 and divides by 6; a remainder means False.
p :: Integral a => a -> a
p n = (n + 1) `mod` 6

-- Subtracts 1 and divides by 6; a remainder means False.
m :: Integral a => a -> a
m n = (n - 1) `mod` 6

3. GHCi RUN

Prelude> :l test
[1 of 1] Compiling Main             ( test.hs, interpreted )
Ok, modules loaded: Main.

*Main> main

=========================================================================

Type a positive integer you want to test for prime then press Enter.
29996224275833

=========================================================================

QUESTION: True or False, is the number you entered a prime number?

ANSWER: True.

=========================================================================

*Main>

4. CONCLUSION

The above Haskell program is a quick way to determine if very large positive integers are prime numbers.

5. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.

HASKELL PROOF BY CONTRADICTION EXAMPLE 1

REVISED: Saturday, October 5, 2024

1. INTRODUCTION

1.1 GIVEN

1.1.1 Consider the following proposition:

For all n in the set of positive Natural numbers, the function f n = n ^ 2 + n + 41 is a prime number is True.

1.1.2 Definition

A Prime Number is a whole number greater than or equal to 2 which has two and only two factors; for example, it can be divided without a remainder only by 1 and itself.

2. HASKELL PROGRAM

2.1 TO BE PROVED

We will use a proof by contradiction.

Therefore, we assume that the statement of the proposition that for all n in the set of positive Natural numbers, the function f n = n ^ 2 + n + 41 is a prime number is False.

2.2 PROOF

The Haskell program used for the proof is as follows:

-- C:\Users\Tinnel\Haskell2024\proof1.hs

import Data.Char
import Data.List
import Data.List (elemIndex)
import Data.Map
import Data.Maybe
import Data.Set
import System.IO
--
--
main :: IO ()    -- Has type I/O action.
main = do {  putStrLn ""    -- putStrLn Has type I/O action.
                   ; putStrLn "======================================================"
                   ; putStrLn ""
                   ; putStrLn "Prove the proposition that for all n in the set of positive Natural numbers, the function"
                   ; putStrLn ""
                   ; putStrLn "f n = n ^ 2 + n + 41"
                   ; putStrLn ""
                   ; putStrLn "is a prime number is False."
                   ; putStrLn ""
                   ; putStrLn "======================================================"
                   ; putStrLn ""
                   ; putStrLn "Type a positive integer value for n then press Enter."
                   ; s <- getLine -- getLine is a function, getLine :: IO String
                   ; putStrLn ""
                   ; putStrLn "======================================================"
                   ; putStrLn ""
                   ; putStrLn ("Computing the function with n equal to " ++ s ++ ".")
                   ; putStrLn ""
                   ; let n = (read s)::Integer  -- Type converted from IO String s to Integer n.
                   ; let z = f n  -- z is the integer prime number computed by n.
                   ; let zS = show z  -- Type converted from Integer z to String z.
                   ; putStrLn ("f n = n ^ 2 + n + 41 equals " ++ zS ++ ".")
                   ; putStrLn ""
                   ; putStrLn "======================================================"
                   ; putStrLn ""
                   ; putStrLn "The list of the first 300 prime numbers starting with 2 is as follows:"
                   ; putStrLn ""
                   ; print p  -- The list of prime numbers.
                   ; putStrLn ""
                   ; putStrLn "======================================================"
                   ; putStrLn ""
                   ; putStrLn ("QUESTION: True or False is " ++ zS ++ " a prime number?")
                   ; putStrLn ""
                   ; let i = if elem z p == True then "True" else "False"
                   ; putStrLn ("ANSWER: " ++ i ++ ".")
                   ; putStrLn ""
                   ; putStrLn ""
                   ; putStrLn ""
                 }
--
--
-- t computes prime numbers.
t :: Integral a => [a] -> [a]
t (p : xs) = p : t [x | x <- xs, x `mod` p /= 0]

-- primes is a list of prime numbers computed by t.
primes :: [Integer]
primes = t [2..]  -- Starting with 2 because zero and 1 are not prime numbers.
                         -- However, main can compute n = 0, and n = 1.

-- p is a list of prime numbers taken from those computed by t.
p :: [Integer]
p = take 300 primes

-- f n computes each number compared to the list p for prime.
f :: Num a => a -> a
f n = n ^ 2 + n + 41

-- read :: Read a => String -> a
-- (==) :: (Eq a) => a -> a -> Bool

3. GHCi RUN

GHCi, version 9.8.1: http://www.haskell.org/ghc/  :? for help
Prelude> :l proof1
[1 of 1] Compiling Main             ( proof1.hs, interpreted )
Ok, modules loaded: Main.

*Main> main

=========================================================================

Prove the proposition that for all n in the set of positive Natural numbers, the function

f n = n ^ 2 + n + 41

is a prime number is False.

=========================================================================

Type a positive integer value for n then press Enter.
5

=========================================================================

Computing the function with n equal to 5.

f n = n ^ 2 + n + 41 equals 71.

=========================================================================

The list of the first 300 prime numbers starting with 2 is as follows:

[2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97,101,103,107,109,113,127,131,137,139,149,151,157,163,167,173,179,181,191,193,197,199,211,223,227,229,233,239,241,251,257,263,269,271,277,281,283,293,307,311,313,317,331,337,347,349,353,359,367,373,379,383,389,397,401,409,419,421,431,433,439,443,449,457,461,463,467,479,487,491,499,503,509,521,523,541,547,557,563,569,571,577,587,593,599,601,607,613,617,619,631,641,643,647,653,659,661,673,677,683,691,701,709,719,727,733,739,743,751,757,761,769,773,787,797,809,811,821,823,827,829,839,853,857,859,863,877,881,883,887,907,911,919,929,937,941,947,953,967,971,977,983,991,997,1009,1013,1019,1021,1031,1033,1039,1049,1051,1061,1063,1069,1087,1091,1093,1097,1103,1109,1117,1123,1129,1151,1153,1163,1171,1181,1187,1193,1201,1213,1217,1223,1229,1231,1237,1249,1259,1277,1279,1283,1289,1291,1297,1301,1303,1307,1319,1321,1327,1361,1367,1373,1381,1399,1409,1423,1427,1429,1433,1439,1447,1451,1453,1459,1471,1481,1483,1487,1489,1493,1499,1511,1523,1531,1543,1549,1553,1559,1567,1571,1579,1583,1597,1601,1607,1609,1613,1619,1621,1627,1637,1657,1663,1667,1669,1693,1697,1699,1709,1721,1723,1733,1741,1747,1753,1759,1777,1783,1787,1789,1801,1811,1823,1831,1847,1861,1867,1871,1873,1877,1879,1889,1901,1907,1913,1931,1933,1949,1951,1973,1979,1987]

=========================================================================

QUESTION: True or False is 71 a prime number?

ANSWER: True.

4. TRUTH TABLE

Running the Haskell program for each element of n we obtain the truth table shown below:

n    f n = n^2 + n + 41      Prime
---- ------------------------     -------
  0                           41    True
  1                           43    True
  2                           47    True
  3                           53    True
  4                           61    True
  5                           71    True
  6                           83    True
  7                           97    True
  8                         113    True
  9                         131    True
10                         151    True
11                         173    True
12                         197    True
13                         223    True
14                         251    True
15                         281    True
16                         313    True
17                         347    True
18                         383    True
19                         421    True
20                         461    True
21                         503    True
22                         547    True
23                         593    True
24                         641    True
25                         691    True
26                         743    True
27                         797    True
28                         853    True
29                         911    True
30                         971    True
31                       1033    True
32                       1097    True
33                       1163    True
34                       1231    True
35                       1301    True
36                       1373    True
37                       1447    True
38                       1523    True
39                       1601    True
40                       1681    False  Q.E.D.
41                       1763    False
42                       1847    True
43                       1933    True
44                       2021     Outside of the first 300 prime number range.

5. CONCLUSION

The proposition that for all n in the set of positive Natural numbers, the function f n = n ^ 2 + n + 41 is a prime number is False.

As shown above, you must be careful when concluding whether a proof is True or False. The first 39 tests would lead most people to assume f n = n^2 + n + 41 could be used to compute prime numbers. However tests 40 and 41 show the proposition is not True, it is False.

6. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.