ACL2 不接受简单数值定理
Simple numeric theorem not accepted by ACL2
ACL2 不能证明以下定理：
(defthm thm-0
(implies
(and
(integerp n)
(oddp n)
(>= n 1))
(oddp (* n n))))
我的猜测是应该应用在奇数上步进两个的归纳方案：
(defun odd-induction (x)
"Induct by going two steps at a time"
(if (or (zp x) (equal x 1))
x
(+ 2 (odd-induction (1- x)))))
(defthm thm-0
(implies
(and
(integerp n)
(oddp n)
(>= n 1))
(oddp (* n n)))
:hints (("Goal" :induct (odd-induction n))) :rule-classes nil)
该定理仍未被接受。非常感谢对我错误或过于乐观的地方进行解释。
加法：
由于这个类似的定理在没有归纳提示的情况下被接受，我怀疑 thm-0 有其他问题。
(defthm thm-1
(implies
(and
(integerp o)
(integerp e)
(oddp o)
(evenp e))
(evenp (* o e))))
首先，很抱歉回复时间过长。我认为 ACL2 社区对 ACL2 帮助邮件列表上的查询的响应通常比在 Stack Overflow 等地方更快（即在一两天内），尽管我们中的一些人确实会不时尝试在此处检查 ACL2 标签。
ACL2 定义偶数和奇数时说如果 (integerp (/ x 2)) 则 x 是偶数，如果 x 不是偶数则 x 是奇数。不幸的是，这些定义有点笨拙，而且彼此之间不是很对称，所以关于 evenp 或 oddp 的一些定理很可能在 ACL2 可以证明它们之前需要大量的哄骗，即使它能够很容易证明关于 evenp 或 oddp 的其他定理。
例如，ACL2 可以通过以下推理证明您的thm-1：
e is even, meaning that (* e 1/2) is an integer. We want to prove that (* o e) is even, i.e. that (* (* o e) 1/2) is an integer. We expand out this latter expression to (* o e 1/2) using associativity of *. But since o is an integer and (* e 1/2) is known to be an integer, then (* o e 1/2) (which is really (* o (* e 1/2))) must also be an integer.
这是 ACL2 试图证明 thm-0 的失败尝试：
n is odd, meaning that (* n 1/2) is not an integer. We want to prove that (* (* n n) 1/2) is not an integer. Hmm. We expand out this latter expression to (* n n 1/2). Hmm. We normalize the (* n 1/2) inside this latter expression to (* 1/2 n) because we know * is commutative and our heuristics say that the constant 1/2 is "lighter" than the variable n. Hmm. Can't think of anything else to simplify, so let's move on to the next step in the waterfall, which is induction. But we can't figure out what to induct on because no recursive functions are involved.
这导致目标 (not (integerp (* n 1/2 n))) 和消息 "no induction schemes are suggested"。
是什么让第一个证明比第二个更容易？第一个证明依赖于 属性 整数集在乘法下是封闭的，即整数乘以整数必须是整数。在此证明中，类似的步骤是通过使用 n 是整数且 (* n 1/2) 是 non-integer 这一事实来证明 (* n n 1/2) 是 non-integer .
不幸的是，整数乘以 non-integer 并不一定是整数——例如，(* 2 1/2) 是整数。那么为什么 (* n (* n 1/2)) 不能是一个整数呢？为了解释原因，我们需要能够表达 (* n 1/2) 不仅仅是任何 non-integer 这一事实——特别是，它是一个分母为偶数的有理数，因为 n 是奇数, 乘以 n 不能从 (* n 1/2) 的分母中消去 2。从人类推理的角度来看，这是我能想到的最直接的方法来修复 ACL2 在上述证明中的不成功尝试，但是以 ACL2 可以理解的方式表述该论点可能有些困难——我会采取完全不同的方法并且使用归纳法，正如您尝试做的那样。
所以不幸的是，虽然你的 thm-0 和 thm-1 看起来与人类相似，但它们看起来与 ACL2 非常不同。
现在，我们如何证明你想要的定理？这是我的解决方案。 （请记住，解决 ACL2 中的某个问题通常有许多不同的方法，其他更有经验的用户可能会想出与我完全不同的解决方案。）
首先，很遗憾，您的 odd-induction 函数没有按照您的预期运行。该函数使用递减 1 的参数对自身进行递归，将 2 添加到结果，并且 returns。但是当你创建一个函数只是为了使用它的归纳方案时，函数 returns 是什么并不重要，重要的是它递归的特定方式——即所有递归调用是什么，它们的参数是什么，以及每次递归调用发生必须满足什么条件。
在这种情况下，有一个递归调用，参数为 (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 (+ -2 N)) 作为假设来证明 (:P N)。 （这里，:P指的是你试图通过归纳法证明的目标。）
为了避免直接推理除以二和事物是否为整数的混乱，让我们禁用 evenp 和 oddp。只推理 evenp 及其否定，而忘记 oddp 也会更简单，所以我们将在禁用 evenp 和 [=29] 之前证明一个促进这一点的定理=].
(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 是偶数，所以它们的和应该是偶数。如果我们证明事实上，子目标 *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))))
请注意，如果我们之前没有禁用 evenp，ACL2 已经 "know" 这个事实，使 evenp 的定义不可用。事实上，这就是我们能够通过在证明期间再次暂时启用 evenp 来证明该定理的方式。通常值得将 ACL2 "forget" 做成一堆东西，然后有选择地 re-prove 只有您实际需要的特定事实。
现在让我们尝试再次提交 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 重写器在 "clauses" 上运行，它是 "literals" 的析取，每个文字都是任意项。当一个目标看起来像
(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))))
那个工作得很好。请注意，为 two-summand 情况证明它就足够了，因为产生的重写规则将伸缩到更大数量的被加数。即当a、b、c、d为偶数时，要证明(+ a b c d)为偶数，ACL2会依次证明(+ 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))))
这个没用。检查点 ACL2 打印表示它在尝试证明 (* x 1/2 y) 是一个整数时卡住了，因为 (* 1/2 x) 是一个整数。如果我们可以将 (* x 1/2 y) 重新排列为 (* y 1/2 x)（与 (* y (* 1/2 x)) 相同），这样我们就可以在乘法下使用整数的闭包，那就太好了。
一种方法是在结论中交换 y 和 x 来证明定理，然后通过指定 :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-even 已成功证明，子目标 *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))))
这是我尝试证明你想要的特定定理的一种最懒惰的方式，但当然还有更强大的方法来处理它，例如构建关于 evenp 和 oddp 的有用定理的完整集合，从中可以得出像 thm-0 这样的特定情况。您可以在社区书籍 coi/super-ihs/evenp.
中找到 one such example
ACL2 不能证明以下定理：
(defthm thm-0
(implies
(and
(integerp n)
(oddp n)
(>= n 1))
(oddp (* n n))))
我的猜测是应该应用在奇数上步进两个的归纳方案：
(defun odd-induction (x)
"Induct by going two steps at a time"
(if (or (zp x) (equal x 1))
x
(+ 2 (odd-induction (1- x)))))
(defthm thm-0
(implies
(and
(integerp n)
(oddp n)
(>= n 1))
(oddp (* n n)))
:hints (("Goal" :induct (odd-induction n))) :rule-classes nil)
该定理仍未被接受。非常感谢对我错误或过于乐观的地方进行解释。
加法：
由于这个类似的定理在没有归纳提示的情况下被接受，我怀疑 thm-0 有其他问题。
(defthm thm-1
(implies
(and
(integerp o)
(integerp e)
(oddp o)
(evenp e))
(evenp (* o e))))
首先，很抱歉回复时间过长。我认为 ACL2 社区对 ACL2 帮助邮件列表上的查询的响应通常比在 Stack Overflow 等地方更快（即在一两天内），尽管我们中的一些人确实会不时尝试在此处检查 ACL2 标签。
ACL2 定义偶数和奇数时说如果 (integerp (/ x 2)) 则 x 是偶数，如果 x 不是偶数则 x 是奇数。不幸的是，这些定义有点笨拙，而且彼此之间不是很对称，所以关于 evenp 或 oddp 的一些定理很可能在 ACL2 可以证明它们之前需要大量的哄骗，即使它能够很容易证明关于 evenp 或 oddp 的其他定理。
例如，ACL2 可以通过以下推理证明您的thm-1：
eis even, meaning that(* e 1/2)is an integer. We want to prove that(* o e)is even, i.e. that(* (* o e) 1/2)is an integer. We expand out this latter expression to(* o e 1/2)using associativity of*. But sinceois an integer and(* e 1/2)is known to be an integer, then(* o e 1/2)(which is really(* o (* e 1/2))) must also be an integer.
这是 ACL2 试图证明 thm-0 的失败尝试：
nis odd, meaning that(* n 1/2)is not an integer. We want to prove that(* (* n n) 1/2)is not an integer. Hmm. We expand out this latter expression to(* n n 1/2). Hmm. We normalize the(* n 1/2)inside this latter expression to(* 1/2 n)because we know*is commutative and our heuristics say that the constant1/2is "lighter" than the variablen. Hmm. Can't think of anything else to simplify, so let's move on to the next step in the waterfall, which is induction. But we can't figure out what to induct on because no recursive functions are involved.
这导致目标 (not (integerp (* n 1/2 n))) 和消息 "no induction schemes are suggested"。
是什么让第一个证明比第二个更容易？第一个证明依赖于 属性 整数集在乘法下是封闭的，即整数乘以整数必须是整数。在此证明中，类似的步骤是通过使用 n 是整数且 (* n 1/2) 是 non-integer 这一事实来证明 (* n n 1/2) 是 non-integer .
不幸的是，整数乘以 non-integer 并不一定是整数——例如，(* 2 1/2) 是整数。那么为什么 (* n (* n 1/2)) 不能是一个整数呢？为了解释原因，我们需要能够表达 (* n 1/2) 不仅仅是任何 non-integer 这一事实——特别是，它是一个分母为偶数的有理数，因为 n 是奇数, 乘以 n 不能从 (* n 1/2) 的分母中消去 2。从人类推理的角度来看，这是我能想到的最直接的方法来修复 ACL2 在上述证明中的不成功尝试，但是以 ACL2 可以理解的方式表述该论点可能有些困难——我会采取完全不同的方法并且使用归纳法，正如您尝试做的那样。
所以不幸的是，虽然你的 thm-0 和 thm-1 看起来与人类相似，但它们看起来与 ACL2 非常不同。
现在，我们如何证明你想要的定理？这是我的解决方案。 （请记住，解决 ACL2 中的某个问题通常有许多不同的方法，其他更有经验的用户可能会想出与我完全不同的解决方案。）
首先，很遗憾，您的 odd-induction 函数没有按照您的预期运行。该函数使用递减 1 的参数对自身进行递归，将 2 添加到结果，并且 returns。但是当你创建一个函数只是为了使用它的归纳方案时，函数 returns 是什么并不重要，重要的是它递归的特定方式——即所有递归调用是什么，它们的参数是什么，以及每次递归调用发生必须满足什么条件。
在这种情况下，有一个递归调用，参数为 (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 (+ -2 N)) 作为假设来证明 (:P N)。 （这里，:P指的是你试图通过归纳法证明的目标。）
为了避免直接推理除以二和事物是否为整数的混乱，让我们禁用 evenp 和 oddp。只推理 evenp 及其否定，而忘记 oddp 也会更简单，所以我们将在禁用 evenp 和 [=29] 之前证明一个促进这一点的定理=].
(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 是偶数，所以它们的和应该是偶数。如果我们证明事实上，子目标 *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))))
请注意，如果我们之前没有禁用 evenp，ACL2 已经 "know" 这个事实，使 evenp 的定义不可用。事实上，这就是我们能够通过在证明期间再次暂时启用 evenp 来证明该定理的方式。通常值得将 ACL2 "forget" 做成一堆东西，然后有选择地 re-prove 只有您实际需要的特定事实。
现在让我们尝试再次提交 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 重写器在 "clauses" 上运行，它是 "literals" 的析取，每个文字都是任意项。当一个目标看起来像
(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))))
那个工作得很好。请注意，为 two-summand 情况证明它就足够了，因为产生的重写规则将伸缩到更大数量的被加数。即当a、b、c、d为偶数时，要证明(+ a b c d)为偶数，ACL2会依次证明(+ 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))))
这个没用。检查点 ACL2 打印表示它在尝试证明 (* x 1/2 y) 是一个整数时卡住了，因为 (* 1/2 x) 是一个整数。如果我们可以将 (* x 1/2 y) 重新排列为 (* y 1/2 x)（与 (* y (* 1/2 x)) 相同），这样我们就可以在乘法下使用整数的闭包，那就太好了。
一种方法是在结论中交换 y 和 x 来证明定理，然后通过指定 :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-even 已成功证明，子目标 *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))))
这是我尝试证明你想要的特定定理的一种最懒惰的方式，但当然还有更强大的方法来处理它，例如构建关于 evenp 和 oddp 的有用定理的完整集合，从中可以得出像 thm-0 这样的特定情况。您可以在社区书籍 coi/super-ihs/evenp.