Isabelle 中的代数简化

Question

我一直在玩 Isabelle 的基本证明示例。

考虑以下简单证明：

lemma
    fixes n::nat
    shows "n*(n+1) = n^2 + n"
    by simp

在我看来，像 Isabelle 这样强大的证明助手应该能够在没有太多指导的情况下证明这个引理。 然而，我惊讶地发现 Isabelle 在这里应用规则 simp 确实失败了（我还尝试了其他“通用”规则，例如 simp_all、auto em>, force, blast 但结果是一样的）。

如果我将最后一行替换为以下内容，则可以解决：

by (simp add: power2_eq_square)

我担心的是，我觉得我不应该告诉系统特定规则 power2_eq_square 来完成这个证明。

玩弄类似的琐碎例子，我发现 simp 能够证明

n*(n+2)=n*n+n*2

但失败了

n*(n+3)=n*n+n*3

最后一个例子得到证明

by (simp add: distrib_left)

为什么我需要在第二个示例中指定 distrib_left 而不是在第一个示例中指定（为什么？），这对我来说完全是个谜。

我给出这些例子并不是为了它们本身，而是主要是为了说明我的主要问题：

有没有办法自动验证常规代数身份，例如 Isabelle 中的上述情况？如果没有，那为什么不呢？有哪些技术障碍？

Answer 1

日常证明工作确实经常遇到“常规代数恒等式”；但是经过一些实践经验后，人们通常会产生一些直觉，如何有效地解决这些问题。我多年来开发的一种模式，例如：

context semidom
begin

lemma "a * (b ^ 2 + c) + 2 = a * b * b + c * a + 2"

典型的探索性证明以

开头

  apply auto

那么结合性和交换性也被考虑

  apply (auto simp add: ac_simps)

然后应用更多的代数规范化规则

  apply (auto simp add: algebra_simps)

最后一个缺口很容易被大锤填补

  apply (simp add: power2_eq_square)

之后，证明可以紧缩

  by (simp add: algebra_simps power2_eq_square)

Answer 2

引理

lemma power2_eq_square: "a^2 = a * a"

一般而言，这不是一个好的重写规则，因为它很容易破坏术语的大小。因此，预计 simp 这样的术语基于重写的自动化不会在没有您告知的情况下应用。

你想要的是某种证明搜索，Isabelle 提供了：写完引理后，你可以调用sledgehammer 工具，它会轻松快速地为你找到证明：

Sledgehammering... 
Proof found... 
"z3": Try this: by (simp add: power2_eq_square) (1 ms) 
"cvc4": Try this: by (simp add: power2_eq_square) (5 ms)