日記
自己紹介
開発
RSS
連絡先

ACL2 でリストの回転に関する性質を証明してみた

目次

投稿日: 2022-03-24 木
ACL2

注意

[2023-02-05 Sun]

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

はじめに

ACL2 を使いこなせるようになるための練習問題として、 リストの回転に関する定理を証明してみます。

ここでいう回転とはリストの最初の要素を最後に移動する操作のことです。 なお、空リストを回転させた場合の結果は空リストとします。

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

回転操作 rotate 関数の定義

関数 rotate を定義します。 guard 機能により真リストでない値を受けつけないようにしています。 

(defun rotate (x)
  (declare (xargs :guard (true-listp x)))
  (if (endp x)
      nil
      (append (rest x)
              (list (first x)))))
出力を確認する 

Since ROTATE is non-recursive, its admission is trivial.  We observe
that the type of ROTATE is described by the theorem (TRUE-LISTP (ROTATE X)).
We used primitive type reasoning and the :type-prescription rules 
BINARY-APPEND and TRUE-LISTP-APPEND.

Computing the guard conjecture for ROTATE....

The guard conjecture for ROTATE is trivial to prove, given primitive
type reasoning.  ROTATE is compliant with Common Lisp.

Summary
Form:  ( DEFUN ROTATE ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION BINARY-APPEND)
        (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 ROTATE

ACL2 では再帰的でない関数を定義してしまうと、 in-theory という機能で関数を disable して証明時に関数を展開しない限り、 rotate に関連する定理にマッチしなくなるという問題があります。 今回定理を証明するときに出力される [Non-rec] という警告はこれについてのものです。

これを回避したい場合は必要な定理を準備したあとに関数を展開しないようにするとか、 そもそも関数じゃなくてマクロを使うという方法があるのですが、 今回は rotate に関する定理の使用ではなくて定理の証明が主な目的なのでとりあえず気にしないこととします。

回転操作をしても長さが変わらないことを示す

リストの回転操作によってリストの長さが変わるわけがありません。 長さが変わらないことを示す定理 len-rotate を定義します。 

(defthm len-rotate
  (equal (len (rotate x))
         (len x)))
証明失敗: 出力を確認する 

ACL2 Warning [Non-rec] in ( DEFTHM LEN-ROTATE ...):  A :REWRITE rule
generated from LEN-ROTATE will be triggered only by terms containing
the function symbol ROTATE, which has a non-recursive definition. 
Unless this definition is disabled, this rule is unlikely ever to be
used.


Splitter note (see :DOC splitter) for Goal (2 subgoals).
  if-intro: ((:DEFINITION ROTATE))

Subgoal 2
Subgoal 2'
Subgoal 2''
Subgoal 2'''

([ A key checkpoint:

Subgoal 2'
(IMPLIES (CONSP X)
         (EQUAL (LEN (APPEND (CDR X) (LIST (CAR X))))
                (+ 1 (LEN (CDR X)))))

Normally we would attempt to prove Subgoal 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 (LEN X).  This suggestion
was produced using the :induction rule LEN.  If we let (:P X) denote
*1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P X))
     (IMPLIES (AND (CONSP X) (:P (CDR X)))
              (:P X))).
This induction is justified by the same argument used to admit LEN.
When applied to the goal at hand the above induction scheme produces
two nontautological subgoals.
Subgoal *1/2
Subgoal *1/1

Splitter note (see :DOC splitter) for Subgoal *1/1 (2 subgoals).
  if-intro: ((:DEFINITION ROTATE))

Subgoal *1/1.2
Subgoal *1/1.2'
Subgoal *1/1.2''
Subgoal *1/1.2'''
Subgoal *1/1.2'4'
Subgoal *1/1.2'5'

([ A key checkpoint while proving *1 (descended from Goal):

Subgoal *1/1.2'
(IMPLIES (AND (CONSP X)
              (CONSP (CDR X))
              (EQUAL (LEN (APPEND (CDDR X) (LIST (CADR X))))
                     (+ 1 (LEN (CDDR X)))))
         (EQUAL (+ 1
                   (LEN (APPEND (CDDR X) (LIST (CAR X)))))
                (+ 2 (LEN (CDDR X)))))

*1.1 (Subgoal *1/1.2'5') is pushed for proof by induction.

])
Subgoal *1/1.1

So we now return to *1.1, which is

(IMPLIES (AND (INTEGERP I)
              (<= 0 I)
              (EQUAL (LEN (APPEND X4 (LIST X3)))
                     (+ 1 I)))
         (EQUAL (+ 1 (LEN (APPEND X4 (LIST X1))))
                (+ 2 I))).
Subgoal *1.1/3
Subgoal *1.1/3'
Subgoal *1.1/3''
Subgoal *1.1/3'''
Subgoal *1.1/3'4'
Subgoal *1.1/3'5'

*1.1.1 (Subgoal *1.1/3'5') is pushed for proof by induction.
Subgoal *1.1/2
Subgoal *1.1/2'
Subgoal *1.1/2''
Subgoal *1.1/2'''
Subgoal *1.1/2'4'
Subgoal *1.1/2'5'
Subgoal *1.1/2'6'
Subgoal *1.1/2'7'
Subgoal *1.1/2'8'
Subgoal *1.1/2'9'

*1.1.2 (Subgoal *1.1/2'9') is pushed for proof by induction.
Subgoal *1.1/1
Subgoal *1.1/1'
Subgoal *1.1/1''

So we now return to *1.1.2, which is

(IMPLIES (AND (INTEGERP I) (<= 0 I))
         (EQUAL (+ 2 (LEN (APPEND X6 (LIST X1))))
                (+ 2 I))).
Subgoal *1.1.2/2
Subgoal *1.1.2/2'
Subgoal *1.1.2/2''
Subgoal *1.1.2/2'''
Subgoal *1.1.2/2'4'
Subgoal *1.1.2/2'5'
Subgoal *1.1.2/2'6'
Subgoal *1.1.2/2'7'
Subgoal *1.1.2/2'8'
Subgoal *1.1.2/2'9'

A goal of NIL, Subgoal *1.1.2/2'9', has been generated!  Obviously,
the proof attempt has failed.

Summary
Form:  ( DEFTHM LEN-ROTATE ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION LEN)
        (:DEFINITION NOT)
        (:DEFINITION ROTATE)
        (:DEFINITION SYNP)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION BINARY-APPEND)
        (:INDUCTION LEN)
        (:REWRITE CDR-CONS)
        (:REWRITE FOLD-CONSTS-IN-+)
        (:TYPE-PRESCRIPTION BINARY-APPEND)
        (:TYPE-PRESCRIPTION LEN)
        (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION ROTATE))
Warnings:  Non-rec
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
Prover steps counted:  5549

---
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
<GOAL>

*** Key checkpoint under a top-level induction
    before generating a goal of NIL (see :DOC nil-goal): ***

Subgoal *1/1.2'
(IMPLIES (AND (CONSP X)
              (CONSP (CDR X))
              (EQUAL (LEN (APPEND (CDDR X) (LIST (CADR X))))
                     (+ 1 (LEN (CDDR X)))))
         (EQUAL (+ 1
                   (LEN (APPEND (CDDR X) (LIST (CAR X)))))
                (+ 2 (LEN (CDDR X)))))

ACL2 Error in ( DEFTHM LEN-ROTATE ...):  See :DOC failure.

******** FAILED ********

自動証明に失敗してしまいました。 Subgoal *1/1.2' に (LEN (APPEND (CDDR X) (LIST (CAR X)))) とあることに注目しましょう。 (len (append x y)) は (+ (len x) (len y)) と明らかに同じです。 これを示す定理 len-append を定義します。 

(defthm len-append
  (equal (len (append x y))
         (+ (len x) (len y))))
証明成功: 出力を確認する 

*1 (the initial Goal, a key checkpoint) is pushed for proof by induction.

Perhaps we can prove *1 by induction.  Three induction schemes are
suggested by this conjecture.  These merge into two derived induction
schemes.  However, one of these is flawed and so we are left with one
viable candidate.  

We will induct according to a scheme suggested by (LEN X), but modified
to accommodate (APPEND X Y).  These suggestions were produced using
the :induction rules BINARY-APPEND and LEN.  If we let (:P X Y) denote
*1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P X Y))
     (IMPLIES (AND (CONSP X) (:P (CDR X) Y))
              (:P X Y))).
This induction is justified by the same argument used to admit LEN.
When applied to the goal at hand the above induction scheme produces
two nontautological subgoals.
Subgoal *1/2
Subgoal *1/1

*1 is COMPLETED!
Thus key checkpoint Goal is COMPLETED!

Q.E.D.

Summary
Form:  ( DEFTHM LEN-APPEND ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION FIX)
        (:DEFINITION LEN)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION BINARY-APPEND)
        (:INDUCTION LEN)
        (:REWRITE CDR-CONS)
        (:REWRITE COMMUTATIVITY-2-OF-+)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE UNICITY-OF-0)
        (:TYPE-PRESCRIPTION LEN))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  316
 LEN-APPEND

自動証明に成功しました。 この状態で再度 len-rotate 定理の証明を試みます。 

(defthm len-rotate
  (equal (len (rotate x))
         (len x)))
証明成功: 出力を確認する 

ACL2 Warning [Non-rec] in ( DEFTHM LEN-ROTATE ...):  A :REWRITE rule
generated from LEN-ROTATE will be triggered only by terms containing
the function symbol ROTATE, which has a non-recursive definition. 
Unless this definition is disabled, this rule is unlikely ever to be
used.


Splitter note (see :DOC splitter) for Goal (2 subgoals).
  if-intro: ((:DEFINITION ROTATE))

Subgoal 2
Subgoal 2'
Subgoal 1
Subgoal 1'

Q.E.D.

Summary
Form:  ( DEFTHM LEN-ROTATE ...)
Rules: ((:DEFINITION LEN)
        (:DEFINITION NOT)
        (:DEFINITION ROTATE)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART LEN)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CDR-CONS)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE LEN-APPEND))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION ROTATE))
Warnings:  Non-rec
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  184
 LEN-ROTATE

今度は証明に成功しました。 len-rotate の証明の鍵は len-append にありました。

回転操作をしても元のリストの部分集合であることを示す

リストを回転しているだけなので新しい要素が追加されることはありえません。 このことを証明してみましょう。 

(defthm subsetp-rotate
  (subsetp (rotate x) x))
証明失敗: 出力を確認する 

ACL2 Warning [Non-rec] in ( DEFTHM SUBSETP-ROTATE ...):  A :REWRITE
rule generated from SUBSETP-ROTATE will be triggered only by terms
containing the function symbol ROTATE, which has a non-recursive definition.
Unless this definition is disabled, this rule is unlikely ever to be
used.

Goal'

Splitter note (see :DOC splitter) for Goal' (2 subgoals).
  if-intro: ((:DEFINITION ROTATE))

Subgoal 2
Subgoal 2'
Subgoal 2''

([ A key checkpoint:

Subgoal 2
(IMPLIES (CONSP X)
         (SUBSETP-EQUAL (APPEND (CDR X) (LIST (CAR X)))
                        X))

Normally we would attempt to prove Subgoal 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.)

])

No induction schemes are suggested by *1.  Consequently, the proof
attempt has failed.

Summary
Form:  ( DEFTHM SUBSETP-ROTATE ...)
Rules: ((:DEFINITION RETURN-LAST)
        (:DEFINITION ROTATE)
        (:DEFINITION SUBSETP-EQL-EXEC$GUARD-CHECK)
        (:ELIM CAR-CDR-ELIM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION ROTATE))
Warnings:  Non-rec
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  454

---
The key checkpoint goal, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---

*** Key checkpoint before reverting to proof by induction: ***

Subgoal 2
(IMPLIES (CONSP X)
         (SUBSETP-EQUAL (APPEND (CDR X) (LIST (CAR X)))
                        X))

ACL2 Error in ( DEFTHM SUBSETP-ROTATE ...):  See :DOC failure.

******** FAILED ********

自動証明に失敗しました。 Subgoal 2 の (SUBSETP-EQUAL (APPEND (CDR X) (LIST (CAR X))) X) に注目しましょう。 (subsetp (append x y) z) は (and (subsetp x z) (subsetp y z)) であると言い換えることができます。

このことを subsetp-append という名前の定理として ACL2 に教えてあげましょう。 

(defthm subsetp-append
  (equal (subsetp (append x y) z)
         (and (subsetp x z)
              (subsetp y z))))
証明成功: 出力を確認する 
Goal'
Subgoal 2

([ A key checkpoint:

Subgoal 2
(IMPLIES (SUBSETP-EQUAL X Z)
         (EQUAL (SUBSETP-EQUAL (APPEND X Y) Z)
                (SUBSETP-EQUAL Y Z)))

*1 (Subgoal 2) is pushed for proof by induction.

])
Subgoal 1
Subgoal 1'

([ A key checkpoint:

Subgoal 1'
(IMPLIES (NOT (SUBSETP-EQUAL X Z))
         (NOT (SUBSETP-EQUAL (APPEND X Y) Z)))

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.  Three induction schemes are
suggested by this conjecture.  These merge into two derived induction
schemes.  However, one of these is flawed and so we are left with one
viable candidate.  

We will induct according to a scheme suggested by (SUBSETP-EQUAL X Z),
but modified to accommodate (APPEND X Y).  These suggestions were produced
using the :induction rules BINARY-APPEND and SUBSETP-EQUAL.  If we
let (:P X Y Z) denote *1 above then the induction scheme we'll use
is
(AND (IMPLIES (AND (NOT (ENDP X))
                   (NOT (MEMBER-EQUAL (CAR X) Z)))
              (:P X Y Z))
     (IMPLIES (AND (NOT (ENDP X))
                   (MEMBER-EQUAL (CAR X) Z)
                   (:P (CDR X) Y Z))
              (:P X Y Z))
     (IMPLIES (ENDP X) (:P X Y Z))).
This induction is justified by the same argument used to admit SUBSETP-EQUAL.
When applied to the goal at hand the above induction scheme produces
three nontautological subgoals.
Subgoal *1/3
Subgoal *1/3'
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 SUBSETP-APPEND ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION SUBSETP-EQUAL)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION BINARY-APPEND)
        (:INDUCTION SUBSETP-EQUAL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION MEMBER-EQUAL)
        (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  1425
 SUBSETP-APPEND

なんら問題なく証明できました。 それでは、再度 subset-rotate の証明を試みましょう。 

(defthm subsetp-rotate
  (subsetp (rotate x) x))
証明失敗: 出力を確認する 

ACL2 Warning [Non-rec] in ( DEFTHM SUBSETP-ROTATE ...):  A :REWRITE
rule generated from SUBSETP-ROTATE will be triggered only by terms
containing the function symbol ROTATE, which has a non-recursive definition.
Unless this definition is disabled, this rule is unlikely ever to be
used.

Goal'

Splitter note (see :DOC splitter) for Goal' (2 subgoals).
  if-intro: ((:DEFINITION ROTATE))

Subgoal 2
Subgoal 2'
Subgoal 2''
Subgoal 2'''

([ A key checkpoint:

Subgoal 2'
(IMPLIES (CONSP X)
         (SUBSETP-EQUAL (CDR X) X))

Normally we would attempt to prove Subgoal 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.)

])

