-- Induction.hs
-- by Scot Drysdale on 10/7/09
-- Demonstrates that writing an inductive proof as a recursive 
-- program can allow a full proof to be generated for any given case.

-- Proves that the sum of integers from 1 to n is n(n+1)/2.
proveSum  :: Int -> IO()
proveSum n =
  if n == 0 
  then 
    do putStrLn "We verify that 0*1/2 = 0,"
       putStrLn "  so Sum(n) = n(n+1)/2 holds for n = 0."
       putStrLn "In what follows we use the fact that "
       putStrLn "  Sum(n) = Sum(n-1) + n."
      
  else 
    do putStrLn ("To verify that Sum(n) = n(n+1)/2 holds for n = " 
                      ++ show n)
       putStrLn ("  we first show that it holds for n = " 
                      ++ (show (n-1)) ++ ".")
       proveSum (n-1)
       putStrLn ("Having proved that Sum(" ++ (show (n-1)) ++ 
                   ") = " ++ (show (n-1)) ++ "*" ++
                   (show n) ++ "/2 = " ++ (show ((n-1)*n `div` 2)))
       putStrLn ("  we note that " ++ (show ((n-1)*n `div` 2)) ++ " + " 
                   ++ (show n) ++ " = " ++ (show (n*(n+1) `div` 2))  ++ 
                   " = " ++ (show n) ++ "*" ++ (show (n+1)) ++ "/2.")
       putStrLn ("Thus Sum(n) = n(n+1)/2 holds for n = " ++ (show n)
                   ++ ".")