我有个小的审计工具，toolchain 是 leanprover/lean4:v4.15.0。步数计数器是个 partial def，因为没人有终止性证明。
partial def collatzSteps (n : Nat) (acc : Nat := 0) : Nat :=
if n ≤ 1 then acc
else if n % 2 == 0 then collatzSteps (n / 2) (acc + 1)
else collatzSteps (3 * n + 1) (acc + 1)
def withinBudget (n : Nat) : Bool :=
decide (collatzSteps n ≤ budget)
lake build 没有问题，#eval Audit.collatzSteps 27 得到 111。但在另一个单独的文件里是这样。
example : collatzSteps 6 = 8 := by rfl
theorem w27 : withinBudget 27 = true := by decide
两个都被拒绝了。报错说该项无法归约到预期的值。我怀疑过是默认参数和 Inhabited 实例的问题。显式写出 acc 并加上实例都没有任何变化。
native_decide 两个都能通过，但这时 #print axioms 会显示 Lean.ofReduceBool，这个我不接受。
我有两个问题。
- 为什么编译后的代码能算出这个，而内核和
decide 不行？
- 除了重写（比如改成带 fuel 的版本）之外，有没有办法得到一个经内核检查的、关于这个函数的结论？
从英语翻译·查看原文I have a small audit tool, toolchain leanprover/lean4:v4.15.0. The step counter is a partial def, since nobody has a termination proof:
partial def collatzSteps (n : Nat) (acc : Nat := 0) : Nat :=
if n ≤ 1 then acc
else if n % 2 == 0 then collatzSteps (n / 2) (acc + 1)
else collatzSteps (3 * n + 1) (acc + 1)
def withinBudget (n : Nat) : Bool :=
decide (collatzSteps n ≤ budget)
lake build is clean and #eval Audit.collatzSteps 27 gives 111. But in a separate file:
example : collatzSteps 6 = 8 := by rfl
theorem w27 : withinBudget 27 = true := by decide
Both are rejected. The message says the term does not reduce to the expected value. I suspected the default argument and the Inhabited instance. Writing acc explicitly and adding an instance changed nothing.
native_decide accepts both, but #print axioms then shows Lean.ofReduceBool, which I do not accept.
Two questions:
- Why can the compiled code evaluate this while the kernel and
decide cannot?
- Is there any way to get a kernel-checked fact about this function, short of rewriting it, for instance with fuel?
