fibonacci

other

(in-package "ACL2")

include-book

(include-book "int-division")

include-book

(include-book "grcd")

npmacro

(defmacro np
  (x)
  (list 'and (list 'integerp x) (list '<= 0 x)))

pintpmacro

(defmacro pintp
  (x)
  (list 'and (list 'integerp x) (list '< 0 x)))

fib-generalfunction

(defun fib-general
  (x y n)
  (cond ((zp n) 0)
    ((equal n 0) 0)
    ((equal n 1) x)
    ((equal n 2) y)
    ((< 2 n) (fib-general y (+ x y) (+ -1 n)))
    (t nil)))

fibfunction

(defun fib
  (n)
  (cond ((zp n) 0)
    ((equal n 0) 0)
    ((equal n 1) 1)
    (t (+ (fib (- n 1)) (fib (- n 2))))))

fib-general-at-3theorem

(defthm fib-general-at-3
  (equal (fib-general x y 3) (+ x y))
  :hints (("Goal" :expand (fib-general x y 3))))

fib-general-recursive-equationtheorem

(defthm fib-general-recursive-equation
  (implies (and (integerp n) (< 2 n))
    (equal (+ (fib-general x y (+ -1 n)) (fib-general x y (+ -2 n)))
      (fib-general x y n))))

fib-is-special-case-of-fib-generaltheorem

(defthm fib-is-special-case-of-fib-general
  (equal (fib n) (fib-general 1 1 n))
  :hints (("Goal" :induct (fib n)))
  :rule-classes nil)

fib-identity-base-casetheorem

(defthm fib-identity-base-case
  (implies (and (integerp n) (< 1 n))
    (equal (fib n) (+ (fib (- n 1)) (fib (- n 2))))))

fib-identitytheorem

(defthm fib-identity
  (implies (and (pintp n) (pintp k) (< k n))
    (equal (fib n)
      (+ (* (fib k) (fib (+ n (- k) 1)))
        (* (fib (+ k -1)) (fib (+ n (- k)))))))
  :rule-classes nil)

in-theory

(in-theory (disable fib))

fib-neighbours-lemmatheorem

(defthm fib-neighbours-lemma
  (implies (and (integerp k) (< 1 k))
    (equal (grcd (fib k) (fib (+ -1 k)))
      (grcd (fib (+ -1 k)) (fib (+ -2 k)))))
  :hints (("Goal" :use ((:instance grcd-addition-lemma
        (a (fib (+ -1 k)))
        (b (fib (+ -2 k)))
        (c 1))))))

in-theory

(in-theory (disable fib-identity-base-case))

local

(local (defun ind-int->=-2
    (n)
    (if (and (integerp n) (<= 2 n))
      (ind-int->=-2 (+ -1 n))
      t)))

fib-neighbours-are-relative-primestheorem

(defthm fib-neighbours-are-relative-primes
  (implies (pintp k) (equal (grcd (fib k) (fib (+ -1 k))) 1))
  :hints (("Goal" :induct (ind-int->=-2 k))))

grcd-fib-recursion-lemma-1theorem

(defthm grcd-fib-recursion-lemma-1
  (implies (and (pintp n) (pintp k) (<= k n))
    (equal (grcd (fib k) (* (fib (+ -1 k)) (fib (+ (- k) n))))
      (grcd (fib k) (fib (- n k)))))
  :hints (("Goal" :use ((:instance grcd-multiplication-with-relative-prime
        (a (fib k))
        (b (fib (- n k)))
        (c (fib (+ -1 k))))))))

grcd-fib-recursion-lemma-2theorem

(defthm grcd-fib-recursion-lemma-2
  (implies (and (pintp n)
      (pintp k)
      (<= k n)
      (equal (fib n)
        (+ (* (fib k) (fib (+ 1 (- k) n)))
          (* (fib (+ -1 k)) (fib (+ (- k) n))))))
    (equal (grcd (fib k) (fib n)) (grcd (fib k) (fib (- n k)))))
  :hints (("Goal" :use ((:instance grcd-addition-lemma
        (a (fib k))
        (b (* (fib (- n k)) (fib (+ -1 k))))
        (c (fib (+ 1 n (- k)))))))))

grcd-subtracttheorem

(defthm grcd-subtract
  (implies (and (integerp k) (integerp n))
    (equal (grcd k (+ (- k) n)) (grcd k n)))
  :hints (("Goal" :use ((:instance grcd-addition-lemma (a k) (b n) (c (- 1)))))))

grcd-0theorem

(defthm grcd-0
  (implies (np a) (equal (grcd 0 a) a))
  :hints (("Goal" :in-theory (enable grcd euclid-alg-nat))))

grcd-fib-recursiontheorem

(defthm grcd-fib-recursion
  (implies (and (pintp n) (pintp k) (<= k n))
    (equal (grcd (fib k) (fib n)) (grcd (fib k) (fib (- n k)))))
  :hints (("Goal" :use fib-identity)))

in-theory

(in-theory (enable euclid-alg-nat))

main-grcd-fibtheorem

(defthm main-grcd-fib
  (implies (and (pintp n) (pintp k))
    (equal (grcd (fib k) (fib n)) (fib (grcd k n))))
  :hints (("Goal" :induct (euclid-alg-nat k n)) ("Subgoal *1/4" :in-theory (disable grcd-fib-recursion))))

Included Books