No induction schemes are suggested by *1.  Consequently, the proof
attempt has failed.

Summary
Form:  ( DEFTHM SUBSETP-ROTATE ...)
Rules: ((:DEFINITION MEMBER-EQUAL)
        (:DEFINITION RETURN-LAST)
        (:DEFINITION ROTATE)
        (:DEFINITION SUBSETP-EQL-EXEC$GUARD-CHECK)
        (:DEFINITION SUBSETP-EQUAL)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE SUBSETP-APPEND)
        (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION ROTATE))
Warnings:  Non-rec
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  439

---
The key checkpoint goal, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---

*** Key checkpoint before reverting to proof by induction: ***

Subgoal 2'
(IMPLIES (CONSP X)
         (SUBSETP-EQUAL (CDR X) X))

ACL2 Error in ( DEFTHM SUBSETP-ROTATE ...):  See :DOC failure.

******** FAILED ********

また証明に失敗しましたが、だいぶ簡単になってきました。 (cdr x) が x の部分集合であることは自明なように思いますが、 ACL2 的にはそうではないようです。 そもそも ACL2 は初期状態だと (subsetp x x) すら自明ではありません。 これは ACL2 - Introductory-challenge-problem-2 という ACL2 のチュートリアルの問題で知りました。

というわけで (subsetp x x) であることを示します。 ただ、これは ACL2 - Introductory-challenge-problem-2 の解答になってしまうので、ACL2 の勉強中の人は見ないようにしてください。

