작은 감사 도구를 만들고 있고, 툴체인은 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
둘 다 거부돼요. 메시지는 항이 기대한 값으로 reduce되지 않는다고 해요. 기본 인자랑 Inhabited 인스턴스가 원인인가 싶었어요. acc를 명시적으로 쓰고 인스턴스도 추가해 봤지만 달라진 게 없었어요.
native_decide는 둘 다 받아주는데, #print axioms를 하면 Lean.ofReduceBool이 나와서 그건 받아들일 수 없어요.
질문이 두 가지예요:
- 왜 컴파일된 코드는 이걸 평가할 수 있는데 kernel과
decide는 못 하나요?
- 함수를 다시 쓰지 않고, 예를 들어 fuel을 쓰는 것 말고, 이 함수에 대해 kernel이 검증한 사실을 얻을 방법이 있나요?
영어에서 번역·원문 보기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?
