Is it possible to implement infinite loop in lean?

Stream: new members

[Rui Liu]

Is it possible to define such a function: def find_first_true: (N -> bool) -> N, which will find the first value of natural number that's true for a function?

[Yakov Pechersky]

docs#nat.find might be related

[Mario Carneiro]

This is nat.find, but note the precondition: it needs to be not always false!

[Rui Liu]

Is it possible that this call runs forever?

[Mario Carneiro]

all lean programs terminate

[Mario Carneiro]

halting problem solved :)

[Rui Liu]

so in lean, it's not possible to have infinite loop? lean cannot be used as general programming language?

[Kevin Buzzard]

you can write meta code and then it's just like Haskell

[Kevin Buzzard]

but if it's not meta, the kernel checks that it terminates

[Mario Carneiro]

there are caveats, of course. But for non-meta functions it would break the logic (make it inconsistent) to have nonterminating functions

[Rui Liu]

OK...

[Mario Carneiro]

consider that if you could write find_first_true in lean, you should be able to refine it to the signature \all f : N -> bool, {n | f n = tt}, and this is plainly false

[Mario Carneiro]

however if you don't care about computation or garbage values and just want a function with that signature, you can write

noncomputable def nat.maybe_find (f : ℕ → bool) : ℕ :=
by classical; exact
if h : ∃ n, f n = tt then nat.find h else 37