acl2 等于否定答案

【问题标题】：acl2 equality with negationacl2 等于否定
【发布时间】：2014-09-21 04:45:00
【问题描述】：

我在使用 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)))))

它很容易成功。有谁知道为什么会发生这种情况以及如何解决？

【问题讨论】：

标签： equality negation acl2

【解决方案1】：

人们通常期望 ACL2 能够“开箱即用”地推理一切。在实践中，我们这些使用 ACL2 的人通常会包含相关的库。在本例中，我将使用“算术/顶级”库。

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 ...)”的内置规则

【讨论】：