折り畳んだ部分で、下記の定理を証明しています。 

(defthm subsetp-reflexive
  (subsetp x x))
(subsetp x x)の証明(Introductory-challenge-problem-2 の解答のため閲覧注意！) 
(defthm subsetp-reflexive
  (subsetp x x))
証明失敗: 出力を確認する 
Goal'

([ A key checkpoint:

Goal'
(SUBSETP-EQUAL X X)

*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 (SUBSETP-EQUAL X X).
This suggestion was produced using the :induction rule SUBSETP-EQUAL.
If we let (:P X) denote *1 above then the induction scheme we'll use
is
(AND (IMPLIES (AND (NOT (ENDP X))
                   (NOT (MEMBER-EQUAL (CAR X) X)))
              (:P X))
     (IMPLIES (AND (NOT (ENDP X))
                   (MEMBER-EQUAL (CAR X) X)
                   (:P (CDR X)))
              (:P X))
     (IMPLIES (ENDP X) (:P X))).
This induction is justified by the same argument used to admit SUBSETP-EQUAL.
When applied to the goal at hand the above induction scheme produces
three nontautological subgoals.
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/2''
Subgoal *1/2'''
Subgoal *1/2'4'

([ A key checkpoint while proving *1 (descended from Goal'):

Subgoal *1/2''
(IMPLIES (AND (CONSP X)
              (SUBSETP-EQUAL (CDR X) (CDR X)))
         (SUBSETP-EQUAL (CDR X) X))

*1.1 (Subgoal *1/2'4') is pushed for proof by induction.

])
Subgoal *1/1
Subgoal *1/1'

So we now return to *1.1, which is

(IMPLIES (SUBSETP-EQUAL X2 X2)
         (SUBSETP-EQUAL X2 (CONS X1 X2))).
Subgoal *1.1/4
Subgoal *1.1/4'
Subgoal *1.1/3
Subgoal *1.1/3'

Splitter note (see :DOC splitter) for Subgoal *1.1/3' (2 subgoals).
  if-intro: ((:DEFINITION MEMBER-EQUAL))

Subgoal *1.1/3.2
Subgoal *1.1/3.2'
Subgoal *1.1/3.2''

*1.1.1 (Subgoal *1.1/3.2'') is pushed for proof by induction.
Subgoal *1.1/3.1
Subgoal *1.1/3.1'
Subgoal *1.1/3.1''

*1.1.2 (Subgoal *1.1/3.1'') is pushed for proof by induction.
Subgoal *1.1/2
Subgoal *1.1/2'

Splitter note (see :DOC splitter) for Subgoal *1.1/2' (2 subgoals).
  if-intro: ((:DEFINITION MEMBER-EQUAL))

Subgoal *1.1/2.2
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
Subgoal *1.1/2.1'
Subgoal *1.1/2.1''

*1.1.4 (Subgoal *1.1/2.1'') is pushed for proof by induction.
Subgoal *1.1/1
Subgoal *1.1/1'

So we now return to *1.1.4, which is

(IMPLIES (AND (LIST* X1 X3 X4)
              (NOT (SUBSETP-EQUAL X4 X4))
              (SUBSETP-EQUAL X4 (CONS X3 X4)))
         (SUBSETP-EQUAL X4 (LIST* X1 X3 X4))).

The formula above is subsumed by one of its parents, *1, which we're
in the process of trying to prove by induction.  When an inductive
proof pushes a subgoal for induction that is less general than the
original goal, it may be a sign that either an inappropriate induction
was chosen or that the original goal is insufficiently general.  In
any case, our proof attempt has failed.

Summary
Form:  ( DEFTHM SUBSETP-REFLEXIVE ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION MEMBER-EQUAL)
        (:DEFINITION NOT)
        (:DEFINITION RETURN-LAST)
        (:DEFINITION SUBSETP-EQL-EXEC$GUARD-CHECK)
        (:DEFINITION SUBSETP-EQUAL)
        (:ELIM CAR-CDR-ELIM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SUBSETP-EQUAL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION MEMBER-EQUAL))
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  5331

---
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'
(SUBSETP-EQUAL X X)

*** Key checkpoint under a top-level induction: ***

Subgoal *1/2''
(IMPLIES (AND (CONSP X)
              (SUBSETP-EQUAL (CDR X) (CDR X)))
         (SUBSETP-EQUAL (CDR X) X))

ACL2 Error in ( DEFTHM SUBSETP-REFLEXIVE ...):  See :DOC failure.

******** FAILED ********

Subgoal *1/2'' では (subsetp-equal (cdr x) (cdr x)) のときに、 (subsetp-equal (cdr x) x) とあるので、これを証明しましょう。

こういうのが証明できないのは、 subsetp の引数に両方 x を入れてしまっているせいで、 帰納法による証明がうまくいかないのが原因なので一般化してしまうのがよいです。 subsetp の第一引数 (cdr x) を x, 第二引数の x を y とおいて下記のように、 subsetp-cdr という定理を示しましょう。 

(defthm subsetp-cdr
  (implies (subsetp x (cdr y))
           (subsetp x y)))
証明成功: 出力を確認する 
Goal'
Subgoal 2
Subgoal 1
Subgoal 1'

([ A key checkpoint:

Goal'
(IMPLIES (SUBSETP-EQUAL X (CDR Y))
         (SUBSETP-EQUAL X Y))

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 (SUBSETP-EQUAL X Y).
This suggestion was produced using the :induction rule SUBSETP-EQUAL.
If we let (:P X Y) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP X))
                   (NOT (MEMBER-EQUAL (CAR X) Y)))
              (:P X Y))
     (IMPLIES (AND (NOT (ENDP X))
                   (MEMBER-EQUAL (CAR X) Y)
                   (:P (CDR X) Y))
              (:P X Y))
     (IMPLIES (ENDP X) (:P X Y))).
This induction is justified by the same argument used to admit SUBSETP-EQUAL.
When applied to the goal at hand the above induction scheme produces
three nontautological subgoals.
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'

*1 is COMPLETED!
Thus key checkpoint Goal is COMPLETED!

Q.E.D.

The storage of SUBSETP-CDR depends upon the :type-prescription rule
SUBSETP-EQUAL.

Summary
Form:  ( DEFTHM SUBSETP-CDR ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION MEMBER-EQUAL)
        (:DEFINITION NOT)
        (:DEFINITION SUBSETP-EQUAL)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SUBSETP-EQUAL)
        (:REWRITE DEFAULT-CDR)
        (:TYPE-PRESCRIPTION MEMBER-EQUAL)
        (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  1051
 SUBSETP-CDR

再度 subsetp-reflexive の証明を試みます。 

(defthm subsetp-reflexive
  (subsetp x x))
証明成功: 出力を確認する 
Goal'

([ A key checkpoint:

Goal'
(SUBSETP-EQUAL X X)

*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 (SUBSETP-EQUAL X X).
This suggestion was produced using the :induction rule SUBSETP-EQUAL.
If we let (:P X) denote *1 above then the induction scheme we'll use
is
(AND (IMPLIES (AND (NOT (ENDP X))
                   (NOT (MEMBER-EQUAL (CAR X) X)))
              (:P X))
     (IMPLIES (AND (NOT (ENDP X))
                   (MEMBER-EQUAL (CAR X) X)
                   (:P (CDR X)))
              (:P X))
     (IMPLIES (ENDP X) (:P X))).
This induction is justified by the same argument used to admit SUBSETP-EQUAL.
When applied to the goal at hand the above induction scheme produces
three nontautological subgoals.
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'

*1 is COMPLETED!
Thus key checkpoint Goal' is COMPLETED!

Q.E.D.

The storage of SUBSETP-REFLEXIVE depends upon the :type-prescription
rule SUBSETP-EQUAL.

Summary
Form:  ( DEFTHM SUBSETP-REFLEXIVE ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION MEMBER-EQUAL)
        (:DEFINITION NOT)
        (:DEFINITION RETURN-LAST)
        (:DEFINITION SUBSETP-EQL-EXEC$GUARD-CHECK)
        (:DEFINITION SUBSETP-EQUAL)
        (:EXECUTABLE-COUNTERPART CDR)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SUBSETP-EQUAL)
        (:REWRITE DEFAULT-CDR)
        (:REWRITE SUBSETP-CDR)
        (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  400
 SUBSETP-REFLEXIVE

では、再び subsetp-rotate の証明を試みます。 

(defthm subsetp-rotate
  (subsetp (rotate x) x))
証明成功: 出力を確認する 

ACL2 Warning [Non-rec] in ( DEFTHM SUBSETP-ROTATE ...):  A :REWRITE
rule generated from SUBSETP-ROTATE will be triggered only by terms
containing the function symbol ROTATE, which has a non-recursive definition.
Unless this definition is disabled, this rule is unlikely ever to be
used.

Goal'

Splitter note (see :DOC splitter) for Goal' (2 subgoals).
  if-intro: ((:DEFINITION ROTATE))

Subgoal 2
Subgoal 1

Q.E.D.

The storage of SUBSETP-ROTATE depends upon the :type-prescription rule
SUBSETP-EQUAL.

Summary
Form:  ( DEFTHM SUBSETP-ROTATE ...)
Rules: ((:DEFINITION MEMBER-EQUAL)
        (:DEFINITION RETURN-LAST)
        (:DEFINITION ROTATE)
        (:DEFINITION SUBSETP-EQL-EXEC$GUARD-CHECK)
        (:DEFINITION SUBSETP-EQUAL)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART SUBSETP-EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE DEFAULT-CDR)
        (:REWRITE SUBSETP-APPEND)
        (:REWRITE SUBSETP-CDR)
        (:REWRITE SUBSETP-REFLEXIVE)
        (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION ROTATE))
Warnings:  Non-rec
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  466
 SUBSETP-ROTATE

今度は成功しました。 これで、回転操作によって新しい要素が入ることはないということを示すことができました。

元のリストは回転操作したものの部分集合であることを示す

回転操作によって新しい要素が入らないことを示しましたが、 元々あった要素が消えてしまうということもありえません。

よって、 (subsetp x (rotate x)) であるはずです。

これを subsetp-rotate-flip と命名し、証明しましょう。 

(defthm subsetp-rotate-flip
  (subsetp x (rotate x)))
証明失敗: 出力を確認する 

ACL2 Warning [Non-rec] in ( DEFTHM SUBSETP-ROTATE-FLIP ...):  A :REWRITE
rule generated from SUBSETP-ROTATE-FLIP will be triggered only by terms
containing the function symbol ROTATE, which has a non-recursive definition.
Unless this definition is disabled, this rule is unlikely ever to be
used.

Goal'

Splitter note (see :DOC splitter) for Goal' (2 subgoals).
  if-intro: ((:DEFINITION ROTATE))

Subgoal 2

Splitter note (see :DOC splitter) for Subgoal 2 (2 subgoals).
  if-intro: ((:DEFINITION SUBSETP-EQUAL))

Subgoal 2.2
Subgoal 2.2'
Subgoal 2.2''

([ A key checkpoint:

Subgoal 2.2
(IMPLIES (CONSP X)
         (MEMBER-EQUAL (CAR X)
                       (APPEND (CDR X) (LIST (CAR X)))))

Normally we would attempt to prove Subgoal 2.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 
(SUBSETP-EQUAL X (ROTATE X)).  This suggestion was produced using the
:induction rule SUBSETP-EQUAL.  If we let (:P X) denote *1 above then
the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X))
                   (NOT (MEMBER-EQUAL (CAR X) (ROTATE X))))
              (:P X))
     (IMPLIES (AND (NOT (ENDP X))
                   (MEMBER-EQUAL (CAR X) (ROTATE X))
                   (:P (CDR X)))
              (:P X))
     (IMPLIES (ENDP X) (:P X))).
This induction is justified by the same argument used to admit SUBSETP-EQUAL.
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'

([ A key checkpoint while proving *1 (descended from Goal):

Subgoal *1/3''
(IMPLIES (CONSP X)
         (MEMBER-EQUAL (CAR X)
                       (APPEND (CDR X) (LIST (CAR X)))))

*1.1 (Subgoal *1/3'4') is pushed for proof by induction.

])
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/2''
Subgoal *1/2'''
Subgoal *1/2'4'
Subgoal *1/2'5'
Subgoal *1/2'6'
Subgoal *1/2'7'
Subgoal *1/2'8'

([ A key checkpoint while proving *1 (descended from Goal):

Subgoal *1/2'5'
(IMPLIES (AND (CONSP X)
              (NOT (EQUAL (CAR X) (CADR X)))
              (MEMBER-EQUAL (CAR X)
                            (APPEND (CDDR X) (LIST (CAR X))))
              (CONSP (CDR X))
              (MEMBER-EQUAL (CADR X)
                            (APPEND (CDDR X) (LIST (CADR X))))
              (SUBSETP-EQUAL (CDDR X)
                             (APPEND (CDDR X) (LIST (CADR X)))))
         (SUBSETP-EQUAL (CDDR X)
                        (CONS (CADR X)
                              (APPEND (CDDR X) (LIST (CAR X))))))

*1.2 (Subgoal *1/2'8') is pushed for proof by induction.

])
Subgoal *1/1
Subgoal *1/1'

So we now return to *1.2, which is

(IMPLIES (AND (CONSP L)
              (TRUE-LISTP L)
              (CONSP LST)
              (TRUE-LISTP LST)
              (NOT (EQUAL X1 X3))
              (MEMBER-EQUAL X1 LST)
              (MEMBER-EQUAL X3 L)
              (SUBSETP-EQUAL X4 L))
         (SUBSETP-EQUAL X4 (CONS X3 LST))).
Subgoal *1.2/6
Subgoal *1.2/6'
Subgoal *1.2/6''
Subgoal *1.2/6'''
Subgoal *1.2/6'4'

*1.2.1 (Subgoal *1.2/6'4') is pushed for proof by induction.
Subgoal *1.2/5
Subgoal *1.2/5'
Subgoal *1.2/4
Subgoal *1.2/3
Subgoal *1.2/3'
Subgoal *1.2/3''
Subgoal *1.2/2
Subgoal *1.2/2'
Subgoal *1.2/2''
Subgoal *1.2/2'''
Subgoal *1.2/2'4'

*1.2.2 (Subgoal *1.2/2'4') is pushed for proof by induction.
Subgoal *1.2/1

So we now return to *1.2.2, which is

(IMPLIES (AND (CONSP L)
              (TRUE-LISTP L)
              (TRUE-LISTP LST2)
              (NOT (EQUAL LST1 X3))
              (MEMBER-EQUAL X3 L)
              (SUBSETP-EQUAL X4 L))
         (SUBSETP-EQUAL X4 (LIST* X3 LST1 LST2))).
Subgoal *1.2.2/4
Subgoal *1.2.2/4'
Subgoal *1.2.2/4''
Subgoal *1.2.2/4'''
Subgoal *1.2.2/4'4'

*1.2.2.1 (Subgoal *1.2.2/4'4') is pushed for proof by induction.
Subgoal *1.2.2/3
Subgoal *1.2.2/3'
Subgoal *1.2.2/2
Subgoal *1.2.2/2'
Subgoal *1.2.2/1
Subgoal *1.2.2/1'

So we now return to *1.2.2.1, which is

(IMPLIES (AND (NOT (EQUAL X5 X3))
              (NOT (EQUAL X5 LST1))
              (NOT (MEMBER-EQUAL X5 LST2))
              (CONSP L)
              (TRUE-LISTP L)
              (TRUE-LISTP LST2)
              (NOT (EQUAL LST1 X3))
              (MEMBER-EQUAL X3 L)
              (MEMBER-EQUAL X5 L))
         (NOT (SUBSETP-EQUAL X6 L))).
Subgoal *1.2.2.1/3
Subgoal *1.2.2.1/3'
Subgoal *1.2.2.1/3''

*1.2.2.1.1 (Subgoal *1.2.2.1/3'') is pushed for proof by induction.
Subgoal *1.2.2.1/2
Subgoal *1.2.2.1/1

So we now return to *1.2.2.1.1, which is

(IMPLIES (AND (NOT (EQUAL X5 X3))
              (NOT (EQUAL X5 LST1))
              (CONSP L)
              (TRUE-LISTP L)
              (NOT (EQUAL LST1 X3))
              (MEMBER-EQUAL X3 L)
              (MEMBER-EQUAL X5 L))
         (NOT (SUBSETP-EQUAL X6 L))).
Subgoal *1.2.2.1.1/3
Subgoal *1.2.2.1.1/3'
Subgoal *1.2.2.1.1/2
Subgoal *1.2.2.1.1/2'
Subgoal *1.2.2.1.1/1
Subgoal *1.2.2.1.1/1'
Subgoal *1.2.2.1.1/1''
Subgoal *1.2.2.1.1/1'''

*1.2.2.1.1.1 (Subgoal *1.2.2.1.1/1''') is pushed for proof by induction.

So we now return to *1.2.2.1.1.1, which is

(IMPLIES (AND (NOT (EQUAL X5 X3))
              (NOT (EQUAL X5 LST1))
              (CONSP L)
              (TRUE-LISTP L)
              (NOT (EQUAL LST1 X3))
              (MEMBER-EQUAL X3 L))
         (NOT (MEMBER-EQUAL X5 L))).
Subgoal *1.2.2.1.1.1/6
Subgoal *1.2.2.1.1.1/6'
Subgoal *1.2.2.1.1.1/5
Subgoal *1.2.2.1.1.1/5'
Subgoal *1.2.2.1.1.1/5''
Subgoal *1.2.2.1.1.1/5'''
Subgoal *1.2.2.1.1.1/5'4'
Subgoal *1.2.2.1.1.1/5'5'

*1.2.2.1.1.1.1 (Subgoal *1.2.2.1.1.1/5'5') is pushed for proof by induction.
Subgoal *1.2.2.1.1.1/4
Subgoal *1.2.2.1.1.1/3
Subgoal *1.2.2.1.1.1/3'

Splitter note (see :DOC splitter) for Subgoal *1.2.2.1.1.1/3' (2 subgoals).
  if-intro: ((:DEFINITION MEMBER-EQUAL))

Subgoal *1.2.2.1.1.1/3.2
Subgoal *1.2.2.1.1.1/3.1
Subgoal *1.2.2.1.1.1/2
Subgoal *1.2.2.1.1.1/2'
Subgoal *1.2.2.1.1.1/2''
Subgoal *1.2.2.1.1.1/2'''
Subgoal *1.2.2.1.1.1/2'4'

*1.2.2.1.1.1.2 (Subgoal *1.2.2.1.1.1/2'4') is pushed for proof by induction.
Subgoal *1.2.2.1.1.1/1

So we now return to *1.2.2.1.1.1.2, which is

(IMPLIES (AND (NOT (EQUAL L1 X3))
              (NOT (EQUAL L1 LST1))
              (TRUE-LISTP L2)
              (NOT (EQUAL LST1 X3)))
         (NOT (MEMBER-EQUAL X3 L2))).
Subgoal *1.2.2.1.1.1.2/4
Subgoal *1.2.2.1.1.1.2/4'
Subgoal *1.2.2.1.1.1.2/3
Subgoal *1.2.2.1.1.1.2/2
Subgoal *1.2.2.1.1.1.2/2'
Subgoal *1.2.2.1.1.1.2/2''
Subgoal *1.2.2.1.1.1.2/2'''
Subgoal *1.2.2.1.1.1.2/2'4'
Subgoal *1.2.2.1.1.1.2/2'5'

A goal of NIL, Subgoal *1.2.2.1.1.1.2/2'5', has been generated!  Obviously,
the proof attempt has failed.

Summary
Form:  ( DEFTHM SUBSETP-ROTATE-FLIP ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION MEMBER-EQUAL)
        (:DEFINITION NOT)
        (:DEFINITION RETURN-LAST)
        (:DEFINITION ROTATE)
        (:DEFINITION SUBSETP-EQL-EXEC$GUARD-CHECK)
        (:DEFINITION SUBSETP-EQUAL)
        (:DEFINITION TRUE-LISTP)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION MEMBER-EQUAL)
        (:INDUCTION SUBSETP-EQUAL)
        (:INDUCTION TRUE-LISTP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE SUBSETP-CDR)
        (:TYPE-PRESCRIPTION BINARY-APPEND)
        (:TYPE-PRESCRIPTION MEMBER-EQUAL)
        (:TYPE-PRESCRIPTION SUBSETP-EQUAL)
        (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION MEMBER-EQUAL)
             (:DEFINITION ROTATE)
             (:DEFINITION SUBSETP-EQUAL))
Warnings:  Non-rec
Time:  0.05 seconds (prove: 0.04, print: 0.01, other: 0.00)
Prover steps counted:  19772

---
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
<GOAL>

*** Key checkpoints under a top-level induction
    before generating a goal of NIL (see :DOC nil-goal): ***

Subgoal *1/3''
(IMPLIES (CONSP X)
         (MEMBER-EQUAL (CAR X)
                       (APPEND (CDR X) (LIST (CAR X)))))

Subgoal *1/2'5'
(IMPLIES (AND (CONSP X)
              (NOT (EQUAL (CAR X) (CADR X)))
              (MEMBER-EQUAL (CAR X)
                            (APPEND (CDDR X) (LIST (CAR X))))
              (CONSP (CDR X))
              (MEMBER-EQUAL (CADR X)
                            (APPEND (CDDR X) (LIST (CADR X))))
              (SUBSETP-EQUAL (CDDR X)
                             (APPEND (CDDR X) (LIST (CADR X)))))
         (SUBSETP-EQUAL (CDDR X)
                        (CONS (CADR X)
                              (APPEND (CDDR X) (LIST (CAR X))))))

ACL2 Error in ( DEFTHM SUBSETP-ROTATE-FLIP ...):  See :DOC failure.

******** FAILED ********

失敗しました。

Subgoal *1/2'5' に (subsetp x (cons e) (append x y)) という構造があることに着目しましょう。 どう考えてもこれは自明なので、これを subsetp-cons-append と命名し証明します。 

(defthm subsetp-cons-append
  (subsetp x (cons e (append x y))))
証明成功: 出力を確認する 
Goal'

([ A key checkpoint:

Goal'
(SUBSETP-EQUAL X (CONS E (APPEND X Y)))

*1 (Goal') is pushed for proof by induction.

])

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 
(SUBSETP-EQUAL X (CONS E (APPEND X Y))), but modified to accommodate
(APPEND X Y).  These suggestions were produced using the :induction
rules BINARY-APPEND and SUBSETP-EQUAL.  If we let (:P E X Y) denote
*1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X))
                   (NOT (MEMBER-EQUAL (CAR X)
                                      (CONS E (APPEND X Y)))))
              (:P E X Y))
     (IMPLIES (AND (NOT (ENDP X))
                   (MEMBER-EQUAL (CAR X)
                                 (CONS E (APPEND X Y)))
                   (:P E (CDR X) Y))
              (:P E X Y))
     (IMPLIES (ENDP X) (:P E X Y))).
