基本的に、私はタイトルが言うことを書く必要があります.私が考えることができた唯一の関係は、リストからいくつかの要素をTAKE取り、次にそれほど重要ではない残りの半分を取り、CDR次にAPPEND2つの元のリストと同じであることを証明するために取ったものです。(それを構築するのに長い時間を費やした後)、証明は問題ないように見えますが (問題なくコンパイルされます)、何らかの理由で実行時に失敗します。情報が必要な場合に備えて、Dracula で Proofpad を使用しています。
コードは次のとおりです。
(include-book "doublecheck" :dir :teachpacks)
(defproperty take-append-relationship-test ;not sure why this fails.
(xs :value (random-integer-list))
(iff (consp xs)
(let* ((x1 (take 1 xs))
(xs2 (cdr xs)))
(equal (append x1 xs2)
xs))))
ここに私が得るエラーログがあります。
By the simple :definition TAKE we reduce the conjecture to
Goal'
(COND ((CONSP XS)
(LET ((X1 (FIRST-N-AC 1 XS NIL)))
(EQUAL (APPEND X1 (CDR XS)) XS)))
((LET ((X1 (FIRST-N-AC 1 XS NIL)))
(EQUAL (APPEND X1 (CDR XS)) XS))
NIL)
(T T)).
This simplifies, using the :definition FIRST-N-AC, the :executable-
counterparts of BINARY-+, BINARY-APPEND, CONS, FIRST-N-AC and ZP, primitive
type reasoning and the :rewrite rules DEFAULT-CAR and DEFAULT-CDR,
to
Goal''
(IMPLIES (CONSP XS)
(EQUAL (APPEND (FIRST-N-AC 1 XS NIL) (CDR XS))
XS)).
The destructor terms (CAR XS) and (CDR XS) can be eliminated by using
CAR-CDR-ELIM to replace XS by (CONS XS1 XS2), (CAR XS) by XS1 and (CDR XS)
by XS2. This produces the following goal.
Goal'''
(IMPLIES (CONSP (CONS XS1 XS2))
(EQUAL (APPEND (FIRST-N-AC 1 (CONS XS1 XS2) NIL)
XS2)
(CONS XS1 XS2))).
This simplifies, using primitive type reasoning, to
Goal'4'
(EQUAL (APPEND (FIRST-N-AC 1 (CONS XS1 XS2) NIL)
XS2)
(CONS XS1 XS2)).
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.)
No induction schemes are suggested by *1. Consequently, the proof
attempt has failed.
Summary
Form: ( DEFTHM TAKE-APPEND-RELATIONSHIP-TEST ...)
Rules: ((:DEFINITION FIRST-N-AC)
(:DEFINITION IFF)
(:DEFINITION TAKE)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART BINARY-APPEND)
(:EXECUTABLE-COUNTERPART CONS)
(:EXECUTABLE-COUNTERPART FIRST-N-AC)
(:EXECUTABLE-COUNTERPART ZP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE DEFAULT-CAR)
(:REWRITE DEFAULT-CDR))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 328
---
The key checkpoint goal, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---
*** Key checkpoint before reverting to proof by induction: ***
Goal''
(IMPLIES (CONSP XS)
(EQUAL (APPEND (FIRST-N-AC 1 XS NIL) (CDR XS))
XS))
ACL2 Error in ( DEFTHM TAKE-APPEND-RELATIONSHIP-TEST ...): See :DOC
failure.
******** FAILED ********
誰かが少なくとも私を正しい方向に向けることができますか? エラーログを読んだところ、何らかの冗長性があることがわかりました。これを修正する方法がまったくわかりません。
それを行うと（の'(1 2 3 4)代わりに(random-integer-list)）、エラーがスローされます：
ACL2 Error in TOP-LEVEL: One value, '(1 2 3 4 5), is being returned
where 2 values were expected. Note: This error occurred in the context
(MV-LET (XS STATE)
'(1 2 3 4 5)
(IF T
(MV-LET (STATE RESULT ASSIGNMENTS)
(EXPAND-VARS NIL (IFF # #))
(MV STATE RESULT (CONS # ASSIGNMENTS)))
(MV STATE 'WHERE-NOT-MATCHED NIL))).
(See :DOC set-iprint to be able to see elided values in this message.)
私のセットアップ：
- ラケットを取り付ける
それを開いて、次のコードを実行します。
(ポンド)lang ラケット (require (planet cce/dracula:8:23/lang/dracula))
Dr ラケットを再起動します。ウィンドウの下部にある [Choose Language] をクリックし、Dracula の下にある ACL2 を選択します。
Dracula メニューから、[Change ACL2 Executable Path...] を選択し、プルーフパッドのインストール フォルダー (つまり、"C:\Program Files (x86)\Proof") にある "run_acl2" (または "run_acl2.exe") を選択します。 Pad」、64 ビット PC を使用している場合)
PSP++ をダウンロードして実行します。Proofpad のインストール ディレクトリで必ず解凍してください。そうしないと、必要なものが見つからなかったことを知らせるメッセージが表示されます。