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

## はじめに

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

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

## 回転操作 `rotate` 関数の定義

```(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 ********
```

```(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
```

```(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
```

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

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

```(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 ********
```

このことを `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
```

```(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))
(APPEND (CDDR X) (LIST (CADR X))))
(SUBSETP-EQUAL (CDDR X)
(APPEND (CDDR X) (LIST (CADR X)))))
(SUBSETP-EQUAL (CDDR 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))
(APPEND (CDDR X) (LIST (CADR X))))
(SUBSETP-EQUAL (CDDR X)
(APPEND (CDDR X) (LIST (CADR X)))))
(SUBSETP-EQUAL (CDDR 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))
(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
```

## 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
```

では、 `(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 のときも真か

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

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

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

## おわりに

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

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