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

;; 数字を足したり引いたりする関数に関する証明をするときに便利な 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))))
  (if (and (posp n) (posp m))
      (cond
        ((= n m)
         n)
        ((< n m) (gcd$ (- m n) n))
        (t (gcd$ (- n m) m)))
      0))

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

;; c が n と m の公約数であるかを調べる述語
(defmacro common-divisor-p (c n m)
  `(and (integerp (* ,n (/ ,c)))
        (integerp (* ,m (/ ,c)))))

;; gcd-is-common-divisor の補助定理
(defthm gcd-is-common-divisor-lemma-1
  (implies (common-divisor-p c (+ (- a) b) a)
           (integerp (* b (/ c))))
  :rule-classes ((:rewrite :match-free :all)))

;; gcd-is-common-divisor の補助定理
(defthm gcd-is-common-divisor-lemma-2
  (implies (common-divisor-p c (+ a (- b)) b)
           (integerp (* a (/ c))))
  :rule-classes ((:rewrite :match-free :all)))

;; (gcd$ n m) は n と m の公約数である
(defthm gcd-is-common-divisor
  (implies (and (natp n)
                (natp m))
           (common-divisor-p (gcd$ m n) n m)))

;; 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)))))