This induction is justified by the same argument used to admit SUBSETP-EQUAL.
When applied to the goal at hand the above induction scheme produces
three nontautological subgoals.
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/2''
Subgoal *1/2'''
Subgoal *1/2'4'
Subgoal *1/2'5'
Subgoal *1/2'6'

([ A key checkpoint while proving *1 (descended from Goal'):

Subgoal *1/2'''
(IMPLIES (AND (CONSP X)
              (NOT (EQUAL (CAR X) E))
              (CONS (CAR X) (APPEND (CDR X) Y))
              (SUBSETP-EQUAL (CDR X)
                             (CONS E (APPEND (CDR X) Y))))
         (SUBSETP-EQUAL (CDR X)
                        (LIST* E (CAR X) (APPEND (CDR X) Y))))

*1.1 (Subgoal *1/2'6') is pushed for proof by induction.

])
Subgoal *1/1
Subgoal *1/1'

So we now return to *1.1, which is

(IMPLIES (AND (NOT (EQUAL X1 E))
              (CONS X1 BAD)
              (SUBSETP-EQUAL X2 (CONS E BAD)))
         (SUBSETP-EQUAL X2 (LIST* E X1 BAD))).
Subgoal *1.1/4
Subgoal *1.1/4'
Subgoal *1.1/3
Subgoal *1.1/3'
Subgoal *1.1/2
Subgoal *1.1/2'
Subgoal *1.1/1
Subgoal *1.1/1'

