(set-defunc-function-contract-strictp nil)

(definec sum (k :nat) :nat
  (if (= k 0)
      0
    (+ k (sum (- k 1)))))

(time$ (sum (expt 10 3)))
(time$ (sum (expt 10 4)))
(time$ (sum (expt 10 5)))
(time$ (sum (expt 10 7)))

;; Hmm. What is going on? We need a tail recursive definition.

(definec asum (k :nat acc :nat) :nat
  (if (= k 0)
      acc
    (asum (- k 1) (+ k acc))))

(definec tsum (k :nat) :nat
  (asum k 0))

(time$ (sum  (expt 10 3)))
(time$ (tsum (expt 10 3)))

(time$ (sum  (expt 10 5)))
(time$ (tsum (expt 10 5)))

; this one led to a stack overflow before
(time$ (tsum (expt 10 7)))
(time$ (tsum (expt 10 8)))
(time$ (tsum (expt 10 9)))

"So, notice we went from about about 0.05 to 0.5 to 5 seconds,
an exponential increase in time by increasing the size of the
input by 1 (we added one 0)."

(expt 10 7) ; 1 followed by 7 0s
(expt 10 8) ; size increased by 1
(expt 10 9) ; size increased by 1


"Let's see how our efficient definition does."
(definec fsum (k :nat) :nat
  (/ (* k (+ k 1)) 2))

"Let's ask ACL2s to prove it is equivalent to the previous definition."
(thm (implies (natp k)
              (equal (sum k)
                     (fsum k))))

"This took tsum ~ 5 seconds"
(time$ (fsum (expt 10 9)))

"The next form would take tsum ~5*10^3=5000 seconds ~1.3 hours to do"
(time$ (fsum (expt 10 12))) 

"The next form would take tsum ~5*10^11 seconds ~15,000 years to do"
(time$ (fsum (expt 10 20)))