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

## 注意

[2023-02-05 Sun]

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

## はじめに

これは私が過去に書いた https://git.tojo.tokyo/acl2-theorems.git/tree/palindrome-sandwich.lisp を記事にして解説したものです。 このプログラムを作成した 2021/07/19 の当時と比べると ACL2 の扱いに少し慣れてきているためプログラムを修正しています。

## 回文の何について証明したいのか

1. 「リスト `x``y` について、 `x` が回文のとき `y``(reverse y)``x` を挟んだリスト `(append y x (reverse y))` は回文である」
2. 「リスト `x``y` について、 `y``(reverse y)` で挟んだリスト `(append y x (reverse y))` が回文であることと、 `x` が回文であることは等しい」

1番目の定理の逆は 「 `(append y x (reverse y))` が回文であるとき `x` は回文である」であり 2番目の定理は1番目に加えて1番目の逆も示したものとなっています。

この性質の1番目はある日買い物をして家に帰っている途中に気づきました。謎です。 ACL2 を使って証明を試みている途中に逆も成立することに気づきました。

`palindromep` は下記のように定義していて、 `reverse` した結果と `x` が等しいときに回文であると見做します。

```(defmacro palindromep (x)
`(equal (reverse ,x) ,x))
```

```
Summary
Form:  ( DEFMACRO PALINDROMEP ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
PALINDROMEP
```

## 準備: `reverse` 関数を `rev` 関数に変換する

ACL2 では `(reverse x)` 関数は `(revappend x nil)` と定義されています。 詳細は下記の `:doc reverse` を確認してください。

```:doc reverse
```

```Parents: LISTS, STRINGS and ACL2-BUILT-INS.

Reverse a list or string

(Reverse x) is the result of reversing the order of the elements of
the list or string x.

The [guard] for reverse requires that its argument is a true list or
a string.

Reverse is defined in Common Lisp.  See any Common Lisp documentation

Function: <reverse>

(defun reverse (x)
(declare (xargs :guard (or (true-listp x) (stringp x))))
(cond ((stringp x)
(coerce (revappend (coerce x 'list) nil)
'string))
(t (revappend x nil))))
```

`(revappend x y)``x` の先頭から `y``cons` していく末尾再帰の関数です。

```:doc revappend
```

```Parents: LISTS and ACL2-BUILT-INS.

Concatenate the [reverse] of one list to another

(Revappend x y) [concatenate]s the [reverse] of the list x to y,
which is also typically a list.

The following theorem characterizes this English description.

(equal (revappend x y)
(append (reverse x) y))

Hint: This lemma follows immediately from the definition of [reverse]
and the following lemma.

(defthm revappend-append
(equal (append (revappend x y) z)
(revappend x (append y z))))

The [guard] for (revappend x y) requires that x is a true list.

Revappend is defined in Common Lisp.  See any Common Lisp

Function: <revappend>

(defun revappend (x y)
(declare (xargs :guard (true-listp x)))
(if (endp x)
y (revappend (cdr x) (cons (car x) y))))
```

```(defun rev (x)
(if (endp x)
nil
(append (rev (cdr x)) (list (car x)))))
```

```
The admission of REV 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 REV is described by the
theorem (TRUE-LISTP (REV X)).  We used primitive type reasoning and
the :type-prescription rules BINARY-APPEND and TRUE-LISTP-APPEND.

Summary
Form:  ( DEFUN REV ...)
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)
REV
```

`(reverse x)` の正体は `(revappend x nil)` なので、 まずは `(revappend x y)``(append (rev x) y)` であることを証明します。

```(defthm revappend-equal-append-rev
(equal (revappend x y)
(append (rev x) y)))
```

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

Perhaps we can prove *1 by induction.  Two induction schemes are suggested
by this conjecture.  Subsumption reduces that number to one.

We will induct according to a scheme suggested by (REVAPPEND X Y).
This suggestion was produced using the :induction rules REV and REVAPPEND.
If we let (:P X Y) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP X))
(:P (CDR X) (CONS (CAR X) Y)))
(:P X Y))
(IMPLIES (ENDP X) (:P X Y))).
This induction is justified by the same argument used to admit REVAPPEND.
Note, however, that the unmeasured variable Y is being instantiated.
When applied to the goal at hand the above induction scheme produces
two nontautological subgoals.
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)
(EQUAL (REVAPPEND (CDR X) (CONS (CAR X) Y))
(APPEND (REV (CDR X))
(CONS (CAR X) Y))))
(EQUAL (REVAPPEND (CDR X) (CONS (CAR X) Y))
(APPEND (APPEND (REV (CDR X)) (LIST (CAR X)))
Y)))

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

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

(IMPLIES (TRUE-LISTP RV)
(EQUAL (APPEND RV (CONS X1 Y))
(APPEND (APPEND RV (LIST X1)) Y))).
Subgoal *1.1/3
Subgoal *1.1/3'
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.

Summary
Form:  ( DEFTHM REVAPPEND-EQUAL-APPEND-REV ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION REV)
(:DEFINITION REVAPPEND)
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART CONSP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION BINARY-APPEND)
(:INDUCTION REV)
(:INDUCTION REVAPPEND)
(:INDUCTION TRUE-LISTP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION BINARY-APPEND)
(:TYPE-PRESCRIPTION REV)
(:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  1658
REVAPPEND-EQUAL-APPEND-REV
```

```(defthm reverse-equal-rev
(equal (reverse x)
(if (stringp x)
(coerce (rev (coerce x 'list))
'string)
(rev x))))
```

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

Q.E.D.

Summary
Form:  ( DEFTHM REVERSE-EQUAL-REV ...)
Rules: ((:DEFINITION REVERSE)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE APPEND-TO-NIL)
(:REWRITE REVAPPEND-EQUAL-APPEND-REV)
(:TYPE-PRESCRIPTION REV))
Warnings:  Non-rec
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  147
REVERSE-EQUAL-REV
```

Summary に `(:REWRITE REVAPPEND-EQUAL-APPEND-REV)` とあるので、 意図した通りに `revappend-equal-append-rev` を使って証明してくれたようです。

`Non-rec` という警告がでていますがこれは `reverse` は再帰関数じゃないから展開されてしまうため、 Rewrite ルールでは絶対マッチしないよっていう意味です。 それでは困るし `reverse` は展開する必要はないため下記によって、 証明時に `reverse` 関数を展開しないようにします。

```(in-theory (disable reverse))
```

```
Summary
Form:  ( IN-THEORY (DISABLE ...))
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(:NUMBER-OF-ENABLED-RUNES 4341)
```

これで今後は `reverse``rev` に書き換えられるようになりました。

## 1. `x` が回文のとき `y` と `(reverse y)` に挟まれたものが回文であることを示す

`x` が回文のとき `y``(reverse y)` に挟まれたものが回文であることを Lisp 的に表現すると下記のようになります。 この定理を使って何かをするわけではないので `:rule-classes``nil` としておきます。

```(defthm palindrome-sandwich-1
(implies (and (true-listp x)
(true-listp y)
(palindromep x))
(palindromep (append y x (reverse y))))
:rule-classes nil)
```

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

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

([ A key checkpoint:

Subgoal 2
(IMPLIES (AND (CONSP X)
(TRUE-LISTP Y)
(EQUAL (REV X) X))
(EQUAL (REV (APPEND Y X (REV Y)))
(APPEND Y X (REV Y))))

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.  Six induction schemes are suggested
by this conjecture.  Subsumption reduces that number to four.  These
merge into two derived induction schemes.  We will choose arbitrarily
among these.

We will induct according to a scheme suggested by (APPEND X (REVERSE Y)).
This suggestion was produced using the :induction rules BINARY-APPEND
and TRUE-LISTP.  If we let (:P X Y) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X) Y))
(:P X Y))
(IMPLIES (ENDP X) (:P X Y))).
This induction is justified by the same argument used to admit BINARY-APPEND.
When applied to the goal at hand the above induction scheme produces
two nontautological subgoals.
Subgoal *1/2
Subgoal *1/2'

Splitter note (see :DOC splitter) for Subgoal *1/2' (3 subgoals).
if-intro: ((:REWRITE REVERSE-EQUAL-REV))

Subgoal *1/2.3
Subgoal *1/2.3'
Subgoal *1/2.3''
Subgoal *1/2.3'''
Subgoal *1/2.3'4'
Subgoal *1/2.3'5'
Subgoal *1/2.3'6'
Subgoal *1/2.3'7'

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

Subgoal *1/2.3'
(IMPLIES (AND (CONSP X)
(NOT (EQUAL (REV (CDR X)) (CDR X)))
(TRUE-LISTP X)
(TRUE-LISTP Y)
(EQUAL (APPEND (REV (CDR X)) (LIST (CAR X)))
X))
(EQUAL (REV (APPEND Y
(CONS (CAR X)
(APPEND (CDR X) (REV Y)))))
(APPEND Y
(CONS (CAR X)
(APPEND (CDR X) (REV Y))))))

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

])
Subgoal *1/2.2
Subgoal *1/2.2'
Subgoal *1/2.2''
Subgoal *1/2.2'''
Subgoal *1/2.2'4'
Subgoal *1/2.2'5'
Subgoal *1/2.2'6'
Subgoal *1/2.2'7'
Subgoal *1/2.2'8'
Subgoal *1/2.2'9'
Subgoal *1/2.2'10'

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

Subgoal *1/2.2''
(IMPLIES (AND (CONSP X)
(EQUAL (REV (APPEND Y (CDR X) (REV Y)))
(APPEND Y (CDR X) (REV Y)))
(TRUE-LISTP X)
(TRUE-LISTP Y)
(EQUAL (APPEND (REV (CDR X)) (LIST (CAR X)))
X))
(EQUAL (REV (APPEND Y
(CONS (CAR X)
(APPEND (CDR X) (REV Y)))))
(APPEND Y
(CONS (CAR X)
(APPEND (CDR X) (REV Y))))))

*1.2 (Subgoal *1/2.2'10') is pushed for proof by induction.

])
Subgoal *1/2.1
Subgoal *1/2.1'
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 (TRUE-LISTP Y)
(EQUAL (REV (APPEND Y (REV Y)))
(APPEND Y (REV Y))))

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

])

Subgoal *1.3/3
Subgoal *1.3/3'
Subgoal *1.3/3''
Subgoal *1.3/3'''
Subgoal *1.3/3'4'
Subgoal *1.3/3'5'

*1.3.1 (Subgoal *1.3/3'5') is pushed for proof by induction.
Subgoal *1.3/2
Subgoal *1.3/1
Subgoal *1.3/1'

Subgoal *1.3.1/3
Subgoal *1.3.1/3'

Splitter note (see :DOC splitter) for Subgoal *1.3.1/3' (2 subgoals).
if-intro: ((:REWRITE CONS-EQUAL))

Subgoal *1.3.1/3.2
Subgoal *1.3.1/3.2'
Subgoal *1.3.1/3.2''

*1.3.1.1 (Subgoal *1.3.1/3.2'') is pushed for proof by induction.
Subgoal *1.3.1/3.1
Subgoal *1.3.1/3.1'
Subgoal *1.3.1/3.1''
Subgoal *1.3.1/3.1'''

*1.3.1.2 (Subgoal *1.3.1/3.1''') is pushed for proof by induction.
Subgoal *1.3.1/2
Subgoal *1.3.1/1
Subgoal *1.3.1/1'

Subgoal *1.3.1.2/3
Subgoal *1.3.1.2/3'
Subgoal *1.3.1.2/3''
Subgoal *1.3.1.2/3'''
Subgoal *1.3.1.2/3'4'
Subgoal *1.3.1.2/3'5'
Subgoal *1.3.1.2/3'6'
Subgoal *1.3.1.2/3'7'

*1.3.1.2.1 (Subgoal *1.3.1.2/3'7') is pushed for proof by induction.
Subgoal *1.3.1.2/2
Subgoal *1.3.1.2/1
Subgoal *1.3.1.2/1'
Subgoal *1.3.1.2/1''
Subgoal *1.3.1.2/1'''
Subgoal *1.3.1.2/1'4'

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

Summary
Form:  ( DEFTHM PALINDROME-SANDWICH-1 ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION HIDE)
(:DEFINITION NOT)
(:DEFINITION REV)
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART REV)
(:EXECUTABLE-COUNTERPART REVERSE)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION BINARY-APPEND)
(:INDUCTION REV)
(:INDUCTION TRUE-LISTP)
(:REWRITE CONS-EQUAL)
(:REWRITE REVERSE-EQUAL-REV)
(:TYPE-PRESCRIPTION BINARY-APPEND)
(:TYPE-PRESCRIPTION REV)
(:TYPE-PRESCRIPTION REVERSE)
(:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION TRUE-LISTP)
(:REWRITE CONS-EQUAL)
(:REWRITE REVERSE-EQUAL-REV))
Time:  0.03 seconds (prove: 0.03, print: 0.00, other: 0.00)
Prover steps counted:  15671

---
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/2.3'
(IMPLIES (AND (CONSP X)
(NOT (EQUAL (REV (CDR X)) (CDR X)))
(TRUE-LISTP X)
(TRUE-LISTP Y)
(EQUAL (APPEND (REV (CDR X)) (LIST (CAR X)))
X))
(EQUAL (REV (APPEND Y
(CONS (CAR X)
(APPEND (CDR X) (REV Y)))))
(APPEND Y
(CONS (CAR X)
(APPEND (CDR X) (REV Y))))))

Subgoal *1/2.2''
(IMPLIES (AND (CONSP X)
(EQUAL (REV (APPEND Y (CDR X) (REV Y)))
(APPEND Y (CDR X) (REV Y)))
(TRUE-LISTP X)
(TRUE-LISTP Y)
(EQUAL (APPEND (REV (CDR X)) (LIST (CAR X)))
X))
(EQUAL (REV (APPEND Y
(CONS (CAR X)
(APPEND (CDR X) (REV Y)))))
(APPEND Y
(CONS (CAR X)
(APPEND (CDR X) (REV Y))))))

Subgoal *1/1'''
(IMPLIES (TRUE-LISTP Y)
(EQUAL (REV (APPEND Y (REV Y)))
(APPEND Y (REV Y))))

ACL2 Error in ( DEFTHM PALINDROME-SANDWICH-1 ...):  See :DOC failure.

******** FAILED ********
```

```Subgoal *1/1'''
(IMPLIES (TRUE-LISTP Y)
(EQUAL (REV (APPEND Y (REV Y)))
(APPEND Y (REV Y))))
```

```(defthm rev-append
(equal (rev (append x y))
(append (rev y) (rev x))))
```

```
*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.  Subsumption reduces that number to two.
However, one of these is flawed and so we are left with one viable
candidate.

We will induct according to a scheme suggested by (APPEND X Y).  This
suggestion was produced using the :induction rules BINARY-APPEND and
REV.  If we let (:P X Y) denote *1 above then the induction scheme
we'll use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X) Y))
(:P X Y))
(IMPLIES (ENDP X) (:P X Y))).
This induction is justified by the same argument used to admit BINARY-APPEND.
When applied to the goal at hand the above induction scheme produces
two nontautological subgoals.
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)
(EQUAL (REV (APPEND (CDR X) Y))
(APPEND (REV Y) (REV (CDR X)))))
(EQUAL (APPEND (REV (APPEND (CDR X) Y))
(LIST (CAR X)))
(APPEND (REV Y)
(REV (CDR X))
(LIST (CAR X)))))

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

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

(IMPLIES (AND (TRUE-LISTP RV) (TRUE-LISTP RV0))
(EQUAL (APPEND (APPEND RV0 RV) (LIST X1))
(APPEND RV0 RV (LIST X1)))).
Subgoal *1.1/3
Subgoal *1.1/3'
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.

Summary
Form:  ( DEFTHM REV-APPEND ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION REV)
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART CONSP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION BINARY-APPEND)
(:INDUCTION REV)
(:INDUCTION TRUE-LISTP)
(:REWRITE APPEND-TO-NIL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION REV)
(:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  2624
REV-APPEND
```

```(defthm palindrome-sandwich-1
(implies (and (true-listp x)
(true-listp y)
(palindromep x))
(palindromep (append y x (reverse y))))
:rule-classes nil)
```

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

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

([ A key checkpoint:

Subgoal 2
(IMPLIES (AND (CONSP X)
(TRUE-LISTP Y)
(EQUAL (REV X) X))
(EQUAL (APPEND (APPEND (REV (REV Y)) X)
(REV Y))
(APPEND Y X (REV Y))))

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.  Six induction schemes are suggested
by this conjecture.  Subsumption reduces that number to four.  These
merge into two derived induction schemes.  We will choose arbitrarily
among these.

We will induct according to a scheme suggested by (APPEND X (REVERSE Y)).
This suggestion was produced using the :induction rules BINARY-APPEND
and TRUE-LISTP.  If we let (:P X Y) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X) Y))
(:P X Y))
(IMPLIES (ENDP X) (:P X Y))).
This induction is justified by the same argument used to admit BINARY-APPEND.
When applied to the goal at hand the above induction scheme produces
two nontautological subgoals.
Subgoal *1/2
Subgoal *1/2'

