ACL2 でリストの回文に関する性質を証明した
目次
投稿日: 2022-04-04 月
注意
この記事はいま思うとあまりよく分かっていなかったときに書いたものなので参考にしない方がいいです。 近々、本当に役に立つ初心者向けの記事を書く予定なので作成しだいここにリンクを張る予定です。
はじめに
これは私が過去に書いた https://git.tojo.tokyo/acl2-theorems.git/tree/palindrome-sandwich.lisp を記事にして解説したものです。 このプログラムを作成した 2021/07/19 の当時と比べると ACL2 の扱いに少し慣れてきているためプログラムを修正しています。
本記事中のプログラムのライセンスは三条項BSDライセンスとします。
回文の何について証明したいのか
本記事では次の二つを証明します。
- 「リスト
xとyについて、xが回文のときyと(reverse y)でxを挟んだリスト(append y x (reverse y))は回文である」 - 「リスト
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
何故関数ではなくてマクロを書いているかというと、 ACL2 は再帰しない関数を定理の左辺に書くと証明時に関数の展開を止めない限り定理の rewrite ルールではマッチしないという厄介な問題があるのでそうしています。
準備: 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
for more information.
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
documentation for more information.
Function: <revappend>
(defun revappend (x y)
(declare (xargs :guard (true-listp x)))
(if (endp x)
y (revappend (cdr x) (cons (car x) y))))
末尾再帰の関数は定理を証明するときに若干扱いにくいので、 reverse
を直感的ではあるけど実行速度の遅い rev という関数を定義して、
証明時には reverse を rev に変換するようにします(末尾再帰の関数だと状態変数の変化を追い掛けるのが面倒なのです)。
rev は下記のように定義します。 アトムがきたら nil, さもなくば (append (rev (cdr x)) (list (car x)))
を返します(そのまま)。
末尾再帰のものと比べて計算量が大きいので実際のプログラミングでこの定義が使われることはまずありませんが、
定理証明するときには結構便利です。
(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'
So we now return to *1.1, which is
(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
自動証明されました。
revappend が証明できたなら reverse もいけるでしょう。
reverse は文字列の場合についても考慮されているので、
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.
])
So we now return to *1.3, which is
(IMPLIES (TRUE-LISTP BAD)
(EQUAL (REV BAD) BAD)).
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'
So we now return to *1.3.1, which is
(IMPLIES (TRUE-LISTP BAD2)
(EQUAL (APPEND BAD2 (LIST BAD1))
(CONS BAD1 (REV BAD2)))).
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'
So we now return to *1.3.1.2, which is
(IMPLIES (TRUE-LISTP BAD4)
(EQUAL (APPEND BAD4 (LIST BAD1))
(APPEND (REV BAD4) (LIST BAD3)))).
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''' に注目しましょう。
これは (rev (append y (rev y)) をうまく書き換えて、
append を外側に弾きだせば式が (append y (rev y)) に近づきそうです。
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'
So we now return to *1.1, which is
(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
再度 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)
証明失敗: 出力を確認する
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.
])
So we now return to *1.3, which is
(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.
So we now return to *1.3.2, which is
(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'
So we now return to *1.3.2.1, which is
(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'
So we now return to *1.2, which is
(IMPLIES (AND (TRUE-LISTP BAD)
(TRUE-LISTP RV)
(TRUE-LISTP RV0)
(TRUE-LISTP X2)
(EQUAL (APPEND (APPEND Y RV) RV0)
(APPEND Y BAD))
(TRUE-LISTP (CONS X1 X2))
(TRUE-LISTP Y)
(EQUAL (APPEND RV (LIST X1))
(CONS X1 X2)))
(EQUAL (APPEND (APPEND Y (CONS X1 X2)) RV0)
(APPEND Y (CONS X1 BAD)))).
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
So we now return to *1.2.1, which is
(IMPLIES (AND (TRUE-LISTP BAD)
(TRUE-LISTP RV)
(TRUE-LISTP RV0)
(TRUE-LISTP X2)
(TRUE-LISTP (CONS X1 X2))
(EQUAL (APPEND RV (LIST X1))
(CONS X1 X2)))
(EQUAL (APPEND X2 RV0) BAD)).
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.
So we now return to *1.2.1.3, which is
(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
証明できました。
「 x が回文なら (append y x (reverse y)) も回文」という定理については、
自動証明に失敗した原因を単純に取り除くだけで証明できる感じですね。
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'
So we now return to *1.1, which is
(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.
So we now return to *1.1.1, which is
(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.
So we now return to *1.1.1.3, which is
(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.
])
So we now return to *1.3, which is
(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.
So we now return to *1.3.1, which is
(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.
])
So we now return to *1.4, which is
(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.
So we now return to *1.4.1, which is
(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 がでてきました。
Subgoal *1/2''' を見てみましょう。
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.
])
So we now return to *1.4, which is
(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.
So we now return to *1.4.1, which is
(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
証明できました。Summary の Rules に (:REWRITE DIFFERENT-LEN-IMPLIES-NOT-EQUAL) があることに注意してください。
ACL2 は長さが違うリストは等しくないという定理を利用して証明してくれました。
正直どうしてただの rewrite ルールでそんなことができるのかはよく分かっていません……。
なんとなく ACL2 に期待してやってみたらうまくいっちゃったって感じです。
いつかしっかり勉強してなぜ上手くいくのか調べたいと思います。
では 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.
])
So we now return to *1.4, which is
(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
(IMPLIES (AND (TRUE-LISTP BAD)
(TRUE-LISTP BAD0)
(NOT (EQUAL (APPEND Y BAD0) (APPEND Y BAD)))
(TRUE-LISTP Y))
(NOT (EQUAL (APPEND Y (CONS X2 BAD0))
(APPEND Y (CONS X3 BAD))))).
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
(IMPLIES (AND (TRUE-LISTP BAD)
(TRUE-LISTP Y)
(EQUAL (APPEND Y (CONS X2 BAD))
(APPEND Y (CONS X3 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 の日本語情報が私の記事ばかりになる前にプロの定理証明 ACL2 ユーザーが表出してくれることを願うばかりです。