;; consecutive-fibonacci-numbers-are-coprime.lisp: 隣り合うフィボナッチ数は互いに素である

;; 数字を足したり引いたりする関数に関する証明をするときに便利な Book
(include-book "arithmetic/top-with-meta" :dir :system)

;; フィボナッチ関数の定義
(defun fibonacci (n)
  (declare (xargs :guard (natp n)))
  (cond
    ((zp n) 0)
    ((equal n 1) 1)
    (t (+ (fibonacci (- n 1))
          (fibonacci (- n 2))))))

;; ユークリッドの互除法による最大公約数の定義
(defun gcd$ (n m)
  (declare (xargs :measure (+ (nfix m) (nfix n))
                  :guard (and (posp n)
                              (posp m))))
  (cond
    ((or (not (posp n))
         (not (posp m))
         (= (nfix n) (nfix m)))
     n)
    ((< n m) (gcd$ (- m n) n))
    (t (gcd$ (- n m) m))))

;; gcd$ の結果は正の整数である
(defthm posp-gcd$
  (implies (and (posp m)
                (posp n))
           (posp (gcd$ m n))))

;; n と m が互いに素かどうかを調べる述語
(defmacro coprimep (n m)
  `(equal (gcd$ ,n ,m) 1))

;; 隣り合うフィボナッチ数は互いに素である
(defthm consecutive-fibonacci-numbers-are-coprime
  (implies (posp n)
           (coprimep (fibonacci n)
                     (fibonacci (+ n 1)))))