Splitter note (see :DOC splitter) for Subgoal *1/2' (3 subgoals).
if-intro: ((:REWRITE REVERSE-EQUAL-REV))

Subgoal *1/2.3
Subgoal *1/2.3'
Subgoal *1/2.3''
Subgoal *1/2.3'''
Subgoal *1/2.3'4'

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

Subgoal *1/2.3'
(IMPLIES (AND (CONSP X)
(NOT (EQUAL (REV (CDR X)) (CDR X)))
(TRUE-LISTP X)
(TRUE-LISTP Y)
(EQUAL (APPEND (REV (CDR X)) (LIST (CAR X)))
X))
(EQUAL (APPEND (APPEND (REV (REV Y)) X)
(REV Y))
(APPEND Y
(CONS (CAR X)
(APPEND (CDR X) (REV Y))))))

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

])
Subgoal *1/2.2
Subgoal *1/2.2'
Subgoal *1/2.2''
Subgoal *1/2.2'''
Subgoal *1/2.2'4'
Subgoal *1/2.2'5'
Subgoal *1/2.2'6'

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

Subgoal *1/2.2''
(IMPLIES (AND (CONSP X)
(EQUAL (APPEND (APPEND (REV (REV Y)) (REV (CDR X)))
(REV Y))
(APPEND Y (CDR X) (REV Y)))
(TRUE-LISTP X)
(TRUE-LISTP Y)
(EQUAL (APPEND (REV (CDR X)) (LIST (CAR X)))
X))
(EQUAL (APPEND (APPEND (REV (REV Y)) X)
(REV Y))
(APPEND Y
(CONS (CAR X)
(APPEND (CDR X) (REV Y))))))

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

])
Subgoal *1/2.1
Subgoal *1/2.1'
Subgoal *1/1
Subgoal *1/1'
Subgoal *1/1''
Subgoal *1/1'''
Subgoal *1/1'4'

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

Subgoal *1/1'''
(IMPLIES (TRUE-LISTP Y)
(EQUAL (APPEND (REV (REV Y)) (REV Y))
(APPEND Y (REV Y))))

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

])

