making sInf computable

Stream: new members

[ooovi]

I want to talk about and find the smallest element of a Set Nat. I think i'd want to use Nat.instInfSet, which is noncomputable. However, I can constructively prove that my set is not empty, and looking at the definition of sInf on Nat, that should be enough to allow computing my element. Is there a way to use sInf (and all the nice theorems about it), but getting rid of the noncomputable? Do I try to prove that it's equal to some computable thing and rewrite whenever I need to? That seems kind of odd somehow?
A silly example:

-- a nice nonempty set
instance dec : Decidable (∃ n, n ∈ {m | 1 < m + 1}) := isTrue ⟨1, by simp⟩

-- using sInf to find the smallest element:
-- this gives complaints:
-- failed to compile definition, consider marking it as 'noncomputable'
-- because it depends on 'Nat.instInfSet', and it does not have executable code
example : ℕ := by
  let N := sInf {m | 1 < m + 1}
  match N with
  | 0 => exact 0
  | n + 1 => exact 1

-- finding the smallest element manually like sInf works fine
example : ℕ := by
  let N := if h : ∃ (n : ℕ), n ∈ {m | 1 < m + 1} then Nat.find h else 0
  match N with
  | 0 => exact 0
  | n + 1 => exact 1

I'm just asking to understand better. I don't actually need it to compute currently, but I know the moment will come.

[Ruben Van de Velde]

Do you want to try with docs#Nat.find ?