Cannot Derive a Computable Eliminator

Stream: lean4

[haoyi zeng]

Hi, I tried to prove in Lean 4 that for any decidable predicate p over natural number,
we have

$$(\exists x.~ p\,x) \;\to\; \Sigma n.~ p\, n$$

by defining a linear-search-style higher-order inductive predicate.
In principle, such a relation can be established via the following approach:

import Std

open Nat

section TestLogic

  variable (p: Nat → Prop)

  inductive SearchPath : Nat → Prop where
    | Step (n: Nat) : (¬ p n → SearchPath (succ n)) → SearchPath n
  open SearchPath

  def liftP n :
    p n → SearchPath p n :=
      λ pn => Step n (λ npn => False.elim (npn pn))

  def stepBack n :
    SearchPath p (succ n) → SearchPath p n :=
      λ Tsn => Step n (λ _ => Tsn)

  def reduceToZero n :
    SearchPath p n → SearchPath p 0 := λ Tn => match n with
      | 0 => Tn
      | succ m => reduceToZero m (stepBack p m Tn)

  def liftPToZero n :
    p n → SearchPath p 0 := λ pn => reduceToZero _ _ (liftP _ _ pn)

  def liftExists :
    (∃ n, p n) → SearchPath p 0 := λ ep => match ep with | ⟨m, pm⟩ => liftPToZero p m pm

  noncomputable def extractWitness [H: DecidablePred p] (n: Nat): (T: SearchPath p n) -> Σ' n, p n
    := λ T => SearchPath.rec (λ m _ IH => if h: p m then ⟨m, h⟩ else IH h) T
    -- | Step _ φ => if h: p n then ⟨n, h⟩ else extractWitness (succ n) (φ h)
    -- := by admit

end TestLogic

However, it seems that Lean is unable to generate a computable eliminator for SearchPath in this setting.
Has this triggered some feature/limitation that prevents it from working?
In the end, I had to define it as noncomputable, but for concrete examples it always reduces successfully.

[Aaron Liu]

You can definitely make this computable

[Aaron Liu]

It's just that the compiler doesn't support raw recursors

[Aaron Liu]

Your SearchPath looks similar to docs#Acc, for which there is a module in Batteries that makes the recursors computable

[Ruben Van de Velde]

Maybe you can use docs#Nat.find