(IMPLIES (AND (TRUE-LISTP RV) (TRUE-LISTP Y))
(EQUAL (APPEND (REV RV) RV)
(APPEND Y RV))).
Subgoal *1.3/3
Subgoal *1.3/3'
Subgoal *1.3/3''
Subgoal *1.3/3'''
Subgoal *1.3/3'4'

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

*1.3.2 (Subgoal *1.3/1''') is pushed for proof by induction.

(IMPLIES (TRUE-LISTP RV)
(EQUAL (APPEND (REV RV) RV) RV)).
Subgoal *1.3.2/3
Subgoal *1.3.2/3'
Subgoal *1.3.2/3''
Subgoal *1.3.2/3'''
Subgoal *1.3.2/3'4'
Subgoal *1.3.2/3'5'
Subgoal *1.3.2/3'6'

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

(IMPLIES (AND (TRUE-LISTP RV) (TRUE-LISTP RV2))
(EQUAL (APPEND (APPEND RV (LIST RV1))
(CONS RV1 RV2))
(CONS RV1 (APPEND RV RV2)))).
Subgoal *1.3.2.1/3
Subgoal *1.3.2.1/3'
Subgoal *1.3.2.1/3''
Subgoal *1.3.2.1/3'''
Subgoal *1.3.2.1/3'4'

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

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

Summary
Form:  ( DEFTHM PALINDROME-SANDWICH-1 ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION HIDE)
(:DEFINITION NOT)
(:DEFINITION REV)
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART BINARY-APPEND)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART REV)
(:EXECUTABLE-COUNTERPART REVERSE)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION BINARY-APPEND)
(:INDUCTION REV)
(:INDUCTION TRUE-LISTP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE CONS-EQUAL)
(:REWRITE REV-APPEND)
(:REWRITE REVERSE-EQUAL-REV)
(:TYPE-PRESCRIPTION BINARY-APPEND)
(:TYPE-PRESCRIPTION REV)
(:TYPE-PRESCRIPTION REVERSE)
(:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION TRUE-LISTP)
(:REWRITE REVERSE-EQUAL-REV))
Time:  0.03 seconds (prove: 0.03, print: 0.00, other: 0.00)
Prover steps counted:  14468

---
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/2.3'
(IMPLIES (AND (CONSP X)
(NOT (EQUAL (REV (CDR X)) (CDR X)))
(TRUE-LISTP X)
(TRUE-LISTP Y)
(EQUAL (APPEND (REV (CDR X)) (LIST (CAR X)))
X))
(EQUAL (APPEND (APPEND (REV (REV Y)) X)
(REV Y))
(APPEND Y
(CONS (CAR X)
(APPEND (CDR X) (REV Y))))))

Subgoal *1/2.2''
(IMPLIES (AND (CONSP X)
(EQUAL (APPEND (APPEND (REV (REV Y)) (REV (CDR X)))
(REV Y))
(APPEND Y (CDR X) (REV Y)))
(TRUE-LISTP X)
(TRUE-LISTP Y)
(EQUAL (APPEND (REV (CDR X)) (LIST (CAR X)))
X))
(EQUAL (APPEND (APPEND (REV (REV Y)) X)
(REV Y))
(APPEND Y
(CONS (CAR X)
(APPEND (CDR X) (REV Y))))))

Subgoal *1/1'''
(IMPLIES (TRUE-LISTP Y)
(EQUAL (APPEND (REV (REV Y)) (REV Y))
(APPEND Y (REV Y))))

ACL2 Error in ( DEFTHM PALINDROME-SANDWICH-1 ...):  See :DOC failure.

******** FAILED ********
```

`Subgoal *1/1'''` に注目しましょう。 `(rev (rev x))``x` と等しいことを証明すれば `Subgoal *1/1'''` は真ですね。

```Subgoal *1/1'''
(IMPLIES (TRUE-LISTP Y)
(EQUAL (APPEND (REV (REV Y)) (REV Y))
(APPEND Y (REV Y))))
```

```(defthm rev-rev
(implies (true-listp x)
(equal (rev (rev x))
x)))
```

```
*1 (the initial Goal, a key checkpoint) 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 (REV X).  This suggestion
was produced using the :induction rules REV and TRUE-LISTP.  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 REV.
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/1
Subgoal *1/1'

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

Q.E.D.

Summary
Form:  ( DEFTHM REV-REV ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION REV)
(:DEFINITION TRUE-LISTP)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART REV)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION REV)
(:INDUCTION TRUE-LISTP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE CONS-CAR-CDR)
(:REWRITE REV-APPEND))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  447
REV-REV
```

`rev-rev` は問題なく証明できました。 それでは再度 `palindrome-sandwich-1` の証明を試みます。

```(defthm palindrome-sandwich-1
(implies (and (true-listp x)
(true-listp y)
(palindromep x))
(palindromep (append y x (reverse y))))
:rule-classes nil)
```

```Goal'
Goal''
Goal'''
Goal'4'

([ A key checkpoint:

Goal'
(IMPLIES (AND (CONSP X)
(TRUE-LISTP Y)
(EQUAL (REV X) X))
(EQUAL (APPEND (APPEND Y X) (REV Y))
(APPEND Y X (REV Y))))

Normally we would attempt to prove Goal'4' 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.  Six induction schemes are suggested
by this conjecture.  Subsumption reduces that number to four.  These
merge into two derived induction schemes.  We will choose arbitrarily
among these.

We will induct according to a scheme suggested by (APPEND X (REVERSE Y)).
This suggestion was produced using the :induction rules BINARY-APPEND
and TRUE-LISTP.  If we let (:P X Y) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X) Y))
(:P X Y))
(IMPLIES (ENDP X) (:P X Y))).
This induction is justified by the same argument used to admit BINARY-APPEND.
When applied to the goal at hand the above induction scheme produces
two nontautological subgoals.
Subgoal *1/2
Subgoal *1/2'

Splitter note (see :DOC splitter) for Subgoal *1/2' (3 subgoals).
if-intro: ((:REWRITE REVERSE-EQUAL-REV))

Subgoal *1/2.3
Subgoal *1/2.3'
Subgoal *1/2.3''
Subgoal *1/2.3'''
Subgoal *1/2.3'4'

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

Subgoal *1/2.3'
(IMPLIES (AND (CONSP X)
(NOT (EQUAL (REV (CDR X)) (CDR X)))
(TRUE-LISTP X)
(TRUE-LISTP Y)
(EQUAL (APPEND (REV (CDR X)) (LIST (CAR X)))
X))
(EQUAL (APPEND (APPEND Y X) (REV Y))
(APPEND Y
(CONS (CAR X)
(APPEND (CDR X) (REV Y))))))

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

])
Subgoal *1/2.2
Subgoal *1/2.2'
Subgoal *1/2.2''
Subgoal *1/2.2'''
Subgoal *1/2.2'4'
Subgoal *1/2.2'5'
Subgoal *1/2.2'6'

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

Subgoal *1/2.2''
(IMPLIES (AND (CONSP X)
(EQUAL (APPEND (APPEND Y (REV (CDR X)))
(REV Y))
(APPEND Y (CDR X) (REV Y)))
(TRUE-LISTP X)
(TRUE-LISTP Y)
(EQUAL (APPEND (REV (CDR X)) (LIST (CAR X)))
X))
(EQUAL (APPEND (APPEND Y X) (REV Y))
(APPEND Y
(CONS (CAR X)
(APPEND (CDR X) (REV Y))))))

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

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

(TRUE-LISTP RV)
(TRUE-LISTP RV0)
(TRUE-LISTP X2)
(EQUAL (APPEND (APPEND Y RV) RV0)
(TRUE-LISTP (CONS X1 X2))
(TRUE-LISTP Y)
(EQUAL (APPEND RV (LIST X1))
(CONS X1 X2)))
(EQUAL (APPEND (APPEND Y (CONS X1 X2)) RV0)
Subgoal *1.2/4
Subgoal *1.2/4'
Subgoal *1.2/4''
Subgoal *1.2/4'''

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

