首先，很抱歉回复时间长。我认为 ACL2 社区对 ACL2 帮助邮件列表上的查询的响应通常比在 Stack Overflow 之类的地方更快（即在一两天内），尽管我们中的一些人确实不时尝试在这里检查 ACL2 标记。
ACL2 通过说x是偶数来定义偶数(integerp (/ x 2))和x奇数，如果x不是偶数则为奇数。不幸的是，这些定义有点笨拙，并且彼此之间不是很对称，因此在 ACL2 能够证明它们之前，对于一些关于evenp或oddp需要大量哄骗的定理很有可能，即使它能够证明关于evenp或oddp非常容易的其他定理。
例如，ACL2 能够thm-1通过以下推理来证明你：
e是偶数，意思(* e 1/2)是整数。我们要证明它(* o e)是偶数，即它(* (* o e) 1/2)是一个整数。我们将后一个表达式扩展为(* o e 1/2)使用 的关联性*。但既然o是一个整数并且(* e 1/2)已知是一个整数，那么(* o e 1/2)（实际上是(* o (* e 1/2))）也必须是一个整数。
这是 ACL2 试图证明的失败尝试thm-0：
n是奇数，这意味着它(* n 1/2)不是整数。我们要证明它(* (* n n) 1/2)不是整数。唔。我们将后一个表达式扩展为(* n n 1/2)。唔。(* n 1/2)我们将后一个表达式的内部规范化为，(* 1/2 n)因为我们知道*是可交换的，并且我们的启发式方法说常1/2量比变量“轻” n。唔。想不出还有什么可以简化的，所以让我们进入瀑布的下一步，即归纳。但是我们不知道要对什么进行归纳，因为不涉及递归函数。
这导致目标(not (integerp (* n 1/2 n)))和消息“不建议归纳方案”。
是什么让第一个证明比第二个更容易？第一个证明依赖于整数集在乘法下闭合的性质，即整数乘以整数必须是整数。在这个证明中，类似的步骤是通过使用整数和非(* n n 1/2)整数的事实来证明是非整数。n(* n 1/2)
不幸的是，整数乘以非整数一定是整数是不正确的——例如，(* 2 1/2)是整数。那么为什么不能(* n (* n 1/2))是整数呢？为了解释为什么，我们需要能够表达的事实(* n 1/2)不仅仅是任何非整数——特别是，它是一个分母为偶数的有理数，因为n是奇数，所以乘以n不能抵消2分母的(* n 1/2)。从人类推理的角度来看，这是我能想到的最直接的方法来解决 ACL2 在上述证明中的不成功尝试，但是以 ACL2 可以理解的方式制定该论点可能有些困难——我会完全采取不同的方法，并且使用归纳法，就像您尝试做的那样。
所以不幸的是，虽然你的thm-0和thm-1看起来与人类相似，但它们看起来与 ACL2 完全不同。
现在，我们如何证明你想要的定理？这是我的解决方案。（请记住，在 ACL2 中解决某个问题通常有很多不同的方法，其他更有经验的用户可能会提出与我完全不同的解决方案。）
首先，不幸的是，您的奇数归纳函数没有按照您的意图进行。该函数使用自减 1 的参数对自身进行递归，将结果加 2，然后返回。但是当你创建一个函数只是为了使用它的归纳方案时，函数返回什么并不重要，只关心它递归的特定方式——即所有递归调用是什么，它们的参数是什么是，以及每个递归调用的发生必须满足什么条件。
在这种情况下，有一个带有参数的递归调用，(1- x)当两者(zp x)都不(equal x 1)为真时发生。关于函数的其他一切都是无关紧要的。因此，归纳方案具有基本情况(or (zp x) (equal x 1))和归纳步骤(P (1- x))=> (P x)。但是你想要的是归纳步骤是(P (- x 2))=> (P x)。所以这里有一个更好的归纳方案函数：
(defun odd-induction (x)
"Induct by going two steps at a time"
(or (zp x)
(equal x 1)
(odd-induction (- x 2))))
让我们试试最后定理，看看归纳法是什么样子的。请注意，您的归纳方案实际上仅适用于自然数，而不是所有整数，因此我将保留我们仅证明有关正奇数而不是负奇数的此属性的限制。
(defthm thm-0
(implies (and (natp n)
(oddp n))
(oddp (* n n)))
:hints (("Goal" :induct (odd-induction n))))
这失败了，但让我们忽略最后的检查点并查看输出的顶部，其中选择了归纳方案：
We have been told to use induction. One induction scheme is suggested
by the induction hint.
We will induct according to a scheme suggested by (ODD-INDUCTION N).
This suggestion was produced using the :induction rule ODD-INDUCTION.
If we let (:P N) denote *1 above then the induction scheme we'll use
is
(AND (IMPLIES (AND (NOT (ZP N))
(NOT (EQUAL N 1))
(:P (+ -2 N)))
(:P N))
(IMPLIES (AND (NOT (ZP N)) (EQUAL N 1))
(:P N))
(IMPLIES (ZP N) (:P N))).
所以你可以看到，在归纳步骤中，它将尝试证明(:P N)使用(:P (+ -2 N))作为假设。（在这里，:P指的是你试图通过归纳来证明的目标。）
为了避免直接推理除以二以及事物是否为整数的混乱，让我们同时禁用evenp和oddp。仅仅推理evenp和它的否定，而忘记也更简单oddp，所以我们将在禁用evenp和之前证明一个有助于这一点的定理oddp。
(defthm oddp-is-not-evenp
(equal (oddp x)
(not (evenp x))))
(in-theory (disable evenp oddp))
让我们再次尝试提交thm-0，并注意这次的检查点。
Subgoal *1/3.2
(IMPLIES (AND (NOT (ZP N))
(NOT (EQUAL N 1))
(NOT (EVENP (+ 4 (* -2 N) (* -2 N) (* N N))))
(<= 0 N)
(NOT (EVENP N)))
(NOT (EVENP (* N N))))
Subgoal *1/3.1
(IMPLIES (AND (NOT (ZP N))
(NOT (EQUAL N 1))
(EVENP (+ -2 N))
(<= 0 N)
(NOT (EVENP N)))
(NOT (EVENP (* N N))))
从中我们可以看出，ACL2 已经开始归纳证明*1，并且卡住了第三种情况 ( *1/3)，它已经分裂成子目标，其中两个 (*1/3.1和*1/3.2) 它无法证明。
看看 的假设*1/3.1，我们看到他们声称这n不是偶数，而是(+ -2 n)偶数。我们还可以看到它n是一个整数，因为(not (zp n))它成立。这是不可能的，因为-2是偶数并且n是偶数，所以它们的总和应该是偶数。如果我们证明了这一事实，那么 Subgoal*1/3.1应该会消失。
(defthm even-plus-odd-is-odd
(implies (and (evenp x)
(not (evenp y)))
(not (evenp (+ x y))))
:hints (("Goal" :in-theory (enable evenp))))
请注意，如果我们之前没有禁用，ACL2 已经“知道”这个事实evenp，从而使定义evenp不可用。事实上，这就是我们能够通过evenp在证明期间再次启用来证明这个定理的方式。通常值得让 ACL2 “忘记”一堆东西，然后有选择地只重新证明您实际需要的特定事实。
thm-0现在让我们再次尝试提交。这次我们只得到一个子目标：
Subgoal *1/3.2
(IMPLIES (AND (NOT (ZP N))
(NOT (EQUAL N 1))
(NOT (EVENP (+ 4 (* -2 N) (* -2 N) (* N N))))
(<= 0 N)
(NOT (EVENP N)))
(NOT (EVENP (* N N))))
好的，我们怎样才能让这个消失？IMO，查看此子目标的最佳方法是将其中一个假设转变为结论。ACL2 重写器对“子句”起作用，“子句”是“文字”的析取，每个文字都是任意术语。当一个目标看起来像
(implies (and [A]
[B]
[C])
[D])
对于某些术语 A、B、C 和 D，ACL2 在内部实际上正在尝试证明
(or (not [A])
(not [B])
(not [C])
D)
ACL2 将尝试依次简化上述表达式中的四个析取项中的每一个，当它简化一个时，其他三个被视为假设。所以回到我们的子目标，如果我们重新排列子句来想象 ACL2 在简化包含代数表达式的文字时会看到什么，可能会更容易看到如何解决问题(+ 4 (* -2 n) (* -2 n) (* n n))：
(IMPLIES (AND (NOT (ZP N))
(NOT (EQUAL N 1))
(EVENP (* N N))
(<= 0 N)
(NOT (EVENP N)))
(EVENP (+ 4 (* -2 N) (* -2 N) (* N N))))
旁白：您可能会注意到假设中的矛盾——我们有一个假设说n不是偶数，而另一个假设(* n n)是偶数！- 但这是一个矛盾的事实是我们首先试图证明的，所以我们不能通过注意到这个矛盾来解决这个子目标。
现在，我们如何证明这(+ 4 (* -2 n) (* -2 n) (* n n))是偶数？嗯，它是四个偶数的总和。 4显然是一个偶数——ACL2 可以直接计算表达式(evenp 4)来满足这个事实。 (* -2 n)是偶数，因为n是偶数且偶数 ( -2) 乘以任何整数都是偶数。甚至是因为其中(* n n)一个假设是这样说的。
所以，如果我们可以教 ACL2 上一段中使用的关于均匀度的事实，我们应该很好。首先我们证明偶数之和是偶数。
(defthm even-plus-even-is-even
(implies (and (evenp x)
(evenp y))
(evenp (+ x y)))
:hints (("Goal" :in-theory (enable evenp))))
那个工作得很好。请注意，证明它适用于两个加法的情况就足够了，因为产生的重写规则将扩大到更大数量的加法。也就是说，为了证明(+ a b c d)是偶数，当a、b、c和是偶数时，ACL2 将依次使用重写规则 3 次d证明(+ c d)、(+ b c d)和 最后是偶数。(+ a b c d)even-plus-even-is-even
接下来我们尝试证明偶数乘以任何整数是偶数。
(defthm even-times-integer-is-even
(implies (and (evenp x)
(integerp y))
(evenp (* x y)))
:hints (("Goal" :in-theory (enable evenp))))
这个没用。(* x 1/2 y)检查点 ACL2 打印说它在试图证明它是一个整数时卡住了，因为它(* 1/2 x)是一个整数。如果我们可以重新排列(* x 1/2 y)to (* y 1/2 x)（与 相同(* y (* 1/2 x))）这样我们可以在乘法下使用整数的闭包，那就太好了。
一种方法是仅证明定理y并x在结论中交换，然后通过指定 a 来生成我们实际想要的重写:corollary：
(defthm even-times-integer-is-even
(implies (and (evenp x)
(integerp y))
(evenp (* y x))) ; note that x and y are swapped
:hints (("Goal" :in-theory (enable evenp)))
:rule-classes
((:rewrite :corollary
(implies (and (evenp x)
(integerp y))
(evenp (* x y)))))) ; x and y in the correct order
(* y x)主定理陈述和推论之间的转换非常简单，即使使用表格证明了定理(* x y)，ACL2 也可以满足将重写规则存储在表格中。(* x y)(* y x)
我可以想出一些其他方法来证明这个定理even-times-integer-is-even，这些方法可能比上面的方法少一些，但我不会深入探讨它们，因为它们需要更多的引理。
既然已经成功证明even-plus-even-is-even，even-times-integer-is-evenSubgoal*1/3.2应该会消失——确实如此。
作为参考，这是用于证明的整个代码体thm-0：
(defun odd-induction (x)
"Induct by going two steps at a time"
(or (zp x)
(equal x 1)
(odd-induction (- x 2))))
(defthm oddp-is-not-evenp
(equal (oddp x)
(not (evenp x))))
(in-theory (disable evenp oddp))
(defthm even-plus-odd-is-odd
(implies (and (evenp x)
(not (evenp y)))
(not (evenp (+ x y))))
:hints (("Goal" :in-theory (enable evenp))))
(defthm even-plus-even-is-even
(implies (and (evenp x)
(evenp y))
(evenp (+ x y)))
:hints (("Goal" :in-theory (enable evenp))))
(defthm even-times-integer-is-even
(implies (and (evenp x)
(integerp y))
(evenp (* y x))) ; note that x and y are swapped
:hints (("Goal" :in-theory (enable evenp)))
:rule-classes
((:rewrite :corollary
(implies (and (evenp x)
(integerp y))
(evenp (* x y)))))) ; x and y in the correct order
(defthm thm-0
(implies (and (natp n)
(oddp n))
(oddp (* n n)))
:hints (("Goal" :induct (odd-induction n))))
这是我试图证明你想要的特定定理的一种最大程度的懒惰方式，但当然还有更强大的方法来处理它，例如建立一个关于偶数和奇数的有用定理的完整集合，具体情况thm-0喜欢跟随。您可以在社区手册中找到一个这样的示例coi/super-ihs/evenp。