ACL2 で自然数の和の剰余と剰余同士の和の剰余の等しさを示す

目次

投稿日: 2022-06-27 月

1. 注意

[2023-02-05 日]

この記事はいま思うと ACL2 との付き合い方がよく分かっていなかったときに、 書いたものなので参考にしない方がいいです。 近々、本当に役に立つ初心者向けの記事を書く予定なので作成しだいここにリンクを張る予定です。

2. はじめに

ACL2 でうまく剰余に関する証明ができなくて苦戦していたのですが、 自然数の和の剰余に関する性質を一つ証明することまでは成功しました。

ACL2 の組込みの剰余関数である mod, rem をうまく使いこなせなかったため、 本記事では自然数同士の引き算によって剰余を求める nat-mod 関数を定義して、 自然数の剰余に関する定理を ACL2 で証明しました。 nat-mod と ACL2 の mod, rem の関係を証明する方法については今後の課題とします。

[2022-07-08 金] 追記: nat-mod と ACL2 の mod について証明する方法が分かったため、 自然数を対象にする場合は nat-modmod が等しいことを証明しました。

なお、対象読者についてですが本記事はほぼ覚え書きの記事のため ACL2 - Introduction-to-the-theorem-prover を読み終えていることを前提ということにします。

本記事中のプログラムのライセンスは3条項BSDライセンスとします。

<2022-06-27 月 18:30> 追記: タイトルには「ACL2で自然数の和の剰余と剰余同士の和の剰余の等しさを示す」とあるので、このタイトルからは (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 から mn < 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 が等しいことを証明する

[2022-07-08 金] 追記: ACL2 のチュートリアル中の Frequently-asked-questions-by-newcomers を読んでいたところ、 modfloor のような非線形な関数を使用する場合は (include-book "arithmetic-5/top" :dir :system) を使うとよいとありました。自然数を対象にする場合に nat-modmod が等しいことを証明してみます。

まず、 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-modmod が等しいことの証明を試みます。

(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 でうまくやる方法についてご存知の方がいたら教えてください。

[2022-07-08 金] 追記: 剰余まわりの証明を ACL2 でうまくやるには (include-book "arithmetic-5/top" :dir :system) を使うのがよいと分かりました。

著者: Masaya Tojo

Mastodon: @tojoqk

RSS を購読する

トップページに戻る