ACL2 で自然数の和の剰余と剰余同士の和の剰余の等しさを示す
目次
1. 注意
この記事はいま思うと ACL2 との付き合い方がよく分かっていなかったときに、 書いたものなので参考にしない方がいいです。 近々、本当に役に立つ初心者向けの記事を書く予定なので作成しだいここにリンクを張る予定です。
2. はじめに
ACL2 でうまく剰余に関する証明ができなくて苦戦していたのですが、 自然数の和の剰余に関する性質を一つ証明することまでは成功しました。
ACL2 の組込みの剰余関数である mod
, rem
をうまく使いこなせなかったため、
本記事では自然数同士の引き算によって剰余を求める nat-mod
関数を定義して、
自然数の剰余に関する定理を ACL2 で証明しました。
nat-mod
と ACL2 の mod
, rem
の関係を証明する方法については今後の課題とします。
nat-mod
と ACL2 の mod
について証明する方法が分かったため、
自然数を対象にする場合は nat-mod
と mod
が等しいことを証明しました。
なお、対象読者についてですが本記事はほぼ覚え書きの記事のため ACL2 - Introduction-to-the-theorem-prover を読み終えていることを前提ということにします。
本記事中のプログラムのライセンスは3条項BSDライセンスとします。
(equal (mod (+ (mod n1 m) (mod n2 m)) m) (mod (+ n1 n2) m))
を証明する感じになっていますが、実際には (equal (mod (+ n1 (mod n2 m)) m) (mod (+ n1 n2) m))
についての証明をしています。
タイトル詐欺になっていますがだいたい同じ話であり私の関心は後者にあるので後者を証明します。
3. リストの要素の和を求める関数を定義
リストの要素の和を求める関数を次のように定義します。
(defun sum (x) (if (endp x) 0 (+ (car x) (sum (cdr x)))))
出力を確認する (11行)
The admission of SUM is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). We observe that the type of SUM is described by the theorem (ACL2-NUMBERP (SUM X)). We used primitive type reasoning. Summary Form: ( DEFUN SUM ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) SUM
要素が全て自然数であった場合は総和も自然数であることを証明します。
(defthm natp-sum (implies (nat-listp x) (natp (sum x))) :rule-classes :forward-chaining)
証明成功: 出力を確認する (74行)
ACL2 Observation in ( DEFTHM NATP-SUM ...): The :TRIGGER-TERMS for the :FORWARD-CHAINING rule NATP-SUM will consist of the list containing (NAT-LISTP X). Splitter note (see :DOC splitter) for Goal (2 subgoals). if-intro: ((:DEFINITION NATP)) Subgoal 2 ([ A key checkpoint: Subgoal 2 (IMPLIES (NAT-LISTP X) (INTEGERP (SUM X))) *1 (Subgoal 2) is pushed for proof by induction. ]) Subgoal 1 ([ A key checkpoint: Subgoal 1 (IMPLIES (NAT-LISTP X) (<= 0 (SUM X))) Normally we would attempt to prove Subgoal 1 by induction. However, we prefer in this instance to focus on the original input conjecture rather than this simplified special case. We therefore abandon our previous work on this conjecture and reassign the name *1 to the original conjecture. (See :DOC otf-flg.) ]) Perhaps we can prove *1 by induction. Two induction schemes are suggested by this conjecture. These merge into one derived induction scheme. We will induct according to a scheme suggested by (SUM X). This suggestion was produced using the :induction rules NAT-LISTP and SUM. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit SUM. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 Subgoal *1/1' *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( DEFTHM NATP-SUM ...) Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER) (:DEFINITION ENDP) (:DEFINITION NAT-LISTP) (:DEFINITION NATP) (:DEFINITION NOT) (:DEFINITION SUM) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART NATP) (:EXECUTABLE-COUNTERPART SUM) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION NAT-LISTP) (:INDUCTION SUM) (:TYPE-PRESCRIPTION SUM)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 526 NATP-SUM
4. 自然数用の剰余関数 nat-mod
を定義
(nat-mod n m)
は n
から m
を n < m
になるまで減算し続ける関数です。
剰余をこの形で定義します。
(defun nat-mod (n m) (cond ((not (posp m)) 0) ((< (nfix n) m) (nfix n)) (t (nat-mod (- (nfix n) m) m))))
証明成功: 出力を確認する (50行)
For the admission of NAT-MOD we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT N). The non-trivial part of the measure conjecture is Goal (IMPLIES (AND (POSP M) (<= M (NFIX N))) (O< (ACL2-COUNT (+ (NFIX N) (- M))) (ACL2-COUNT N))). Goal' Splitter note (see :DOC splitter) for Goal' (2 subgoals). if-intro: ((:DEFINITION ACL2-COUNT) (:DEFINITION INTEGER-ABS) (:DEFINITION NFIX) (:DEFINITION O<)) Subgoal 2 Subgoal 1 Q.E.D. That completes the proof of the measure theorem for NAT-MOD. Thus, we admit this function under the principle of definition. We observe that the type of NAT-MOD is described by the theorem (AND (INTEGERP (NAT-MOD N M)) (<= 0 (NAT-MOD N M))). We used the :type- prescription rule NFIX. Summary Form: ( DEFUN NAT-MOD ...) Rules: ((:DEFINITION ACL2-COUNT) (:DEFINITION INTEGER-ABS) (:DEFINITION NFIX) (:DEFINITION NOT) (:DEFINITION O-FINP) (:DEFINITION O<) (:DEFINITION POSP) (:EXECUTABLE-COUNTERPART TAU-SYSTEM) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE DISTRIBUTIVITY-OF-MINUS-OVER-+) (:TYPE-PRESCRIPTION NFIX)) Splitter rules (see :DOC splitter): if-intro: ((:DEFINITION ACL2-COUNT) (:DEFINITION INTEGER-ABS) (:DEFINITION NFIX) (:DEFINITION O<)) Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 294 NAT-MOD
5. 自然数の和の剰余と剰余の和の剰余が等しいことを証明する
まず、剰余の和の剰余を求める (sum/nat-mod x m)
を定義します。
これは長さ n
のリスト x = '(N1 N2 ... Nn)
に対して、
(nat-mod (+ N1 (nat-mod (+ N2 (nat-mod ... (nat-mod (+ Nn 0) m) ... m) m) m) m) m)
を求める関数です。
リストの右端から m
で割った余り同士の和についてさらに
m
で割った余りを計算するというのを繰り返しています。
(defun sum/nat-mod (x m) (if (endp x) 0 (nat-mod (+ (car x) (sum/nat-mod (cdr x) m)) m)))
出力を確認する (13行)
The admission of SUM/NAT-MOD is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). We observe that the type of SUM/NAT-MOD is described by the theorem (AND (INTEGERP (SUM/NAT-MOD X M)) (<= 0 (SUM/NAT-MOD X M))). We used the :type-prescription rule NAT-MOD. Summary Form: ( DEFUN SUM/NAT-MOD ...) Rules: ((:TYPE-PRESCRIPTION NAT-MOD)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) SUM/NAT-MOD
(defthm sum/nat-mod-mod-sum (implies (and (nat-listp x) (posp m)) (equal (sum/nat-mod x m) (nat-mod (sum x) m))))
証明失敗: 出力を確認する (218行)
Goal' ([ A key checkpoint: Goal' (IMPLIES (AND (NAT-LISTP X) (INTEGERP M) (< 0 M)) (EQUAL (SUM/NAT-MOD X M) (NAT-MOD (SUM X) M))) *1 (Goal') is pushed for proof by induction. ]) Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. Subsumption reduces that number to two. These merge into one derived induction scheme. We will induct according to a scheme suggested by (SUM/NAT-MOD X M). This suggestion was produced using the :induction rules NAT-LISTP, SUM and SUM/NAT-MOD. If we let (:P M X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (:P M (CDR X))) (:P M X)) (IMPLIES (ENDP X) (:P M X))). This induction is justified by the same argument used to admit SUM/NAT-MOD. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 Subgoal *1/3' Subgoal *1/3'' Subgoal *1/3''' Subgoal *1/3'4' Subgoal *1/3'5' Subgoal *1/3'6' Subgoal *1/3'7' Subgoal *1/3'8' Subgoal *1/3'9' ([ A key checkpoint while proving *1 (descended from Goal'): Subgoal *1/3'' (IMPLIES (AND (CONSP X) (EQUAL (SUM/NAT-MOD (CDR X) M) (NAT-MOD (SUM (CDR X)) M)) (INTEGERP (CAR X)) (<= 0 (CAR X)) (NAT-LISTP (CDR X)) (INTEGERP M) (< 0 M)) (EQUAL (NAT-MOD (+ (CAR X) (SUM/NAT-MOD (CDR X) M)) M) (NAT-MOD (+ (CAR X) (SUM (CDR X))) M))) *1.1 (Subgoal *1/3'9') is pushed for proof by induction. ]) Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 Subgoal *1/1' So we now return to *1.1, which is (IMPLIES (AND (ACL2-NUMBERP SM) (INTEGERP X1) (<= 0 X1) (INTEGERP M) (< 0 M)) (EQUAL (NAT-MOD (+ X1 (NAT-MOD SM M)) M) (NAT-MOD (+ SM X1) M))). Subgoal *1.1/4 Subgoal *1.1/4' Subgoal *1.1/4'' Subgoal *1.1/4''' Subgoal *1.1/3 Subgoal *1.1/2 Subgoal *1.1/2' Splitter note (see :DOC splitter) for Subgoal *1.1/2' (5 subgoals). if-intro: ((:DEFINITION NAT-MOD) (:DEFINITION NFIX)) Subgoal *1.1/2.5 Subgoal *1.1/2.5' *1.1.1 (Subgoal *1.1/2.5') is pushed for proof by induction. Subgoal *1.1/2.4 Subgoal *1.1/2.4' *1.1.2 (Subgoal *1.1/2.4') is pushed for proof by induction. Subgoal *1.1/2.3 Subgoal *1.1/2.2 Subgoal *1.1/2.2' *1.1.3 (Subgoal *1.1/2.2') is pushed for proof by induction. Subgoal *1.1/2.1 *1.1.4 (Subgoal *1.1/2.1) is pushed for proof by induction. Subgoal *1.1/1 So we now return to *1.1.4, which is (IMPLIES (AND (INTEGERP M) (< 0 M) (< SM 0) (ACL2-NUMBERP SM) (INTEGERP X1) (<= 0 X1)) (EQUAL (NAT-MOD X1 M) (NAT-MOD (+ SM X1) M))). Subgoal *1.1.4/5 Subgoal *1.1.4/5' Subgoal *1.1.4/5'' Subgoal *1.1.4/5''' Subgoal *1.1.4/5'4' Subgoal *1.1.4/5'5' Subgoal *1.1.4/5'6' Subgoal *1.1.4/5'7' *1.1.4.1 (Subgoal *1.1.4/5'7') is pushed for proof by induction. Subgoal *1.1.4/4 Subgoal *1.1.4/3 Subgoal *1.1.4/2 Subgoal *1.1.4/2' Subgoal *1.1.4/2'' *1.1.4.2 (Subgoal *1.1.4/2'') is pushed for proof by induction. Subgoal *1.1.4/1 So we now return to *1.1.4.2, which is (IMPLIES (AND (INTEGERP M) (< 0 M) (< X1 M) (< SM 0) (ACL2-NUMBERP SM) (INTEGERP X1) (<= 0 X1)) (EQUAL X1 (NAT-MOD (+ SM X1) M))). No induction schemes are suggested by *1.1.4.2. Consequently, the proof attempt has failed. Summary Form: ( DEFTHM SUM/NAT-MOD-MOD-SUM ...) Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER) (:DEFINITION ENDP) (:DEFINITION FIX) (:DEFINITION NAT-LISTP) (:DEFINITION NAT-MOD) (:DEFINITION NATP) (:DEFINITION NFIX) (:DEFINITION NOT) (:DEFINITION POSP) (:DEFINITION SUM) (:DEFINITION SUM/NAT-MOD) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART NFIX) (:EXECUTABLE-COUNTERPART SUM) (:EXECUTABLE-COUNTERPART TAU-SYSTEM) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING ACL2-NUMBER-LISTP-FORWARD-TO-TRUE-LISTP) (:FORWARD-CHAINING INTEGER-LISTP-FORWARD-TO-RATIONAL-LISTP) (:FORWARD-CHAINING NAT-LISTP-FORWARD-TO-INTEGER-LISTP) (:FORWARD-CHAINING RATIONAL-LISTP-FORWARD-TO-ACL2-NUMBER-LISTP) (:INDUCTION NAT-LISTP) (:INDUCTION NAT-MOD) (:INDUCTION SUM) (:INDUCTION SUM/NAT-MOD) (:REWRITE ASSOCIATIVITY-OF-+) (:REWRITE COMMUTATIVITY-2-OF-+) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION ACL2-NUMBER-LISTP) (:TYPE-PRESCRIPTION INTEGER-LISTP) (:TYPE-PRESCRIPTION NAT-LISTP) (:TYPE-PRESCRIPTION NFIX) (:TYPE-PRESCRIPTION RATIONAL-LISTP) (:TYPE-PRESCRIPTION SUM)) Splitter rules (see :DOC splitter): if-intro: ((:DEFINITION NAT-MOD) (:DEFINITION NFIX)) Time: 0.04 seconds (prove: 0.03, print: 0.00, other: 0.00) Prover steps counted: 10833 --- The key checkpoint goals, below, may help you to debug this failure. See :DOC failure and see :DOC set-checkpoint-summary-limit. --- *** Key checkpoint at the top level: *** Goal' (IMPLIES (AND (NAT-LISTP X) (INTEGERP M) (< 0 M)) (EQUAL (SUM/NAT-MOD X M) (NAT-MOD (SUM X) M))) *** Key checkpoint under a top-level induction: *** Subgoal *1/3'' (IMPLIES (AND (CONSP X) (EQUAL (SUM/NAT-MOD (CDR X) M) (NAT-MOD (SUM (CDR X)) M)) (INTEGERP (CAR X)) (<= 0 (CAR X)) (NAT-LISTP (CDR X)) (INTEGERP M) (< 0 M)) (EQUAL (NAT-MOD (+ (CAR X) (SUM/NAT-MOD (CDR X) M)) M) (NAT-MOD (+ (CAR X) (SUM (CDR X))) M))) ACL2 Error in ( DEFTHM SUM/NAT-MOD-MOD-SUM ...): See :DOC failure. ******** FAILED ********
証明に失敗したので、まず Key checkpoint を確認します。
*** Key checkpoint under a top-level induction: *** Subgoal *1/3'' (IMPLIES (AND (CONSP X) (EQUAL (SUM/NAT-MOD (CDR X) M) (NAT-MOD (SUM (CDR X)) M)) (INTEGERP (CAR X)) (<= 0 (CAR X)) (NAT-LISTP (CDR X)) (INTEGERP M) (< 0 M)) (EQUAL (NAT-MOD (+ (CAR X) (SUM/NAT-MOD (CDR X) M)) M) (NAT-MOD (+ (CAR X) (SUM (CDR X))) M)))
Subgoal *1/3''
ですが、この式の帰結を
仮定 (EQUAL (SUM/NAT-MOD (CDR X) M) (NAT-MOD (SUM (CDR X)) M))
を用いて書き換えると
(EQUAL (NAT-MOD (+ (CAR X) (NAT-MOD (SUM (CDR X)) M)) M) (NAT-MOD (+ (CAR X) (SUM (CDR X))) M))
であり、これが真であることを仮定から導ければよさそうです。
そのために (nat-mod (+ n1 (nat-mod n2 m)) m)
と (nat-mod (+ n1 n2) m)
が等しいことを証明して ACL2 の Rewrite ルールに追加します。
(defthm add-nat-mod (implies (and (natp n1) (natp n2) (posp m)) (equal (nat-mod (+ n1 (nat-mod n2 m)) m) (nat-mod (+ n1 n2) m))))
証明成功: 出力を確認する (68行)
Goal' ([ A key checkpoint: Goal' (IMPLIES (AND (INTEGERP N1) (<= 0 N1) (INTEGERP N2) (<= 0 N2) (INTEGERP M) (< 0 M)) (EQUAL (NAT-MOD (+ N1 (NAT-MOD N2 M)) M) (NAT-MOD (+ N1 N2) M))) *1 (Goal') is pushed for proof by induction. ]) Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (NAT-MOD N2 M). This suggestion was produced using the :induction rule NAT-MOD. If we let (:P M N1 N2) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (POSP M) (<= M (NFIX N2)) (:P M N1 (+ (NFIX N2) (- M)))) (:P M N1 N2)) (IMPLIES (AND (POSP M) (< (NFIX N2) M)) (:P M N1 N2)) (IMPLIES (NOT (POSP M)) (:P M N1 N2))). This induction is justified by the same argument used to admit NAT-MOD. When applied to the goal at hand the above induction scheme produces five nontautological subgoals. Subgoal *1/5 Subgoal *1/5' Subgoal *1/5'' Subgoal *1/5''' Subgoal *1/4 Subgoal *1/3 Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 *1 is COMPLETED! Thus key checkpoint Goal' is COMPLETED! Q.E.D. Summary Form: ( DEFTHM ADD-NAT-MOD ...) Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER) (:DEFINITION NAT-MOD) (:DEFINITION NATP) (:DEFINITION NFIX) (:DEFINITION NOT) (:DEFINITION POSP) (:EXECUTABLE-COUNTERPART TAU-SYSTEM) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION NAT-MOD) (:REWRITE COMMUTATIVITY-2-OF-+) (:REWRITE COMMUTATIVITY-OF-+) (:TYPE-PRESCRIPTION NFIX)) Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) Prover steps counted: 2066 ADD-NAT-MOD
equal
の向きは逆にした方が若干筋が良い気がするのですが、
逆にした場合はルールを無効化してヒントを与えて使わないと Rewrite
ルールが再帰的に発動してしまって証明に失敗する問題があって面倒なのでこの向きにしています。
どちらでも sum/nat-mod-mod-sum
を証明するには十分です。
(defthm sum/nat-mod-mod-sum (implies (and (nat-listp x) (posp m)) (equal (sum/nat-mod x m) (nat-mod (sum x) m))))
証明成功: 出力を確認する (79行)
Goal' ([ A key checkpoint: Goal' (IMPLIES (AND (NAT-LISTP X) (INTEGERP M) (< 0 M)) (EQUAL (SUM/NAT-MOD X M) (NAT-MOD (SUM X) M))) *1 (Goal') is pushed for proof by induction. ]) Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. Subsumption reduces that number to two. These merge into one derived induction scheme. We will induct according to a scheme suggested by (SUM/NAT-MOD X M). This suggestion was produced using the :induction rules NAT-LISTP, SUM and SUM/NAT-MOD. If we let (:P M X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (:P M (CDR X))) (:P M X)) (IMPLIES (ENDP X) (:P M X))). This induction is justified by the same argument used to admit SUM/NAT-MOD. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 Subgoal *1/3' Subgoal *1/3'' Subgoal *1/3''' Subgoal *1/3'4' Subgoal *1/3'5' Subgoal *1/3'6' Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 Subgoal *1/1' *1 is COMPLETED! Thus key checkpoint Goal' is COMPLETED! Q.E.D. Summary Form: ( DEFTHM SUM/NAT-MOD-MOD-SUM ...) Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER) (:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER) (:DEFINITION ENDP) (:DEFINITION NAT-LISTP) (:DEFINITION NAT-MOD) (:DEFINITION NATP) (:DEFINITION NOT) (:DEFINITION POSP) (:DEFINITION SUM) (:DEFINITION SUM/NAT-MOD) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART NFIX) (:EXECUTABLE-COUNTERPART SUM) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING ACL2-NUMBER-LISTP-FORWARD-TO-TRUE-LISTP) (:FORWARD-CHAINING INTEGER-LISTP-FORWARD-TO-RATIONAL-LISTP) (:FORWARD-CHAINING NAT-LISTP-FORWARD-TO-INTEGER-LISTP) (:FORWARD-CHAINING NATP-SUM) (:FORWARD-CHAINING RATIONAL-LISTP-FORWARD-TO-ACL2-NUMBER-LISTP) (:INDUCTION NAT-LISTP) (:INDUCTION SUM) (:INDUCTION SUM/NAT-MOD) (:REWRITE ADD-NAT-MOD) (:TYPE-PRESCRIPTION ACL2-NUMBER-LISTP) (:TYPE-PRESCRIPTION INTEGER-LISTP) (:TYPE-PRESCRIPTION NAT-LISTP) (:TYPE-PRESCRIPTION RATIONAL-LISTP) (:TYPE-PRESCRIPTION SUM)) Time: 0.02 seconds (prove: 0.02, print: 0.00, other: 0.00) Prover steps counted: 3275 SUM/NAT-MOD-MOD-SUM
証明に成功しました。
6. ACL2 の mod と nat-mod が等しいことを証明する
Frequently-asked-questions-by-newcomers を読んでいたところ、
mod
や floor
のような非線形な関数を使用する場合は (include-book "arithmetic-5/top" :dir :system)
を使うとよいとありました。自然数を対象にする場合に nat-mod
と mod
が等しいことを証明してみます。
まず、 arithmetic-5/top
という book を読み込みます。
(local (include-book "arithmetic-5/top" :dir :system))
ACL2 Observation in NON-LINEAR-ARITHMETIC: To turn on non-linear arithmetic, execute : (SET-DEFAULT-HINTS '((NONLINEARP-DEFAULT-HINT STABLE-UNDER-SIMPLIFICATIONP HIST PSPV))) or : (SET-DEFAULT-HINTS '((NONLINEARP-DEFAULT-HINT++ ID STABLE-UNDER-SIMPLIFICATIONP HIST NIL))) See the README for more about non-linear arithmetic and general information about using this library. Summary Form: ( INCLUDE-BOOK "arithmetic-5/top" ...) Rules: NIL Time: 0.34 seconds (prove: 0.00, print: 0.00, other: 0.34) "/gnu/store/c61q2c0mwv0hgqdnd4piazls5ykzy9yr-acl2-8.4/lib/acl2/books/arithmetic-5/top.lisp"
非線形算術のヒントを有効にする方法が出力されたのでその通りに実行します。
(set-default-hints '((nonlinearp-default-hint stable-under-simplificationp hist pspv)))
((NONLINEARP-DEFAULT-HINT STABLE-UNDER-SIMPLIFICATIONP HIST PSPV))
nat-mod
と mod
が等しいことの証明を試みます。
(defthm nat-mod-mod (implies (and (natp n) (posp m)) (equal (nat-mod n m) (mod n m))))
証明成功: 出力を確認する (91行)
Goal' ACL2 Observation in NONLINEARP-DEFAULT-HINT: We now enable non-linear arithmetic. ACL2 Observation in NONLINEARP-DEFAULT-HINT: We now disable non-linear arithmetic. Subgoal 2 ACL2 Observation in NONLINEARP-DEFAULT-HINT: We now disable non-linear arithmetic. Subgoal 1 Subgoal 1' Splitter note (see :DOC splitter) for Subgoal 1' (2 subgoals). if-intro: ((:DEFINITION NOT)) Subgoal 1.2 Subgoal 1.2' Subgoal 1.2'' ACL2 Observation in NONLINEARP-DEFAULT-HINT: We now enable non-linear arithmetic. ([ A key checkpoint: Goal' (IMPLIES (AND (INTEGERP N) (<= 0 N) (INTEGERP M) (< 0 M)) (EQUAL (NAT-MOD N M) (MOD N M))) Normally we would attempt to prove Subgoal 1.2'' by induction. However, we prefer in this instance to focus on the original input conjecture rather than this simplified special case. We therefore abandon our previous work on this conjecture and reassign the name *1 to the original conjecture. (See :DOC otf-flg.) ]) Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (NAT-MOD N M). This suggestion was produced using the :induction rule NAT-MOD. If we let (:P M N) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (POSP M) (<= M (NFIX N)) (:P M (+ (NFIX N) (- M)))) (:P M N)) (IMPLIES (AND (POSP M) (< (NFIX N) M)) (:P M N)) (IMPLIES (NOT (POSP M)) (:P M N))). This induction is justified by the same argument used to admit NAT-MOD. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 Subgoal *1/1' *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( DEFTHM NAT-MOD-MOD ...) Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER) (:DEFINITION NAT-MOD) (:DEFINITION NATP) (:DEFINITION NFIX) (:DEFINITION NOT) (:DEFINITION POSP) (:DEFINITION SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION NAT-MOD) (:REWRITE |(* a (/ a))|) (:REWRITE |(+ 0 x)|) (:REWRITE |(+ x (- x))|) (:REWRITE |(+ y x)|) (:REWRITE BUBBLE-DOWN-+-MATCH-3) (:REWRITE CANCEL-MOD-+) (:REWRITE MOD-X-Y-=-X . 3) (:REWRITE NORMALIZE-ADDENDS) (:REWRITE PREFER-POSITIVE-ADDENDS-<) (:REWRITE REMOVE-WEAK-INEQUALITIES)) Time: 0.10 seconds (prove: 0.10, print: 0.00, other: 0.00) Prover steps counted: 5300 NAT-MOD-MOD
問題なく証明に成功しました。
ACL2 で mod
に関する定理を証明する場合には、基本的に arithmetic-5/top
book
を使うのがよさそうです。
7. おわりに
ACL2 で剰余の性質を証明するのに苦戦していたのですが、これで一歩進むことはできました。 剰余まわりの証明を ACL2 でうまくやる方法についてご存知の方がいたら教えてください。
(include-book "arithmetic-5/top" :dir :system)
を使うのがよいと分かりました。