*1.1 and *1 are COMPLETED!
Thus key checkpoints Subgoal *1/2''' and Goal' are COMPLETED!

Q.E.D.

The storage of SUBSETP-CONS-APPEND depends upon the :type-prescription
rule SUBSETP-EQUAL.

Summary
Form:  ( DEFTHM SUBSETP-CONS-APPEND ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION MEMBER-EQUAL)
        (:DEFINITION NOT)
        (:DEFINITION RETURN-LAST)
        (:DEFINITION SUBSETP-EQL-EXEC$GUARD-CHECK)
        (:DEFINITION SUBSETP-EQUAL)
        (:ELIM CAR-CDR-ELIM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION BINARY-APPEND)
        (:INDUCTION SUBSETP-EQUAL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE SUBSETP-CDR)
        (:TYPE-PRESCRIPTION MEMBER-EQUAL)
        (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
Prover steps counted:  8486
 SUBSETP-CONS-APPEND

subsetp-cons-append は問題なく証明できました。 この証明で地味に subsetp-cdr が使われていますね。 補助定理を書くことで問題としている領域に関する ACL2 の 自動証明の力が増していくのは ACL2 の強みです。

それでは、 subsetp-rotate-flip の証明を再度試みます。 

(defthm subsetp-rotate-flip
  (subsetp x (rotate x)))
証明成功: 出力を確認する 

ACL2 Warning [Non-rec] in ( DEFTHM SUBSETP-ROTATE-FLIP ...):  A :REWRITE
rule generated from SUBSETP-ROTATE-FLIP will be triggered only by terms
containing the function symbol ROTATE, which has a non-recursive definition.
Unless this definition is disabled, this rule is unlikely ever to be
used.

Goal'

Splitter note (see :DOC splitter) for Goal' (2 subgoals).
  if-intro: ((:DEFINITION ROTATE))

Subgoal 2

Splitter note (see :DOC splitter) for Subgoal 2 (2 subgoals).
  if-intro: ((:DEFINITION SUBSETP-EQUAL))

Subgoal 2.2
Subgoal 2.2'
Subgoal 2.2''

([ A key checkpoint:

Subgoal 2.2
(IMPLIES (CONSP X)
         (MEMBER-EQUAL (CAR X)
                       (APPEND (CDR X) (LIST (CAR X)))))

Normally we would attempt to prove Subgoal 2.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 
(SUBSETP-EQUAL X (ROTATE X)).  This suggestion was produced using the
:induction rule SUBSETP-EQUAL.  If we let (:P X) denote *1 above then
the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X))
                   (NOT (MEMBER-EQUAL (CAR X) (ROTATE X))))
              (:P X))
     (IMPLIES (AND (NOT (ENDP X))
                   (MEMBER-EQUAL (CAR X) (ROTATE X))
                   (:P (CDR X)))
              (:P X))
     (IMPLIES (ENDP X) (:P X))).
This induction is justified by the same argument used to admit SUBSETP-EQUAL.
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'

([ A key checkpoint while proving *1 (descended from Goal):

Subgoal *1/3''
(IMPLIES (CONSP X)
         (MEMBER-EQUAL (CAR X)
                       (APPEND (CDR X) (LIST (CAR X)))))

*1.1 (Subgoal *1/3'4') is pushed for proof by induction.

])
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/2''
Subgoal *1/2'''
Subgoal *1/1
Subgoal *1/1'