(TRUE-LISTP RV)
(TRUE-LISTP RV0)
(TRUE-LISTP X2)
(TRUE-LISTP (CONS X1 X2))
(EQUAL (APPEND RV (LIST X1))
(CONS X1 X2)))
Subgoal *1.2.1/5
Subgoal *1.2.1/5'
Subgoal *1.2.1/5''
Subgoal *1.2.1/5'''
Subgoal *1.2.1/5'4'

*1.2.1.1 (Subgoal *1.2.1/5'4') is pushed for proof by induction.
Subgoal *1.2.1/4
Subgoal *1.2.1/4'
Subgoal *1.2.1/4''
Subgoal *1.2.1/4'''
Subgoal *1.2.1/4'4'

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

*1.2.1.3 (Subgoal *1.2.1/1'5') is pushed for proof by induction.

(IMPLIES (TRUE-LISTP RV)
(NOT (EQUAL (APPEND RV (LIST X1))
(LIST X1)))).
Subgoal *1.2.1.3/3
Subgoal *1.2.1.3/3'
Subgoal *1.2.1.3/2
Subgoal *1.2.1.3/1
Subgoal *1.2.1.3/1'
Subgoal *1.2.1.3/1''
Subgoal *1.2.1.3/1'''

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

Summary
Form:  ( DEFTHM PALINDROME-SANDWICH-1 ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION HIDE)
(:DEFINITION NOT)
(:DEFINITION REV)
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART REVERSE)
(:EXECUTABLE-COUNTERPART TRUE-LISTP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION BINARY-APPEND)
(:INDUCTION TRUE-LISTP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE CONS-EQUAL)
(:REWRITE REV-APPEND)
(:REWRITE REV-REV)
(:REWRITE REVERSE-EQUAL-REV)
(:TYPE-PRESCRIPTION BINARY-APPEND)
(:TYPE-PRESCRIPTION REV)
(:TYPE-PRESCRIPTION REVERSE)
(:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Splitter rules (see :DOC splitter):
if-intro: ((:REWRITE REVERSE-EQUAL-REV))
Time:  0.03 seconds (prove: 0.03, print: 0.00, other: 0.00)
Prover steps counted:  14017

---
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/2.3'
(IMPLIES (AND (CONSP X)
(NOT (EQUAL (REV (CDR X)) (CDR X)))
(TRUE-LISTP X)
(TRUE-LISTP Y)
(EQUAL (APPEND (REV (CDR X)) (LIST (CAR X)))
X))
(EQUAL (APPEND (APPEND Y X) (REV Y))
(APPEND Y
(CONS (CAR X)
(APPEND (CDR X) (REV Y))))))

Subgoal *1/2.2''
(IMPLIES (AND (CONSP X)
(EQUAL (APPEND (APPEND Y (REV (CDR X)))
(REV Y))
(APPEND Y (CDR X) (REV Y)))
(TRUE-LISTP X)
(TRUE-LISTP Y)
(EQUAL (APPEND (REV (CDR X)) (LIST (CAR X)))
X))
(EQUAL (APPEND (APPEND Y X) (REV Y))
(APPEND Y
(CONS (CAR X)
(APPEND (CDR X) (REV Y))))))

ACL2 Error in ( DEFTHM PALINDROME-SANDWICH-1 ...):  See :DOC failure.

******** FAILED ********
```

`Subgoal *1/1'''` は消滅しましたね。 いままで目を背けていた `Subgoal *1/2.2''` について見てみましょう。

```Subgoal *1/2.2''
(IMPLIES (AND (CONSP X)
(EQUAL (APPEND (APPEND Y (REV (CDR X)))
(REV Y))
(APPEND Y (CDR X) (REV Y)))
(TRUE-LISTP X)
(TRUE-LISTP Y)
(EQUAL (APPEND (REV (CDR X)) (LIST (CAR X)))
X))
(EQUAL (APPEND (APPEND Y X) (REV Y))
(APPEND Y
(CONS (CAR X)
(APPEND (CDR X) (REV Y))))))
```

`(append x (append y z))` のような構造があるのが気になりますね。 これを `(append x (append y z))` に書き換えればよさそうです。 なお、ACL2 では `(append x y z)` と書いたら `(append x (append y z))` と書いたのと同じ意味になります。 これくらい Built-in-theorems-about-lists にあっても良いんじゃないかと思うのですがどうやら入っていないようです。 たぶん Std/lists のようなライブラリに入っていると思います。

```(defthm associativity-of-append
(equal (append (append x y) z)
(append x y z)))
```

```
*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.  Subsumption reduces that number to two.
However, one of these is flawed and so we are left with one viable
candidate.

We will induct according to a scheme suggested by (APPEND X Y).  This
suggestion was produced using the :induction rule BINARY-APPEND.  If
we let (:P X Y Z) denote *1 above then the induction scheme we'll use
is
(AND (IMPLIES (AND (NOT (ENDP X)) (: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 BINARY-APPEND.
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 ASSOCIATIVITY-OF-APPEND ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION BINARY-APPEND)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  435
ASSOCIATIVITY-OF-APPEND
```

では再度自動証明を試みます。

```(defthm palindrome-sandwich-1
(implies (and (true-listp x)
(true-listp y)
(palindromep x))
(palindromep (append y x (reverse y))))
:rule-classes nil)
```

```
Q.E.D.

Summary
Form:  ( DEFTHM PALINDROME-SANDWICH-1 ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION TRUE-LISTP)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART REVERSE)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE ASSOCIATIVITY-OF-APPEND)
(:REWRITE REV-APPEND)
(:REWRITE REV-REV)
(:REWRITE REVERSE-EQUAL-REV)
(:TYPE-PRESCRIPTION REV)
(:TYPE-PRESCRIPTION REVERSE)
(:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  498
PALINDROME-SANDWICH-1
```

## 2. `(append y x (reverse y))` が回文であることと `x` が回文であることが等しいことを示す

いままでに作成した補助定理で 1番目の定理は既に自動証明されるようになっています。 この状態で下記の定理を証明してみましょう。

```(defthm palindrome-sandwich
(implies (and (true-listp x)
(true-listp y))
(equal (palindromep (append y x (reverse y)))
(palindromep x))))
```

```Subgoal 2
Subgoal 2'

([ A key checkpoint:

Subgoal 2'
(IMPLIES (AND (TRUE-LISTP X)
(TRUE-LISTP Y)
(EQUAL (APPEND Y (REV X) (REV Y))
(APPEND Y X (REV Y))))
(EQUAL (REV X) X))

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

])
Subgoal 1

Perhaps we can prove *1 by induction.  Nine induction schemes are suggested
by this conjecture.  Subsumption reduces that number to four.  These
merge into two derived induction schemes.  One of these has a score
higher than the other.

We will induct according to a scheme suggested by (APPEND Y X (REV Y)).
This suggestion was produced using the :induction rules BINARY-APPEND,
REV and TRUE-LISTP.  If we let (:P X Y) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP Y)) (:P X (CDR Y)))
(:P X Y))
(IMPLIES (ENDP Y) (:P X Y))).
This induction is justified by the same argument used to admit BINARY-APPEND.
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'

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

Subgoal *1/3'''
(IMPLIES (AND (CONSP Y)
(NOT (EQUAL (APPEND (CDR Y) (REV X) (REV (CDR Y)))
(APPEND (CDR Y) X (REV (CDR Y)))))
(TRUE-LISTP X)
(TRUE-LISTP (CDR Y))
(EQUAL (APPEND (CDR Y)
(REV X)
(REV (CDR Y))
(LIST (CAR Y)))
(APPEND (CDR Y)
X (REV (CDR Y))
(LIST (CAR Y)))))
(EQUAL (REV X) X))

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

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

(IMPLIES (AND (CONSP L)
(TRUE-LISTP L)
(TRUE-LISTP RV)
(TRUE-LISTP RV0)
(NOT (EQUAL (APPEND Y2 RV RV0)
(APPEND Y2 X RV0)))
(TRUE-LISTP X)
(TRUE-LISTP Y2)
(EQUAL (APPEND Y2 RV L)
(APPEND Y2 X L)))
(EQUAL RV X)).
Subgoal *1.1/4
Subgoal *1.1/4'
Subgoal *1.1/3
Subgoal *1.1/2
Subgoal *1.1/2'
Subgoal *1.1/1
Subgoal *1.1/1'
Subgoal *1.1/1''
Subgoal *1.1/1'''

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

