为什么在 Isabelle 中证明自然数的简单可计算相等性时必须使用 "numeral_nat" 或 "numeral.simps"

Question

采用阶乘函数的标准定义：

primrec factorial :: "nat ⇒ nat"
  where
    "factorial 0 = 1"
  | "factorial (Suc n) = (Suc n) * (factorial n)"

如果我们要求 value "factorial 3"，Isabelle 会出乎意料地给我们 6。但是，如果我们试图将其作为引理，它将失败：

lemma "factorial (3::nat) = (6::nat)"
  by simp
(* Failed to apply initial proof method *)

simp、auto，甚至arith都找不到解决办法。但是，如果我们加上numeral_nat或者numeral.simps，simp就可以解决：

lemma "factorial (3::nat) = (6::nat)"
  by (simp add: numeral_nat)

lemma "factorial (3::nat) = (6::nat)"
  by (simp add: numeral.simps)

有趣的是，在这两个证明中，Isabelle 都给出了警告“Ignoring duplicate rewrite rule”，这意味着它应该已经知道这些了。此外，Isabelle 可以毫无问题地证明 "3*2*1 = 6"，这让我更加困惑这些引理是如何被使用的。

所以，如果这是一个如此简单且易于计算的等式 - 以至于 Isabelle 可以使用 value 命令计算它 - 这些规则显然是已经存在，为什么 Isabelle 不能在没有它们的情况下解决引理？

Answer 1

numeral_nat 包含 7 个引理：

thm numeral_nat
(*
  Numeral1 = Suc 0
  numeral (num.Bit0 ?n) = Suc (numeral (Num.BitM ?n))
  numeral (num.Bit1 ?n) = Suc (numeral (num.Bit0 ?n))
  Num.BitM num.One = num.One
  Num.BitM (num.Bit0 ?n) = num.Bit1 (Num.BitM ?n)
  Num.BitM (num.Bit1 ?n) = num.Bit1 (num.Bit0 ?n)
  1 = Suc 0
*)

而 simp 抱怨其中的 4 个：

Ignoring duplicate rewrite rule:
Num.BitM num.One ≡ num.One 
Ignoring duplicate rewrite rule:
Num.BitM (num.Bit0 ?n1) ≡ num.Bit1 (Num.BitM ?n1) 
Ignoring duplicate rewrite rule:
Num.BitM (num.Bit1 ?n1) ≡ num.Bit1 (num.Bit0 ?n1) 
Ignoring duplicate rewrite rule:
1 ≡ Suc 0

因此，有7-4=3个新定理。跟踪（参见 simp_trace）显示 numeral_nat(2,3) 是有用的引理。

惯用的方式是（numeral_eq_Suc 通常是一个糟糕的 simp 规则）：

lemma "factorial (3::nat) = (6::nat)"
  by (simp add: numeral_eq_Suc)

您可能想知道为什么实际上需要从 3 扩展到 Suc (Suc (Suc 0)))，因为定义是 factorial (Suc n) = ...。伊莎贝尔的回答是：只针对1。这对于大多数递归函数来说已经足够了，并且避免了目标的爆炸。尝试

lemma "factorial (6::nat) = A" 
  apply (simp add: numeral_nat(2,3))

看到放大的球门。

现在 value 的工作方式大不相同。它具有三种模式：

value 或 value [code]（eval 策略）生成标准 ML 代码并执行它。您信任代码方程和编译器。
value [nbe]（normalization 策略）是通过评估进行归一化（也使用代码生成）。 “可信任的代码栈相当可观”(https://isabelle.in.tum.de/dist/Isabelle2021/doc/codegen.pdf)
value [simp]（code_simp 策略）使用简化器。完全值得信赖。

即使在最后一种情况下，简化器也是使用特定参数和定理调用的，而不是像您那样使用默认参数和定理。因此差异。

为什么在 Isabelle 中证明自然数的简单可计算相等性时必须使用 "numeral_nat" 或 "numeral.simps"

Why do I have to use "numeral_nat" or "numeral.simps" when proving a simple computable equality of naturals in Isabelle

isabelle