So we now return to *1.1, which is

(MEMBER-EQUAL X1 (APPEND X2 (LIST X1))).
Subgoal *1.1/2
Subgoal *1.1/2'
Subgoal *1.1/2''
Subgoal *1.1/1
Subgoal *1.1/1'
Subgoal *1.1/1''

*1.1 and *1 are COMPLETED!
Thus key checkpoints Subgoal *1/3'' and Goal are COMPLETED!

Q.E.D.

The storage of SUBSETP-ROTATE-FLIP depends upon the :type-prescription
rule SUBSETP-EQUAL.

Summary
Form:  ( DEFTHM SUBSETP-ROTATE-FLIP ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION MEMBER-EQUAL)
        (:DEFINITION NOT)
        (:DEFINITION ROTATE)
        (:DEFINITION SUBSETP-EQUAL)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION BINARY-APPEND)
        (:INDUCTION SUBSETP-EQUAL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE SUBSETP-CDR)
        (:REWRITE SUBSETP-CONS-APPEND)
        (:TYPE-PRESCRIPTION BINARY-APPEND)
        (:TYPE-PRESCRIPTION MEMBER-EQUAL)
        (:TYPE-PRESCRIPTION SUBSETP-EQUAL)
        (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Warnings:  Non-rec
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  2600
 SUBSETP-ROTATE-FLIP

成功しました。 subsetp-rotate と組み合わせると、 (rotate x) をしても、 元のリスト x の要素から新しいのが増えることも、 要素が減ることもないということを証明できました。

TODO リストの長さと同じ回数回転すると元のリストと一致することを証明する

最後に結構な難問を考えてみましょう。 リストと同じ回数回転したら元のリストと同じになるはずです。

まずは、n 回リストを回転する rotate-n を定義しましょう。 

(defun rotate-n (x n)
  (if (zp n)
      x
      (rotate-n (rotate x) (1- n))))
出力を確認する 

The admission of ROTATE-N 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 N).  We observe that the type of ROTATE-N is described
by the theorem (OR (TRUE-LISTP (ROTATE-N X N)) (EQUAL (ROTATE-N X N) X)).
We used the :type-prescription rule ROTATE.