(IMPLIES (AND (CONSP L)
(TRUE-LISTP L)
(TRUE-LISTP RV)
(TRUE-LISTP RV0)
(NOT (EQUAL (APPEND RV RV0) (APPEND X RV0)))
(TRUE-LISTP X)
(EQUAL (APPEND RV L) (APPEND X L)))
(EQUAL RV X)).
Subgoal *1.1.1/5
Subgoal *1.1.1/5'
Subgoal *1.1.1/4
Subgoal *1.1.1/4'
Subgoal *1.1.1/4''
Subgoal *1.1.1/4'''
Subgoal *1.1.1/4'4'
Subgoal *1.1.1/4'5'
Subgoal *1.1.1/4'6'
Subgoal *1.1.1/4'7'
Subgoal *1.1.1/4'8'

*1.1.1.1 (Subgoal *1.1.1/4'8') is pushed for proof by induction.
Subgoal *1.1.1/3
Subgoal *1.1.1/3'
Subgoal *1.1.1/3''
Subgoal *1.1.1/3'''
Subgoal *1.1.1/3'4'

*1.1.1.2 (Subgoal *1.1.1/3'4') is pushed for proof by induction.
Subgoal *1.1.1/2
Subgoal *1.1.1/1
Subgoal *1.1.1/1'
Subgoal *1.1.1/1''
Subgoal *1.1.1/1'''
Subgoal *1.1.1/1'4'
Subgoal *1.1.1/1'5'
Subgoal *1.1.1/1'6'

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

(IMPLIES (AND (TRUE-LISTP RV0)
(NOT (EQUAL RV0 (APPEND X RV0)))
(TRUE-LISTP X))
(NOT X)).
Subgoal *1.1.1.3/4
Subgoal *1.1.1.3/3
Subgoal *1.1.1.3/3'
Subgoal *1.1.1.3/3''
Subgoal *1.1.1.3/3'''
Subgoal *1.1.1.3/3'4'
Subgoal *1.1.1.3/3'5'

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

Summary
Form:  ( DEFTHM PALINDROME-SANDWICH ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION REV)
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART REV)
(:EXECUTABLE-COUNTERPART TRUE-LISTP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION BINARY-APPEND)
(:INDUCTION REV)
(:INDUCTION TRUE-LISTP)
(:REWRITE APPEND-TO-NIL)
(:REWRITE ASSOCIATIVITY-OF-APPEND)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE CONS-EQUAL)
(:REWRITE REV-APPEND)
(:REWRITE REV-REV)
(:REWRITE REVERSE-EQUAL-REV)
(:TYPE-PRESCRIPTION BINARY-APPEND)
(:TYPE-PRESCRIPTION REV)
(:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Time:  0.03 seconds (prove: 0.03, print: 0.00, other: 0.00)
Prover steps counted:  11707

---
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: ***

Subgoal 2'
(IMPLIES (AND (TRUE-LISTP X)
(TRUE-LISTP Y)
(EQUAL (APPEND Y (REV X) (REV Y))
(APPEND Y X (REV Y))))
(EQUAL (REV X) X))

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

Subgoal *1/3'''
(IMPLIES (AND (CONSP Y)
(NOT (EQUAL (APPEND (CDR Y) (REV X) (REV (CDR Y)))
(APPEND (CDR Y) X (REV (CDR Y)))))
(TRUE-LISTP X)
(TRUE-LISTP (CDR Y))
(EQUAL (APPEND (CDR Y)
(REV X)
(REV (CDR Y))
(LIST (CAR Y)))
(APPEND (CDR Y)
X (REV (CDR Y))
(LIST (CAR Y)))))
(EQUAL (REV X) X))

ACL2 Error in ( DEFTHM PALINDROME-SANDWICH ...):  See :DOC failure.

******** FAILED ********
```

トップレベルの Key checkpoint を確認しましょう。 どうやら `(equal (rev x) x)` のときに `(equal (append y (rev x) (rev y)) (append y x (rev y)))` であることは自動証明されたようです。

この逆が証明できていないという状態です。

```*** Key checkpoint at the top level: ***

Subgoal 2'
(IMPLIES (AND (TRUE-LISTP X)
(TRUE-LISTP Y)
(EQUAL (APPEND Y (REV X) (REV Y))
(APPEND Y X (REV Y))))
(EQUAL (REV X) X))
```

`rev` という関数によって惑わされてしまうので、一旦 `(rev y)``z`, `x``x1`, `(rev x)``x2` と置いて考えましょう。 するとこの問題は `(append y x1 z)``(append y x2 z)` が等しいとき、 `x1``x2` は等しいかという問題になります。 そりゃあ等しいに決まっています。 なんというか直感的に正しいって分かります。 だって左と右に何かを挟んだやつ同士が等しかったら挟まれたもの同士も等しいに決まってます。

このことを `sandwith-equal` と名付けて証明しましょう。

```(defthm sandwich-equal
(implies (and (true-listp x1)
(true-listp x2)
(true-listp y)
(true-listp z))
(equal (equal (append y x1 z)
(append y x2 z))
(equal x1 x2))))
```

```Subgoal 2
Subgoal 2'

([ A key checkpoint:

Subgoal 2'
(IMPLIES (AND (TRUE-LISTP X1)
(TRUE-LISTP X2)
(TRUE-LISTP Y)
(TRUE-LISTP Z)
(EQUAL (APPEND Y X1 Z) (APPEND Y X2 Z)))
(EQUAL X1 X2))

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

])
Subgoal 1

Perhaps we can prove *1 by induction.  Eight induction schemes are
suggested by this conjecture.  Subsumption reduces that number to seven.
These merge into four derived induction schemes.  However, one of these
is flawed and so we are left with three viable candidates.  We will
choose arbitrarily among these.

We will induct according to a scheme suggested by (APPEND X1 Z).  This
suggestion was produced using the :induction rules BINARY-APPEND and
TRUE-LISTP.  If we let (:P X1 X2 Y Z) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X1))
(:P (CDR X1) X2 Y Z))
(:P X1 X2 Y Z))
(IMPLIES (ENDP X1) (:P X1 X2 Y Z))).
This induction is justified by the same argument used to admit BINARY-APPEND.
When applied to the goal at hand the above induction scheme produces
four nontautological subgoals.
Subgoal *1/4
Subgoal *1/4'
Subgoal *1/4''
Subgoal *1/4'''
Subgoal *1/4'4'
Subgoal *1/4'5'
Subgoal *1/4'6'

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

Subgoal *1/4''
(IMPLIES (AND (CONSP X1)
(TRUE-LISTP (CDR X1))
(TRUE-LISTP Y)
(TRUE-LISTP Z)
(EQUAL (APPEND Y (CONS (CAR X1) (APPEND (CDR X1) Z)))
(APPEND Y (CDR X1) Z)))
(EQUAL X1 (CDR X1)))

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

])
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'

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

Subgoal *1/3'''
(IMPLIES (AND (CONSP X1)
(NOT (EQUAL (APPEND Y (CDR X1) Z)
(APPEND Y X2 Z)))
(TRUE-LISTP (CDR X1))
(TRUE-LISTP X2)
(TRUE-LISTP Y)
(TRUE-LISTP Z)
(EQUAL (APPEND Y (CONS (CAR X1) (APPEND (CDR X1) Z)))
(APPEND Y X2 Z)))
(EQUAL X1 X2))

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

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

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

Subgoal *1/1'''
(IMPLIES (AND (TRUE-LISTP X2)
(TRUE-LISTP Y)
(TRUE-LISTP Z)
(EQUAL (APPEND Y Z) (APPEND Y X2 Z)))
(NOT X2))

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

])

(IMPLIES (AND (TRUE-LISTP X2)
(TRUE-LISTP Y)
(TRUE-LISTP Z)
(EQUAL (APPEND Y Z) (APPEND Y X2 Z)))
(NOT X2)).
Subgoal *1.3/3
Subgoal *1.3/3'
Subgoal *1.3/2
Subgoal *1.3/1
Subgoal *1.3/1'
Subgoal *1.3/1''
Subgoal *1.3/1'''
Subgoal *1.3/1'4'

*1.3.1 (Subgoal *1.3/1'4') is pushed for proof by induction.

(IMPLIES (AND (TRUE-LISTP X2)
(TRUE-LISTP (APPEND X2 Z)))
(NOT X2)).
Subgoal *1.3.1/4
Subgoal *1.3.1/4'
Subgoal *1.3.1/4''
Subgoal *1.3.1/4'''
Subgoal *1.3.1/4'4'
Subgoal *1.3.1/4'5'
Subgoal *1.3.1/4'6'

A goal of NIL, Subgoal *1.3.1/4'6', has been generated!  Obviously,
the proof attempt has failed.

