#|
(defun fib (x) ; Proposed simple but slow definition of fibonacci
               ; (ACL2 has trouble proving termination)
  (if (< x 2)
    1
    (+ (fib (- x 1)) (fib (- x 2)))))
|#

(defun fib (x) ; Simple but slow definition of fibonacci
  (if (or (not (integerp x)) ; <== enables automatic termination proof
          (< x 2))
    1
    (+ (fib (- x 1)) (fib (- x 2)))))

(defun fib2 (x) ; This version eliminates type checks
  (declare (type integer x))
  (if (or (mbe :logic (not (integerp x)) ; <= added MBE
               :exec  nil)               ; <= (must-be-equal)
          (< x 2))
    1
    (+ (fib2 (- x 1)) (fib2 (- x 2)))))

;; Compile (if needed)
(comp '(fib fib2))

;; Timing tests
(list (fib 34) ; prime the pump
      (time$ (fib 34))
      (time$ (fib2 34)))

(thm ; Are they actually equal?  Can we prove it?
 (equal (fib2 x)
        (fib  x)))



(defun fib3-tail (i cur prev) ; Guts of tail-recursive, linear-time version
  (declare (type integer i cur prev))
  (if (or (mbe :logic (not (integerp i))
               :exec nil)
          (< i 2))
    cur
    (fib3-tail (- i 1) (+ cur prev) cur)))

(defun fib3 (x) ; Wrapper for tail-recursive, linear-time version
  (declare (type integer x))
  (fib3-tail x 1 1))

(comp '(fib3-tail fib3))

(list (fib2 34)
      (time$ (fib3 1000))
      (time$ (fib2 34)))


#|
(defthm fib3=fib ; Can we prove that version equals the original? (not yet)
 (equal (fib3 x)
        (fib  x)))
|#

(encapsulate nil ; this exports the fib3-tail--induction-step lemma,
                 ; which is proven using the local lemmas and a book
                 ; of arithemtic reasoning
  (local (defthm fib3-tail-2
           (equal (fib3-tail 2 a b)
                  (+ a b))
           :hints (("Goal" :expand (fib3-tail 2 a b)))))
  
  (local (defthm fib3-tail-3
           (equal (fib3-tail 3 a b)
                  (+ b (* 2 a)))
           :hints (("Goal" :expand (fib3-tail 3 a b)))))

  (local (include-book "arithmetic/top" :dir :system))

  (defthm fib3-tail--induction-step
    (implies (and (integerp x)
                  (<= 2 x))
             (equal (+ (fib3-tail (+ -1 x) v1 v0)
                       (fib3-tail (+ -2 x) v1 v0))
                    (if (equal x 2)
                      (+ v1 v1)
                      (fib3-tail x v1 v0))))))

(defthm fib3=fib ; Now can we see that they're equal?
 (equal (fib3 x)
        (fib  x)))

(defun fib4 (x)
  (declare (type integer x))
  (mbe :logic (fib x)    ; <= Logically, it's the simple, naive version
       :exec (fib3 x))   ; <= For execution, it's the fast version
  )

(thm ; Prove a theorem about simple version using execution
 (= (fib 36)
    24157817))

(thm ; Now with the fast version
 (= (fib4 36)
    24157817))