Summary
Form:  ( DEFUN ROTATE-N ...)
Rules: ((:TYPE-PRESCRIPTION ROTATE))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 ROTATE-N

一応再帰関数で停止性の証明が必要なのですが、 この程度の自明なものでは特になにもしなくても ACL2 が自動証明してくれます。

では、 (equal (rotate-n x (len x)) x) を証明してみましょう。 これは rotate-return と名づけることとします。 

(defthm rotate-return
  (equal (rotate-n x (len x)) x))
証明失敗: 出力を確認する 

*1 (the initial Goal, a key checkpoint) 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 (LEN X).  This suggestion
was produced using the :induction rule LEN.  If we let (:P X) denote
*1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P X))
     (IMPLIES (AND (CONSP X) (:P (CDR X)))
              (:P X))).
This induction is justified by the same argument used to admit LEN.
When applied to the goal at hand the above induction scheme produces
two nontautological subgoals.
Subgoal *1/2
Subgoal *1/1
Subgoal *1/1'
Subgoal *1/1''
Subgoal *1/1'''
Subgoal *1/1'4'
Subgoal *1/1'5'
Subgoal *1/1'6'

([ A key checkpoint while proving *1 (descended from Goal):

Subgoal *1/1'
(IMPLIES (AND (CONSP X)
              (EQUAL (ROTATE-N (CDR X) (LEN (CDR X)))
                     (CDR X)))
         (EQUAL (ROTATE-N (APPEND (CDR X) (LIST (CAR X)))
                          (LEN (CDR X)))
                X))

*1.1 (Subgoal *1/1'6') is pushed for proof by induction.

])

So we now return to *1.1, which is

(IMPLIES (AND (INTEGERP I) (<= 0 I))
         (EQUAL (ROTATE-N (APPEND X2 (LIST X1)) I)
                (CONS X1 (ROTATE-N X2 I)))).
Subgoal *1.1/4
Subgoal *1.1/4'

Splitter note (see :DOC splitter) for Subgoal *1.1/4' (2 subgoals).
  if-intro: ((:DEFINITION ROTATE))

Subgoal *1.1/4.2
Subgoal *1.1/4.2'
Subgoal *1.1/4.2''
Subgoal *1.1/4.2'''
Subgoal *1.1/4.2'4'
Subgoal *1.1/4.2'5'
Subgoal *1.1/4.2'6'