Summary
Form:  ( DEFTHM SANDWICH-EQUAL ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART TRUE-LISTP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION BINARY-APPEND)
(:INDUCTION TRUE-LISTP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Time:  0.02 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  5854

---
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: ***

Subgoal 2'
(IMPLIES (AND (TRUE-LISTP X1)
(TRUE-LISTP X2)
(TRUE-LISTP Y)
(TRUE-LISTP Z)
(EQUAL (APPEND Y X1 Z) (APPEND Y X2 Z)))
(EQUAL X1 X2))

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

Subgoal *1/4''
(IMPLIES (AND (CONSP X1)
(TRUE-LISTP (CDR X1))
(TRUE-LISTP Y)
(TRUE-LISTP Z)
(EQUAL (APPEND Y (CONS (CAR X1) (APPEND (CDR X1) Z)))
(APPEND Y (CDR X1) Z)))
(EQUAL X1 (CDR X1)))

Subgoal *1/3'''
(IMPLIES (AND (CONSP X1)
(NOT (EQUAL (APPEND Y (CDR X1) Z)
(APPEND Y X2 Z)))
(TRUE-LISTP (CDR X1))
(TRUE-LISTP X2)
(TRUE-LISTP Y)
(TRUE-LISTP Z)
(EQUAL (APPEND Y (CONS (CAR X1) (APPEND (CDR X1) Z)))
(APPEND Y X2 Z)))
(EQUAL X1 X2))

Subgoal *1/1'''
(IMPLIES (AND (TRUE-LISTP X2)
(TRUE-LISTP Y)
(TRUE-LISTP Z)
(EQUAL (APPEND Y Z) (APPEND Y X2 Z)))
(NOT X2))

ACL2 Error in ( DEFTHM SANDWICH-EQUAL ...):  See :DOC failure.

******** FAILED ********
```

```We will induct according to a scheme suggested by (APPEND X1 Z).  This
suggestion was produced using the :induction rules BINARY-APPEND and
TRUE-LISTP.  If we let (:P X1 X2 Y Z) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X1))
(:P (CDR X1) X2 Y Z))
(:P X1 X2 Y Z))
(IMPLIES (ENDP X1) (:P X1 X2 Y Z))).
```

`x1``x2` が等しいことを示したいのですから `(:P (CDR X1) X2 Y Z)` のような偏った仮定を使われては困ります。 `(:P (CDR X1) (CDR X2) Y Z)` という感じじゃないと駄目です。

というわけで、 `sandwich-equal` を証明するための、 inductoin scheme を定義しましょう。 これは下記のような再帰関数を定義し hints として与えること実現します。

```(defun sandwich-equal-induction (x y)
(cond
((endp x) y)
((endp y) x)
(t (sandwich-equal-induction (cdr x) (cdr y)))))
```

```
The admission of SANDWICH-EQUAL-INDUCTION 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 could deduce no constraints on
the type of SANDWICH-EQUAL-INDUCTION.

Summary
Form:  ( DEFUN SANDWICH-EQUAL-INDUCTION ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SANDWICH-EQUAL-INDUCTION
```

この関数を `induction scheme` として与えれば `x1``x2` は平等になります。 では、再度証明を試みましょう。

```(defthm sandwich-equal
(implies (and (true-listp x1)
(true-listp x2)
(true-listp y)
(true-listp z))
(equal (equal (append y x1 z)
(append y x2 z))
(equal x1 x2)))
:hints (("Goal" :induct (sandwich-equal-induction x1 x2))))
```

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

We have been told to use induction.  One induction scheme is suggested
by the induction hint.

We will induct according to a scheme suggested by
(SANDWICH-EQUAL-INDUCTION X1 X2).  This suggestion was produced using
the :induction rule SANDWICH-EQUAL-INDUCTION.  If we let (:P X1 X2 Y Z)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X1))
(NOT (ENDP X2))
(:P (CDR X1) (CDR X2) Y Z))
(:P X1 X2 Y Z))
(IMPLIES (AND (NOT (ENDP X1)) (ENDP X2))
(:P X1 X2 Y Z))
(IMPLIES (ENDP X1) (:P X1 X2 Y Z))).
This induction is justified by the same argument used to admit
SANDWICH-EQUAL-INDUCTION.  Note, however, that the unmeasured variable
X2 is being instantiated.  When applied to the goal at hand the above
induction scheme produces three nontautological subgoals.
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/3.3
Subgoal *1/3.3'
Subgoal *1/3.3''
Subgoal *1/3.3'''
Subgoal *1/3.3'4'
Subgoal *1/3.3'5'
Subgoal *1/3.3'6'
Subgoal *1/3.3'7'

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

Subgoal *1/3.3'
(IMPLIES (AND (CONSP X1)
(CONSP X2)
(EQUAL (CDR X1) (CDR X2))
(TRUE-LISTP (CDR X1))
(TRUE-LISTP Y)
(TRUE-LISTP Z)
(EQUAL (APPEND Y (CONS (CAR X1) (APPEND (CDR X1) Z)))
(APPEND Y (CONS (CAR X2) (APPEND (CDR X1) Z)))))
(EQUAL X1 X2))

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

])
Subgoal *1/3.2
Subgoal *1/3.1
Subgoal *1/3.1'
Subgoal *1/3.1''
Subgoal *1/3.1'''
Subgoal *1/3.1'4'
Subgoal *1/3.1'5'
Subgoal *1/3.1'6'

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

Subgoal *1/3.1
(IMPLIES (AND (CONSP X1)
(CONSP X2)
(NOT (EQUAL (APPEND Y (CDR X1) Z)
(APPEND Y (CDR X2) Z)))
(NOT (EQUAL (CDR X1) (CDR X2)))
(TRUE-LISTP (CDR X1))
(TRUE-LISTP (CDR X2))
(TRUE-LISTP Y)
(TRUE-LISTP Z))
(NOT (EQUAL (APPEND Y (CONS (CAR X1) (APPEND (CDR X1) Z)))
(APPEND Y
(CONS (CAR X2) (APPEND (CDR X2) Z))))))

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

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

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

Subgoal *1/2'''
(IMPLIES (AND (CONSP X1)
(TRUE-LISTP X1)
(TRUE-LISTP Y)
(TRUE-LISTP Z))
(NOT (EQUAL (APPEND Y X1 Z) (APPEND Y Z))))

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

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

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

Subgoal *1/1.2
Subgoal *1/1.1
Subgoal *1/1.1'

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

Subgoal *1/1.1'
(IMPLIES (AND (TRUE-LISTP X2)
(TRUE-LISTP Y)
(TRUE-LISTP Z)
(EQUAL (APPEND Y Z) (APPEND Y X2 Z)))
(NOT X2))

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

])

(IMPLIES (AND (TRUE-LISTP X2)
(TRUE-LISTP Y)
(TRUE-LISTP Z)
(EQUAL (APPEND Y Z) (APPEND Y X2 Z)))
(NOT X2)).
Subgoal *1.4/3
Subgoal *1.4/3'
Subgoal *1.4/2
Subgoal *1.4/1
Subgoal *1.4/1'
Subgoal *1.4/1''
Subgoal *1.4/1'''
Subgoal *1.4/1'4'

*1.4.1 (Subgoal *1.4/1'4') is pushed for proof by induction.

(IMPLIES (AND (TRUE-LISTP X2)
(TRUE-LISTP (APPEND X2 Z)))
(NOT X2)).
Subgoal *1.4.1/4
Subgoal *1.4.1/4'
Subgoal *1.4.1/4''
Subgoal *1.4.1/4'''
Subgoal *1.4.1/4'4'
Subgoal *1.4.1/4'5'
Subgoal *1.4.1/4'6'

A goal of NIL, Subgoal *1.4.1/4'6', has been generated!  Obviously,
the proof attempt has failed.

Summary
Form:  ( DEFTHM SANDWICH-EQUAL ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART TRUE-LISTP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION BINARY-APPEND)
(:INDUCTION SANDWICH-EQUAL-INDUCTION)
(:INDUCTION TRUE-LISTP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE CONS-EQUAL)
(:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION TRUE-LISTP))
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
Prover steps counted:  7420

---
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 (TRUE-LISTP X1)
(TRUE-LISTP X2)
(TRUE-LISTP Y)
(TRUE-LISTP Z))
(EQUAL (EQUAL (APPEND Y X1 Z) (APPEND Y X2 Z))
(EQUAL X1 X2)))

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

Subgoal *1/3.3'
(IMPLIES (AND (CONSP X1)
(CONSP X2)
(EQUAL (CDR X1) (CDR X2))
(TRUE-LISTP (CDR X1))
(TRUE-LISTP Y)
(TRUE-LISTP Z)
(EQUAL (APPEND Y (CONS (CAR X1) (APPEND (CDR X1) Z)))
(APPEND Y (CONS (CAR X2) (APPEND (CDR X1) Z)))))
(EQUAL X1 X2))

Subgoal *1/3.1
(IMPLIES (AND (CONSP X1)
(CONSP X2)
(NOT (EQUAL (APPEND Y (CDR X1) Z)
(APPEND Y (CDR X2) Z)))
(NOT (EQUAL (CDR X1) (CDR X2)))
(TRUE-LISTP (CDR X1))
(TRUE-LISTP (CDR X2))
(TRUE-LISTP Y)
(TRUE-LISTP Z))
(NOT (EQUAL (APPEND Y (CONS (CAR X1) (APPEND (CDR X1) Z)))
(APPEND Y
(CONS (CAR X2) (APPEND (CDR X2) Z))))))

Subgoal *1/2'''
(IMPLIES (AND (CONSP X1)
(TRUE-LISTP X1)
(TRUE-LISTP Y)
(TRUE-LISTP Z))
(NOT (EQUAL (APPEND Y X1 Z) (APPEND Y Z))))

Note: There is one additional key checkpoint under a top-level induction.
See :DOC set-checkpoint-summary-limit to change the number printed.

ACL2 Error in ( DEFTHM SANDWICH-EQUAL ...):  See :DOC failure.

******** FAILED ********
```

```Subgoal *1/2'''
(IMPLIES (AND (CONSP X1)
(TRUE-LISTP X1)
(TRUE-LISTP Y)
(TRUE-LISTP Z))
(NOT (EQUAL (APPEND Y X1 Z) (APPEND Y Z))))
```

`x1` の要素数が1以上であるために `(APPEND Y X1 Z)``(APPEND Y Z)` ではリストの長さが異なります。 リストの長さが異なるのであれば確実に `(NOT (EQUAL (APPEND Y X1 Z) (APPEND Y Z)))` です。 ということで、長さの違うリストは等しくないということを ACL2 に教えて上げましょう。

```(defthm different-len-implies-not-equal
(implies (not (equal (len x) (len y)))
(not (equal x y))))
```

```
Q.E.D.

Summary
Form:  ( DEFTHM DIFFERENT-LEN-IMPLIES-NOT-EQUAL ...)
Rules: ((:DEFINITION NOT)
(:FAKE-RUNE-FOR-TYPE-SET NIL))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  46
DIFFERENT-LEN-IMPLIES-NOT-EQUAL
```

また、 `(len (append x y))``(+ (len x) (len y))` と等しいという定理も必要です。

```(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:  355
LEN-APPEND
```

この状態で再度定理を証明してみましょう。

```(defthm sandwich-equal
(implies (and (true-listp x1)
(true-listp x2)
(true-listp y)
(true-listp z))
(equal (equal (append y x1 z)
(append y x2 z))
(equal x1 x2)))
:hints (("Goal" :induct (sandwich-equal-induction x1 x2))))
```

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

We have been told to use induction.  One induction scheme is suggested
by the induction hint.

We will induct according to a scheme suggested by
(SANDWICH-EQUAL-INDUCTION X1 X2).  This suggestion was produced using
the :induction rule SANDWICH-EQUAL-INDUCTION.  If we let (:P X1 X2 Y Z)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X1))
(NOT (ENDP X2))
(:P (CDR X1) (CDR X2) Y Z))
(:P X1 X2 Y Z))
(IMPLIES (AND (NOT (ENDP X1)) (ENDP X2))
(:P X1 X2 Y Z))
(IMPLIES (ENDP X1) (:P X1 X2 Y Z))).
This induction is justified by the same argument used to admit
SANDWICH-EQUAL-INDUCTION.  Note, however, that the unmeasured variable
X2 is being instantiated.  When applied to the goal at hand the above
induction scheme produces three nontautological subgoals.
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/3.3
Subgoal *1/3.3'
Subgoal *1/3.3''
Subgoal *1/3.3'''
Subgoal *1/3.3'4'
Subgoal *1/3.3'5'
Subgoal *1/3.3'6'
Subgoal *1/3.3'7'

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

Subgoal *1/3.3'
(IMPLIES (AND (CONSP X1)
(CONSP X2)
(EQUAL (CDR X1) (CDR X2))
(TRUE-LISTP (CDR X1))
(TRUE-LISTP Y)
(TRUE-LISTP Z)
(EQUAL (APPEND Y (CONS (CAR X1) (APPEND (CDR X1) Z)))
(APPEND Y (CONS (CAR X2) (APPEND (CDR X1) Z)))))
(EQUAL X1 X2))

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

])
Subgoal *1/3.2
Subgoal *1/3.1
Subgoal *1/3.1'
Subgoal *1/3.1''
Subgoal *1/3.1'''
Subgoal *1/3.1'4'
Subgoal *1/3.1'5'
Subgoal *1/3.1'6'

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

