Запуск и тестирование свойства, выражающего связь между TAKE и APPEND

Question

По сути, мне нужно написать то, что написано в названии, единственное отношение, которое я смог придумать, - это если я беру некоторое количество элементов из списка с 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. Откройте его и запустите следующий код:

   (фунт) ракетка ланга (требуется (планета cce/dracula:8:23/lang/dracula))

3. Перезапустите доктора Ракета. Нажмите "Выбрать язык" в нижней части окна и выберите ACL2 под Dracula.

4. В меню Dracula выберите "Изменить путь к исполняемому файлу ACL2..." и выберите "run_acl2" (или "run_acl2.exe"), который находится в папке установки proofpad (т. Е. "C:\Program Files (x86)\Proof"). Pad", если у вас есть 64-битный ПК)

5. скачать PSP ++ и запустить его. Обязательно разархивируйте его в установочный каталог Proofpad, иначе он скажет, что не нашел нужных вещей.