Deterministic Timeout on simple Recursion

Stream: new members

[Ayush Agrawal]

import tactic data.nat.parity
import tactic.induction


def lg : ℕ → ℕ
| 0 := 0
| (x + 1) :=
  have (x + 1) / 2 < (x + 1), from nat.div_lt_self' x 0,
    1 + lg ((x + 1)/2)
#reduce lg 2 --(deterministic) timeout

What is the reason of the above issue?

[Alex J. Best]

What output are you hoping for, does #eval lg 2 work for your purposes? Reduce may be unfolding a lot of things

[Yaël Dillies]

Isn't that because #reduce doesn't work on well-founded recursion anymore?

[Ayush Agrawal]

@Alex J. Best and @Yaël Dillies thanks, this works with #eval. Any reason why #reduce does not work?

[Yaël Dillies]

I think that's for precisely the reason I stated. About a year ago, something was changed in core Lean which involved a regression of #reduce. It now gets stuck on applications of acc, which are used in well-founded recursion. Note that your recursion is not "simple" precisely because it is well-founded :smile:

[Eric Rodriguez]

#reduce also uses the (trusted) kernel = slow, while #eval uses the (untrusted) VM = fast