Subgoal *1/3.1
(IMPLIES (AND (CONSP X1)
(CONSP X2)
(NOT (EQUAL (APPEND Y (CDR X1) Z)
(APPEND Y (CDR X2) Z)))
(NOT (EQUAL (CDR X1) (CDR X2)))
(TRUE-LISTP (CDR X1))
(TRUE-LISTP (CDR X2))
(TRUE-LISTP Y)
(TRUE-LISTP Z))
(NOT (EQUAL (APPEND Y (CONS (CAR X1) (APPEND (CDR X1) Z)))
(APPEND Y
(CONS (CAR X2) (APPEND (CDR X2) Z))))))

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

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

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

Subgoal *1/2'''
(IMPLIES (AND (CONSP X1)
(TRUE-LISTP X1)
(TRUE-LISTP Y)
(TRUE-LISTP Z))
(NOT (EQUAL (APPEND Y X1 Z) (APPEND Y Z))))

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

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

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

Subgoal *1/1.2
Subgoal *1/1.1
Subgoal *1/1.1'

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

Subgoal *1/1.1'
(IMPLIES (AND (TRUE-LISTP X2)
(TRUE-LISTP Y)
(TRUE-LISTP Z)
(EQUAL (APPEND Y Z) (APPEND Y X2 Z)))
(NOT X2))

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

])

(IMPLIES (AND (TRUE-LISTP X2)
(TRUE-LISTP Y)
(TRUE-LISTP Z)
(EQUAL (APPEND Y Z) (APPEND Y X2 Z)))
(NOT X2)).
Subgoal *1.4/3
Subgoal *1.4/3'
Subgoal *1.4/2
Subgoal *1.4/1
Subgoal *1.4/1'
Subgoal *1.4/1''
Subgoal *1.4/1'''
Subgoal *1.4/1'4'

*1.4.1 (Subgoal *1.4/1'4') is pushed for proof by induction.

(IMPLIES (AND (TRUE-LISTP X2)
(TRUE-LISTP (APPEND X2 Z)))
(NOT X2)).
Subgoal *1.4.1/4
Subgoal *1.4.1/4'
Subgoal *1.4.1/4''
Subgoal *1.4.1/4'''
Subgoal *1.4.1/4'4'
Subgoal *1.4.1/4'5'
Subgoal *1.4.1/4'6'

A goal of NIL, Subgoal *1.4.1/4'6', has been generated!  Obviously,
the proof attempt has failed.

Summary
Form:  ( DEFTHM SANDWICH-EQUAL ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART TRUE-LISTP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION BINARY-APPEND)
(:INDUCTION SANDWICH-EQUAL-INDUCTION)
(:INDUCTION TRUE-LISTP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE CONS-EQUAL)
(:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION TRUE-LISTP))
Time:  0.03 seconds (prove: 0.03, print: 0.00, other: 0.00)
Prover steps counted:  12337

---
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 (TRUE-LISTP X1)
(TRUE-LISTP X2)
(TRUE-LISTP Y)
(TRUE-LISTP Z))
(EQUAL (EQUAL (APPEND Y X1 Z) (APPEND Y X2 Z))
(EQUAL X1 X2)))

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

Subgoal *1/3.3'
(IMPLIES (AND (CONSP X1)
(CONSP X2)
(EQUAL (CDR X1) (CDR X2))
(TRUE-LISTP (CDR X1))
(TRUE-LISTP Y)
(TRUE-LISTP Z)
(EQUAL (APPEND Y (CONS (CAR X1) (APPEND (CDR X1) Z)))
(APPEND Y (CONS (CAR X2) (APPEND (CDR X1) Z)))))
(EQUAL X1 X2))

Subgoal *1/3.1
(IMPLIES (AND (CONSP X1)
(CONSP X2)
(NOT (EQUAL (APPEND Y (CDR X1) Z)
(APPEND Y (CDR X2) Z)))
(NOT (EQUAL (CDR X1) (CDR X2)))
(TRUE-LISTP (CDR X1))
(TRUE-LISTP (CDR X2))
(TRUE-LISTP Y)
(TRUE-LISTP Z))
(NOT (EQUAL (APPEND Y (CONS (CAR X1) (APPEND (CDR X1) Z)))
(APPEND Y
(CONS (CAR X2) (APPEND (CDR X2) Z))))))

Subgoal *1/2'''
(IMPLIES (AND (CONSP X1)
(TRUE-LISTP X1)
(TRUE-LISTP Y)
(TRUE-LISTP Z))
(NOT (EQUAL (APPEND Y X1 Z) (APPEND Y Z))))

Note: There is one additional key checkpoint under a top-level induction.
See :DOC set-checkpoint-summary-limit to change the number printed.

ACL2 Error in ( DEFTHM SANDWICH-EQUAL ...):  See :DOC failure.