*1.1.1 (Subgoal *1.1/4.2'6') is pushed for proof by induction.
Subgoal *1.1/4.1
Subgoal *1.1/3
Subgoal *1.1/2
Subgoal *1.1/1
Subgoal *1.1/1'
Subgoal *1.1/1''

*1.1.2 (Subgoal *1.1/1'') is pushed for proof by induction.

So we now return to *1.1.2, which is

(EQUAL (APPEND X2 (LIST X1))
       (CONS X1 X2)).
Subgoal *1.1.2/2
Subgoal *1.1.2/2'
Subgoal *1.1.2/2''
Subgoal *1.1.2/2'''
Subgoal *1.1.2/2'4'

*1.1.2.1 (Subgoal *1.1.2/2'4') is pushed for proof by induction.
Subgoal *1.1.2/1
Subgoal *1.1.2/1'
Subgoal *1.1.2/1''
Subgoal *1.1.2/1'''

A goal of NIL, Subgoal *1.1.2/1''', has been generated!  Obviously,
the proof attempt has failed.

Summary
Form:  ( DEFTHM ROTATE-RETURN ...)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION FIX)
        (:DEFINITION LEN)
        (:DEFINITION NOT)
        (:DEFINITION ROTATE)
        (:DEFINITION ROTATE-N)
        (:DEFINITION SYNP)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART INTEGERP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION BINARY-APPEND)
        (:INDUCTION LEN)
        (:INDUCTION ROTATE-N)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE CONS-EQUAL)
        (:REWRITE FOLD-CONSTS-IN-+)
        (:REWRITE UNICITY-OF-0)
        (:TYPE-PRESCRIPTION BINARY-APPEND)
        (:TYPE-PRESCRIPTION LEN)
        (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION ROTATE))
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
Prover steps counted:  5676

---
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
(EQUAL (ROTATE-N X (LEN X)) X)

*** Key checkpoint under a top-level induction
    before generating a goal of NIL (see :DOC nil-goal): ***

Subgoal *1/1'
(IMPLIES (AND (CONSP X)
              (EQUAL (ROTATE-N (CDR X) (LEN (CDR X)))
                     (CDR X)))
         (EQUAL (ROTATE-N (APPEND (CDR X) (LIST (CAR X)))
                          (LEN (CDR X)))
                X))

ACL2 Error in ( DEFTHM ROTATE-RETURN ...):  See :DOC failure.

******** FAILED ********

ACL2 は次のような帰納法を試してます。

  • x が空リストの場合に真か
  • (cdr x) のときに真のとき x のときも真か

今回は2番目で失敗しました。 ぱっと見よさそうな考えのように見えるのですが、 式を見た感じこのまま解けそうにありません。 というわけで、上記の帰納法の適用は諦めて別の方法を模索することにしました。

……と模索していたら半日くらい経過してしまったため一旦諦めます！

しばらく考えたところ rotate によってリスト上の要素の位置の変化を追跡するような定理を書いて、 丁度 (len x) 回したときに位置の変化がなくなることを示すような方法でいけるかと思ったのですが泥沼にはまりました。

もしも解決したら記事を更新しようと思います。

おわりに

2022/03/24 現在では、リストの長さと同じ回数回転すると元のリストと一致するという、 重要な性質を証明できずに終わってしまいましたが、 まあ補助定理を良い感じに書くことでそこそこ性質を証明できることを確認しました。 ウォーミングアップ的に ACL2 を使ってみたという感じなんで、いきなり重いのは無理でした。すみません。

この記事を読んで「我こそはその問題を解いてみせよう！」と思った人は、 是非 ACL2 を始めてみてください。

著者: Masaya Tojo

Mastodon: @tojoqk

RSS を購読する

トップページに戻る