From 39e473ca059c50cd0f4e4606ddd78969eaed46be Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Sun, 15 Aug 2021 01:37:37 +0900 Subject: consecutive-fibonacci-numbers-are-coprime: Gcd$ is common-divisor. --- consecutive-fibonacci-numbers-are-coprime.lisp | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/consecutive-fibonacci-numbers-are-coprime.lisp b/consecutive-fibonacci-numbers-are-coprime.lisp index 1700e8e..5b807a4 100644 --- a/consecutive-fibonacci-numbers-are-coprime.lisp +++ b/consecutive-fibonacci-numbers-are-coprime.lisp @@ -31,6 +31,29 @@ (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)) -- cgit v1.2.3