From 0cad8821900e6df09c3e0702ad6f922d697a2d05 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sun, 25 Jul 2021 17:13:05 +0900
Subject: consecutive-fibonacci-numbers-are-coprime:
 隣り合うフィボナッチ数が互いに素であることの定理を追加
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

n# Your branch is ahead of 'origin/master' by 1 commit.
---
 consecutive-fibonacci-numbers-are-coprime.lisp | 33 ++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 consecutive-fibonacci-numbers-are-coprime.lisp

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)))))
-- 
cgit v1.2.3