consecutive-fibonacci-numbers-are-coprime: 隣り合うフィボナッチ数が互いに素であることの定理を追加

n# Your branch is ahead of 'origin/master' by 1 commit.

1 files changed, 33 insertions, 0 deletions

diff --git a/consecutive-fibonacci-numbers-are-coprime.lisp b/consecutive-fibonacci-numbers-are-coprime.lisp
new file mode 100644
index 0000000..d80ce43
--- /dev/null
+++ b/consecutive-fibonacci-numbers-are-coprime.lisp
@@ -0,0 +1,33 @@
+;; consecutive-fibonacci-numbers-are-coprime.lisp: 隣り合うフィボナッチ数は互いに素である
+
+;; 数字を足したり引いたりする関数に関する証明をするときに便利な Book
+(include-book "arithmetic/top-with-meta" :dir :system)
+
+;; フィボナッチ関数の定義
+(defun fibonacci (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))))
+  (cond
+    ((or (not (posp n))
+         (not (posp m))
+         (= (nfix n) (nfix m)))
+     n)
+    ((< n m) (gcd$ (- m n) n))
+    (t (gcd$ (- n m) 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)))))