acl2 равенство с отрицанием

Question

У меня проблемы с acl2, пытаюсь доказать следующее:

(thm (implies (acl2-numberp x) (equal (* -2 x) (* 2 (- x)))))

что приводит к:

ACL2 !>(thm (implies (acl2-numberp x) (equal (* -2 x) (* 2 (- x)))))

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

No induction schemes are suggested by *1. Consequently, the proof
attempt has failed.

Summary
Form: ( THM ...)
Rules: NIL
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 63

---
The key checkpoint goal, 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 (ACL2-NUMBERP X)
(EQUAL (* -2 X) (* 2 (- X))))

ACL2 Error in ( THM ...): See :DOC failure.

******** FAILED ********

Тем не менее, когда я пытаюсь:

(thm (implies (acl2-numberp x) (equal (* -1 x) (* 1 (- x)))))

это легко удается. Кто-нибудь знает, почему это происходит и как это исправить?

Answer 1

Часто люди ожидают, что ACL2 сможет рассуждать обо всем "из коробки". На практике те из нас, кто использует ACL2, часто включают соответствующие библиотеки. В этом примере я бы использовал библиотеку "arithmetic/top".

ACL2 !>(include-book "arithmetic/top" :dir :system)

Summary
Form:  ( INCLUDE-BOOK "arithmetic/top" ...)
<snip>
ACL2 !>(thm (implies (acl2-numberp x) (equal (* -2 x) (* 2 (- x)))))

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:EXECUTABLE-COUNTERPART IF)
        (:REWRITE FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-LEFT)
        (:REWRITE FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-RIGHT))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  23

Proof succeeded.
ACL2 !>

Чтобы ответить на ваш вопрос относительно "почему", это потому, что ACL2 имеет встроенные правила для канонизации "(* -1 ..)", но не "(* -2 ...)"