Cannot show termination of non-recursive function

Stream: lean4

[David Hamelin]

Hello,

I am trying to prove that in the following code, test_continuation terminates:

inductive Continuation : Type where
| done (a : Nat)
| step (f: Unit → Continuation)
open Continuation

instance : Inhabited Continuation where
  default := done 0

def to_string : Continuation → String
| done a => s!"Done: {a}"
| step _ => s!"Not done"

partial def test_continuation : Nat → Continuation
| 2 => step (fun () => test_continuation 2)
| x => done x

#eval to_string (test_continuation 2)

I know that test_continuation terminates (eval returns immediately), because there is no recursive call : it returns a function wrapped in a Continuation type.

However, when I remove the partial keyword, Lean 4 shows the following error:

fail to show termination for
  test_continuation
with errors
argument #1 was not used for structural recursion
  failed to eliminate recursive application
    test_continuation 2

structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relation

I tried to use decreasing_by as shown in "Theorem Proving in Lean 4", but it generates a goal I cannot prove:

def test_continuation : Nat → Continuation
| 2 => step (fun () => test_continuation 2)
| x => done x
decreasing_by
  simp_wf
 -- Goal is 2 < a✝, with no hypothesis
  sorry

Could this be proved ?

Thanks in advance

[Sky Wilshaw]

Lean's termination checker isn't really about termination of the executed program, it's termination of the definition. Because test_continuation 2 references test_continuation 2 (even though it's not executed immediately), the termination check fails.

[Sky Wilshaw]

In lean's kernel, there's no concept of "executing" a program, there's just type theory. To build recursive functions at a low level, we use recursors generated from inductive data types, which require this kind of "decreasing" check.

[Kyle Miller]

My understanding is similar to what Sky is referring to. If you start reducing the expression rather than evaluating it, you'd get step (fun () => step (fun () => step (fun () => step (fun () => ...)))), and so on. So in that sense it fails to terminate.

[Kyle Miller]

But also, if you could prove termination, you'd get a contradiction:

inductive Continuation : Type where
| done (a : Nat)
| step (f: Unit → Continuation)
open Continuation

theorem uhoh (x : Continuation) (hx : x = step (fun () => x)) : False := by
  induction x with
  | done _ => cases hx
  | step f ih =>
    simp at hx
    exact ih () (congrFun hx ())

axiom test_continuation : Nat → Continuation
axiom test_continuation.eq_1 : test_continuation 2 = step (fun () => test_continuation 2)
axiom test_continuation.eq_2 (x : Nat) (h : x ≠ 2) : test_continuation x = done x

example : False := uhoh (test_continuation 2) test_continuation.eq_1

[David Hamelin]

I see, thank you very much
I should read more about Lean's kernel to not get into another pitfall

[Sebastian Ullrich]

This would be a fine corecursive function, but Lean does not support that

[Sky Wilshaw]

David Hamelin said:

I should read more about Lean's kernel to not get into another pitfall

Feel free to keep asking questions about it too!