Can we make noncomputable functions computable?

Stream: Is there code for X?

[Kenny Lau]

I suddenly had this idea to do a trick to make noncomputable functions kind of computable by providing an instance of Decidable (f a = b), but unfortunately it didn't give me the results I wanted. Would this work at all? I mean I guess there are tactics like norm_num which kind of acts like a custom decision procedure, so I'm just trying out some basic ideas here.

import Mathlib

class DecidableFun {α β : Sort*} (f : α → β) where
  dec : ∀ a b, Decidable (f a = b)

noncomputable def id' (n : ℕ) : ℕ :=
  Classical.choose (⟨n, rfl⟩ : ∃ n', n' = n)

theorem id'_eq (n : ℕ) : id' n = n :=
  Classical.choose_spec (⟨n, rfl⟩ : ∃ n', n' = n)

instance : DecidableFun id' where
  dec m n := by rw [id'_eq]; infer_instance

attribute [instance] DecidableFun.dec

#check (by decide : id' 2 = 2) -- failed

[Andrew Yang]

One (but might not be all) issue is that you are using rewriting in data (in your implementation of DecidableFun). You need to use decidable_of_iff instead.

[Andrew Yang]

You also need to attribute [instance high] DecidableFun.dec to override the default decidable eq instance on nat. But then it will work.

[Yakov Pechersky]

Andrew's suggestions in code:

import Mathlib

class DecidableFun {α β : Sort*} (f : α → β) where
  dec : ∀ a b, Decidable (f a = b)

noncomputable def id' (n : ℕ) : ℕ :=
  Classical.choose (⟨n, rfl⟩ : ∃ n', n' = n)

theorem id'_eq (n : ℕ) : id' n = n :=
  Classical.choose_spec (⟨n, rfl⟩ : ∃ n', n' = n)

instance : DecidableFun id' where
  dec a b := decidable_of_iff (a = b) <| by
    simp [id']

attribute [instance high] DecidableFun.dec

#check (by decide : id' 2 = 2) -- works

[Jz Pan]

Note that ∀ a b, Decidable (f a = b) does not make the function f computable; it only makes that one can check whether f a = b for any given b. It is true only if there is a computable surjection ℕ -> β (in which case the computable version of f is implemented by Nat.find).

[Kenny Lau]

@Andrew Yang thanks for the suggestions and @Yakov Pechersky thanks for the fix. what would be some drawbacks of this new thing?

@Jz Pan indeed, but when we use decide we usually use it for propositions right? we would have to also prove things like, if f is "semi-computable" and g is "semi-computable", then f o g is also "semi-computable"

[Kyle Miller]

(This reminds me of some experiments I tried to make in this direction a few years ago: #general > computable class @ 💬. I got it to sort of work, but it took some modification to Lean 3's noncomputability checker. I think there's something to it, but I think it needs some metaprogramming to really the carry the idea out!)