2

基本上，我需要写一个标题所说的内容，我能想到的唯一关系是，如果我从列表中取出一些元素TAKE，然后取出不那么重要的另一半，然后再CDR取出APPEND两个我用来证明它与原始列表相同。（经过长时间的痛苦构建），证明似乎很好（它编译得很好），但由于某种原因，它在运行时失败了。我正在将 Proofpad 与 Dracula 一起使用，以防您需要信息。

这是代码： 

(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.)

我的设置：

  1. 安装球拍

  2. 打开它并运行以下代码：

    (磅)lang 球拍 (需要 (planet cce/dracula:8:23/lang/dracula))

  3. 重新启动 Racket 博士。单击窗口底部的“选择语言”，然后在 Dracula 下选择 ACL2。

  4. 从 Dracula 菜单中，选择“Change ACL2 Executable Path...”，然后选择位于 proofpad 安装文件夹（即“C:\Program Files (x86)\Proof”中的“run_acl2”（或“run_acl2.exe”） Pad”，如果您有 64 位 PC）

  5. 下载 PSP++ 并运行它。一定要解压到Proofpad的安装目录下，不然会告诉你没找到需要的东西。

4

0 回答 0