******** FAILED ********
```

`Subgoal *1/2'''` は残ったままですね。 `different-len-implies-not-equal` は使用されていないようです。 `Subgoal *1/2'''` の状況に合わせた定理を書いてみます。 `(not (equal (append y x1 z) (append y z)))` とあるので少し分かりずらいですが、 これは `(not (equal (append y (append x1 z)) (append y z)))` と同じ意味であり、 `y` の部分は共通しているため、 `(append x1 z)``z` が違うことを示してみましょう。

```(defthm sandwich-equal-lemma
(implies (and (consp x)
(true-listp x))
(not (equal (append x y) y))))
```

```
*1 (the initial Goal, a key checkpoint) 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 (APPEND X Y).  This
suggestion was produced using the :induction rules BINARY-APPEND and
TRUE-LISTP.  If we let (:P X Y) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X) Y))
(:P X Y))
(IMPLIES (ENDP X) (:P X Y))).
This induction is justified by the same argument used to admit BINARY-APPEND.
When applied to the goal at hand the above induction scheme produces
four nontautological subgoals.
Subgoal *1/4
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 SANDWICH-EQUAL-LEMMA ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION FIX)
(:DEFINITION LEN)
(:DEFINITION NOT)
(:DEFINITION TRUE-LISTP)
(:EXECUTABLE-COUNTERPART LEN)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION BINARY-APPEND)
(:INDUCTION TRUE-LISTP)
(:REWRITE CDR-CONS)
(:REWRITE COMMUTATIVITY-OF-+)
(:REWRITE DIFFERENT-LEN-IMPLIES-NOT-EQUAL)
(:REWRITE LEN-APPEND)
(:REWRITE UNICITY-OF-0)
(:TYPE-PRESCRIPTION LEN))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  583
SANDWICH-EQUAL-LEMMA
```

では `sandwich-equal` の証明を再度試みます。

```(defthm sandwich-equal
(implies (and (true-listp x1)
(true-listp x2)
(true-listp y)
(true-listp z))
(equal (equal (append y x1 z)
(append y x2 z))
(equal x1 x2)))
:hints (("Goal" :induct (sandwich-equal-induction x1 x2))))
```

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

We have been told to use induction.  One induction scheme is suggested
by the induction hint.

We will induct according to a scheme suggested by
(SANDWICH-EQUAL-INDUCTION X1 X2).  This suggestion was produced using
the :induction rule SANDWICH-EQUAL-INDUCTION.  If we let (:P X1 X2 Y Z)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X1))
(NOT (ENDP X2))
(:P (CDR X1) (CDR X2) Y Z))
(:P X1 X2 Y Z))
(IMPLIES (AND (NOT (ENDP X1)) (ENDP X2))
(:P X1 X2 Y Z))
(IMPLIES (ENDP X1) (:P X1 X2 Y Z))).
This induction is justified by the same argument used to admit
SANDWICH-EQUAL-INDUCTION.  Note, however, that the unmeasured variable
X2 is being instantiated.  When applied to the goal at hand the above
induction scheme produces three nontautological subgoals.
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/3.3
Subgoal *1/3.3'
Subgoal *1/3.3''
Subgoal *1/3.3'''
Subgoal *1/3.3'4'
Subgoal *1/3.3'5'
Subgoal *1/3.3'6'
Subgoal *1/3.3'7'

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

Subgoal *1/3.3'
(IMPLIES (AND (CONSP X1)
(CONSP X2)
(EQUAL (CDR X1) (CDR X2))
(TRUE-LISTP (CDR X1))
(TRUE-LISTP Y)
(TRUE-LISTP Z)
(EQUAL (APPEND Y (CONS (CAR X1) (APPEND (CDR X1) Z)))
(APPEND Y (CONS (CAR X2) (APPEND (CDR X1) Z)))))
(EQUAL X1 X2))

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

])
Subgoal *1/3.2
Subgoal *1/3.1
Subgoal *1/3.1'
Subgoal *1/3.1''
Subgoal *1/3.1'''
Subgoal *1/3.1'4'
Subgoal *1/3.1'5'
Subgoal *1/3.1'6'

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

Subgoal *1/3.1
(IMPLIES (AND (CONSP X1)
(CONSP X2)
(NOT (EQUAL (APPEND Y (CDR X1) Z)
(APPEND Y (CDR X2) Z)))
(NOT (EQUAL (CDR X1) (CDR X2)))
(TRUE-LISTP (CDR X1))
(TRUE-LISTP (CDR X2))
(TRUE-LISTP Y)
(TRUE-LISTP Z))
(NOT (EQUAL (APPEND Y (CONS (CAR X1) (APPEND (CDR X1) Z)))
(APPEND Y
(CONS (CAR X2) (APPEND (CDR X2) Z))))))

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

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

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

Subgoal *1/2'''
(IMPLIES (AND (CONSP X1)
(TRUE-LISTP X1)
(TRUE-LISTP Y)
(TRUE-LISTP Z))
(NOT (EQUAL (APPEND Y X1 Z) (APPEND Y Z))))

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

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

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

Subgoal *1/1.2
Subgoal *1/1.1
Subgoal *1/1.1'

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

Subgoal *1/1.1'
(IMPLIES (AND (TRUE-LISTP X2)
(TRUE-LISTP Y)
(TRUE-LISTP Z)
(EQUAL (APPEND Y Z) (APPEND Y X2 Z)))
(NOT X2))

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

])

(IMPLIES (AND (TRUE-LISTP X2)
(TRUE-LISTP Y)
(TRUE-LISTP Z)
(EQUAL (APPEND Y Z) (APPEND Y X2 Z)))
(NOT X2)).
Subgoal *1.4/3
Subgoal *1.4/3'
Subgoal *1.4/2
Subgoal *1.4/1
Subgoal *1.4/1'

*1.4 is COMPLETED!
Thus key checkpoint Subgoal *1/1.1' is COMPLETED!

We therefore turn our attention to *1.3, which is

(IMPLIES (AND (CONSP X1)
(TRUE-LISTP X1)
(TRUE-LISTP Y)
(TRUE-LISTP Z))
(NOT (EQUAL (APPEND Y X1 Z) (APPEND Y Z)))).
Subgoal *1.3/3
Subgoal *1.3/3'
Subgoal *1.3/2
Subgoal *1.3/1
Subgoal *1.3/1'

*1.3 is COMPLETED!
Thus key checkpoint Subgoal *1/2''' is COMPLETED!

We therefore turn our attention to *1.2, which is

(TRUE-LISTP Y))
(NOT (EQUAL (APPEND Y (CONS X2 BAD0))
Subgoal *1.2/4
Subgoal *1.2/3
Subgoal *1.2/2
Subgoal *1.2/1

*1.2 is COMPLETED!
Thus key checkpoint Subgoal *1/3.1 is COMPLETED!

We therefore turn our attention to *1.1, which is

(TRUE-LISTP Y)
(EQUAL (APPEND Y (CONS X2 BAD))
(EQUAL X2 X3)).
Subgoal *1.1/3
Subgoal *1.1/3'
Subgoal *1.1/2
Subgoal *1.1/1
Subgoal *1.1/1'

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

Q.E.D.

Summary
Form:  ( DEFTHM SANDWICH-EQUAL ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART TRUE-LISTP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION BINARY-APPEND)
(:INDUCTION SANDWICH-EQUAL-INDUCTION)
(:INDUCTION TRUE-LISTP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE CONS-EQUAL)
(:REWRITE SANDWICH-EQUAL-LEMMA)
(:TYPE-PRESCRIPTION BINARY-APPEND)
(:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION TRUE-LISTP))
Time:  0.04 seconds (prove: 0.03, print: 0.00, other: 0.00)
Prover steps counted:  13361
SANDWICH-EQUAL
```

```(defthm palindrome-sandwich
(implies (and (true-listp x)
(true-listp y))
(equal (palindromep (append y x (reverse y)))
(palindromep x))))
```

```
Q.E.D.

Summary
Form:  ( DEFTHM PALINDROME-SANDWICH ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE ASSOCIATIVITY-OF-APPEND)
(:REWRITE REV-APPEND)
(:REWRITE REV-REV)
(:REWRITE REVERSE-EQUAL-REV)
(:REWRITE SANDWICH-EQUAL)
(:TYPE-PRESCRIPTION REV)
(:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  364
PALINDROME-SANDWICH
```

## おわりに

リストの回文に関する性質を証明しました。

この記事だけみると思いついてからすぐに証明できたんかなって感じるかもしれませんが、 実際は帰納法の仕方に問題があるとか、 `sandwich-equal` 定理を書けばいいこととか、 `sandwich-equal-lemma` の必要性とかを発見するのに時間がかかって簡単ではなかったと記憶しています。 1番目の回文の定理(`x` が回文のとき `y``(reverse y)` に挟まれたものが回文であること)については簡単に証明できたような気がしています。

まあ、こんなしょうもないことを記事にするなと思われるかもしれませんが、 潜在的には存在するかもしれない日本語圏の ACL2 ユーザーが記事を書く心理的な障壁を下げるためにこれからもたくさん ACL2 の記事を投稿していきたいと思ってます。

ACL2 の日本語情報が私の記事ばかりになる前にプロの定理証明 ACL2 ユーザーが表出してくれることを願うばかりです。

Mastodon: @tojoqk