;; ===========================================================================
;; A bound for the space needed by the result array in a Karatsuba
;; algorithm by R. E. Maeder.
;; [http://www.springerlink.com/content/w15058mj6v59t565/]
;;
;; Proof for the ACL2 Theorem Prover, http://www.cs.utexas.edu/~moore/acl2/ 
;; ===========================================================================


;; Books containing helper theorems.
(include-book "arithmetic/top-with-meta" :dir :system)
(include-book "arithmetic-2/floor-mod/floor-mod" :dir :system)


;; Amount of memory needed for c when following a certain call path.
(defun cspace (n lim)
  (declare (xargs :guard (and (natp n)
                              (natp lim)
                              (<= 4 lim))
                  :verify-guards nil))
  (and (<= 4 lim)
       (if (<= (nfix n) lim)
           (* 2 n)
         (let ((m (floor (+ n 1) 2)))
              (+ m (cspace (+ m 1) lim))))))

(defthm natp-cspace
  (implies (and (natp n) (natp lim) (<= 4 lim))
           (natp (cspace n lim)))
  :rule-classes :type-prescription)

(verify-guards cspace)


;; =====================================================
;;        Tight upper bound: 3 * (ceil(n/2) + 1)
;; =====================================================

;; Rewriting floor in terms of mod frequently helps.
(defthmd floor-to-mod
  (implies (and (< 0 m) (rationalp m)
                (rationalp x))
           (equal (floor x m)
                  (- (/ x m) (/ (mod x m) m)))))

(defthm lemma-1a
  (implies (and (< 0 m) (natp m)
                (natp n))
           (<= (+ (* 4 (mod n m))
                  (- (* 3 (mod n (* 2 m)))))
               m))
  :rule-classes :linear)
 
(defthm lemma-1b
  (implies (and (< 8 n) (natp n))
           (<= (+ 3 (* 3 (floor (+ 1 n) 4)))
               (* 2 (floor (+ 1 n) 2))))
  :hints (("Goal" :use ((:instance floor-to-mod
                                   (x (+ 1 n))
                                   (m 2))
                        (:instance floor-to-mod
                                   (x (+ 1 n))
                                   (m 4)))))
  :rule-classes :linear)

;; For n <= 8 case analysis is required.
(defthmd upper-bound-n<=8
  (implies (and (<= 4 lim) (< lim n) (<= n 8)
                (natp lim) (natp n))
           (<= (cspace n lim)
               (* 3 (+ 1 (floor (+ n 1) 2)))))
  :hints (("Subgoal *1/5''" :cases ((= n 5) (= n 6) (= n 7) (= n 8)))))


;; The upper bound for cspace.
(defthmd upper-bound
  (implies (and (<= 4 lim) (< lim n)
                (natp lim) (natp n))
           (<= (cspace n lim)
               (* 3 (+ 1 (floor (+ n 1) 2)))))
  :hints (("Goal" :induct t)
          ("Subgoal *1/2.1'" :use (upper-bound-n<=8))))


;; ====================================================
;;        A generous upper bound: 2*n + 1
;; ====================================================

;; This bound holds also if n <= lim
(defthmd generous-upper-bound
  (implies (and (natp n) (natp lim) (<= 4 lim))
           (<= (cspace n lim)
               (+ 1 (* 2 n)))))