Noncomputable local functions

Stream: new members

[Sébastien Boisgérault]

Hi everyone,

Is it possible to declare a local (recursively defined) function as noncomputable?

My use case would be something like:

example (p : ℕ → Prop): (∀ n, ∃ m ≥ n, p m) -> ∃ ns : ℕ → ℕ, StrictMono ns ∧ ∀ i, p (ns i) := by
  intro h
  let rec ns (i : ℕ) : ℕ :=
    match i with
    | 0 => Classical.choose (h 0)
    | i + 1 => Classical.choose (h (ns i))
  admit -- TODO

If it's not possible (?) what would be your suggested refactoring/workaround?

Best regards,

Sébastien

[Mirek Olšák]

Do you need the outer function to be computable? If not, you can mark the full example as noncomputable.

[Mirek Olšák]

Hm, it works with noncomputable def but I see the problem. If you want to use the preferred keyword theorem, then local definitions fail on computability, while you cannot mark theorem as noncomputable. Looks like a bug to me...

[Mirek Olšák]

There is also this way of making a truly noncomputable theorem

noncomputable section in
theorem my_thm (p : ℕ → Prop) : (∀ n, ∃ m ≥ n, p m) -> ∃ ns : ℕ → ℕ, StrictMono ns ∧ ∀ i, p (ns i) := by
  intro h
  let rec ns (i : ℕ) : ℕ :=
    match i with
    | 0 => Classical.choose (h 0)
    | i + 1 => Classical.choose (h (ns i))
  admit -- TODO

[Alfredo Moreira-Rosa]

Theorems are noncomputable.

[Mirek Olšák]

But the auxiliary definitions inside aren't (which is the topic of this thread).

[Robin Arnez]

This is lean4#7878, right?

[Aaron Liu]

I would do let ns : Nat → Nat := Nat.rec (Classical.choose (h 0)) (fun n ih => Classical.choose (h ih))

[Aaron Liu]

then you can do stuff with the contents too

[Sébastien Boisgérault]

Mirek Olšák said:

But the auxiliary definitions inside aren't (which is the topic of this thread).

Yes, thanks a lot for the feedback. So theorems (or examples) are noncomputable, but you can still declare them as noncomputable and it's stronger somehow, since their auxiliary definitions become noncomputable. Ah, that's a bit tricky!

[Sébastien Boisgérault]

Aaron Liu said:

I would do let ns : Nat → Nat := Nat.rec (Classical.choose (h 0)) (fun n ih => Classical.choose (h ih))

Beginner question sorry, but ... why does it work? A special property of recursors? A more general principle (such as having a non-computable function returned by a function instead of declared?)?

[Robin Arnez]

That works because it does not declare a new declaration

[Robin Arnez]

Only let rec declares a declaration, regular lets have no problem

[Sébastien Boisgérault]

Robin Arnez said:

This is lean4#7878, right?

Yes, thanks for the link! :pray:

[Mirek Olšák]

And by the way, if you apply choice before defining your recursive function, you don't run into this issue.

theorem my_thm (p : ℕ → Prop) : (∀ n, ∃ m ≥ n, p m) -> ∃ ns : ℕ → ℕ, StrictMono ns ∧ ∀ i, p (ns i) := by
  intro h
  choose ns nsh using h
  let rec nsr (i : ℕ) : ℕ :=
    match i with
    | 0 => ns 0
    | i + 1 => ns (nsr i)
  let n := ns 5
  sorry -- TODO

To understand what is going on, you can

#print my_thm

You will see that Lean automatically defined my_thm.nsr which takes ns as an argument. So it is equivalent as if you write

def my_thm.nsr (ns : ℕ → ℕ) ...

theorem my_thm ...

Here the definition of my_thm.nsr is computable because its input is a function. When you did it before, it was equivalent to

def my_thm.nsr (h : ∀ n, ∃ m ...) := ... choice ...

theorem my_thm ...

Lean didn't see prefix noncomputable before the first def, and threw an error. The solution with noncomputable section in is then equivalent to

noncomputable section

def my_thm.nsr (h : ∀ n, ∃ m ...) := ... choice ...

theorem my_thm ...

end

[Mirek Olšák]

In this case, I would recommend using the choose tactic. In my experience, it is much more convenient to use over Classical.choose. But I can easily imagine other noncomputable functions you could need in local definitions.