From edb50e14f937d58c50dc72ea4af81330fdafdfde Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sun, 25 Jul 2021 17:09:59 +0900
Subject: divisor-list: 約数リストに関する定理を追加
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 divisor-list.lisp | 111 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 111 insertions(+)
 create mode 100644 divisor-list.lisp

(limited to 'divisor-list.lisp')

diff --git a/divisor-list.lisp b/divisor-list.lisp
new file mode 100644
index 0000000..21cbb10
--- /dev/null
+++ b/divisor-list.lisp
@@ -0,0 +1,111 @@
+;;; divisor-list.lisp: 約数に関する証明
+
+;; e が x の約数であるかどうかを調べる述語
+(defmacro divisorp (e x)
+  `(integerp (/ ,x ,e)))
+
+;; n の約数のリストを作る
+(defun divisors-1 (n i)
+  (cond
+    ((zp i) nil)
+    ((divisorp i n)
+     (cons i (divisors-1 n (1- i))))
+    (t
+     (divisors-1 n (1- i)))))
+
+(defmacro divisors (n)
+  `(divisors-1 ,n ,n))
+
+;; x が n の約数のリストかどうかを調べる述語
+(defun divisor-listp (x n)
+  (cond
+    ((endp x) (null x))
+    (t (and (divisorp (car x) n)
+            (divisor-listp (cdr x) n)))))
+
+;; 約数リストは真リストであることを示す定理
+(defthm divisor-listp-to-true-listp
+  (implies (divisor-listp x n)
+           (true-listp x))
+  :rule-classes :forward-chaining)
+
+;; divisors の結果は約数リストである
+(defthm divisor-listp-divisors-1
+  (implies (and (natp n)
+                (posp m))
+           (divisor-listp (divisors-1 n m) n)))
+
+(defthm divisor-listp-divisors
+  (implies (posp n)
+           (divisor-listp (divisors n) n)))
+
+;; 正数 x について x - 1 が正数でないとき x は 1
+(defthm posp-and-not-posp-n-1
+  (implies (posp n)
+           (iff (not (posp (+ -1 n)))
+                (equal n 1))))
+
+;; divisorp-implies-member-divisors-1 の補助定理
+(defthm divisorp-implies-member-divisors-1-lemma
+  (implies (and (natp n)
+                (posp m)
+                (not (posp (+ -1 m))))
+           (integerp (* (/ m) n)))
+  :hints (("Goal" :in-theory (disable posp-and-not-posp-n-1)
+                  :use (:instance posp-and-not-posp-n-1
+                                  (n m)))))
+
+;; e (e <= n) が n の約数のとき (divisors n) に
+;; e が含まれている
+(defthm divisorp-implies-member-divisors-1
+  (implies (and (natp n)
+                (posp m)
+                (posp e)
+                (<= e m))
+           (implies (divisorp e n)
+                    (member e (divisors-1 n m))))
+  :hints (("Goal" :in-theory (disable posp-and-not-posp-n-1)
+                  :use (:instance posp-and-not-posp-n-1
+                                  (n m)))))
+
+(defthm divisorp-implies-member-divisors
+  (implies (and (posp n)
+                (posp e)
+                (<= e n))
+           (implies (divisorp e n)
+                    (member e (divisors n)))))
+
+;; (divisors n) に e が含まれているとき、
+;; e は n の約数
+(defthm member-divisors-1-implies-divisorp
+  (implies (and (natp n)
+                (posp m)
+                (posp e)
+                (member e (divisors-1 n m)))
+           (divisorp e n)))
+
+(defthm member-divisors-implies-divisorp
+  (implies (and (posp n)
+                (posp e))
+           (implies (member e (divisors n))
+                    (divisorp e n)))
+  :hints (("Goal" :in-theory (disable
+                              member-divisors-1-implies-divisorp)
+                  :use ((:instance member-divisors-1-implies-divisorp
+                                   (n n)
+                                   (m n)
+                                   (e e))))))
+
+;; (divisors n) に e (<= n) が含まれていることは
+;; e が n の約数であることの
+;; 必要十分条件である
+(defthm member-divisors-iff-divisorp
+  (implies (and (posp n)
+                (posp e)
+                (<= e n))
+           (iff (member e (divisors n))
+                (divisorp e n)))
+  :hints (("Goal" :in-theory (disable member-divisors-implies-divisorp)
+                  :use ((:instance member-divisors-implies-divisorp
+                                   (n n)
+                                   (e e))))))
-- 
cgit v1.2.3