带否定的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的人通常会包含相关的库。在本例中，我将使用“算术/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...)“