Why Nat.find is computable, when Wellfounded.fix isn't?

Stream: mathlib4

[Paradoxy]

I cannot understand this piece of code

protected def findX : { n // p n ∧ ∀ m < n, ¬p m } :=
  @WellFounded.fix _ (fun k => (∀ n < k, ¬p n) → { n // p n ∧ ∀ m < n, ¬p m }) lbp (wf_lbp H)
    (fun m IH al =>
      if pm : p m then ⟨m, pm, al⟩
      else
        have : ∀ n ≤ m, ¬p n := fun n h =>
          Or.elim (Nat.lt_or_eq_of_le h) (al n) fun e => by rw [e]; exact pm
        IH _ ⟨rfl, this⟩ fun n h => this n <| Nat.le_of_succ_le_succ h)
    0 fun _ h => absurd h (Nat.not_lt_zero _)

From import Mathlib.Data.Nat.Find.

While WellFounded.fix is noncomputable, somehow findX is accepted as computable? Why?

[Aaron Liu]

If you import batteries then it becomes computable

[Aaron Liu]

probably there's a better way to write the findX without explicitly referencing Wellfounded.fix

[Paradoxy]

Aaron Liu said:

If you import batteries then it becomes computable

Sorry, I don't follow. Let me make my example even more mininal, please explain the behaviour we observe:

def e1 (p : Type* → Prop) (ep : ∃ a, p a) := ep.choose
def e2 (p : Type → Prop) (ep : ∃ a, p a) := ep.choose
noncomputable def e3 (p : Nat → Prop) (ep : ∃ a, p a) := ep.choose -- Why do I have to make it noncomputable?!
noncomputable def e4 (t : Type)(p : t → Prop) (ep : ∃ a, p a) := ep.choose -- Why do I have to make it noncomputable?!
noncomputable def e5 (t : Type*)(p : t → Prop) (ep : ∃ a, p a) := ep.choose -- Why do I have to make it noncomputable?!

Surely I shouldn't import batteries for this, no? I expect everything here to be noncomputable. yet e1 and e2 are computable just fine, despite the fact that I am literally using Classical.choose, a noncomputable function.

[Aaron Liu]

not sure if this is good

/-- Find the smallest `n` satisfying `p n`. Returns a subtype. -/
protected def findX : { n // p n ∧ ∀ m < n, ¬p m } :=
  go H 0 fun _ h => absurd h (Nat.not_lt_zero _)
where
  go (H : ∃ n, p n) (k : Nat) (hk : ∀ n < k, ¬p n) : { n // p n ∧ ∀ m < n, ¬p m } :=
    if pk : p k then ⟨k, pk, hk⟩
    else
      have : ∀ n ≤ k, ¬p n := fun n h =>
        Or.elim (Nat.lt_or_eq_of_le h) (hk n) fun e => by rw [e]; exact pk
      go H (k + 1) fun n h => this n <| Nat.le_of_succ_le_succ h
  termination_by (wf_lbp H).wrap k
  decreasing_by exact ⟨rfl, this⟩

[Aaron Liu]

Paradoxy said:

Aaron Liu said:

If you import batteries then it becomes computable

Sorry, I don't follow. Let me make my example even more mininal, please explain the behaviour we observe:

def e1 (p : Type* → Prop) (ep : ∃ a, p a) := ep.choose
def e2 (p : Type → Prop) (ep : ∃ a, p a) := ep.choose
noncomputable def e3 (p : Nat → Prop) (ep : ∃ a, p a) := ep.choose -- Why do I have to make it noncomputable?!
noncomputable def e4 (t : Type)(p : t → Prop) (ep : ∃ a, p a) := ep.choose -- Why do I have to make it noncomputable?!
noncomputable def e5 (t : Type*)(p : t → Prop) (ep : ∃ a, p a) := ep.choose -- Why do I have to make it noncomputable?!

Surely I shouldn't import batteries for this, no? I expect everything here to be noncomputable. yet e1 and e2 are computable just fine, despite the fact that I am literally using Classical.choose, a noncomputable function.

no batteries specifically does WellFounded.fix along with some other functions (Acc.ndrec, Acc.ndrecOn, WellFounded.fixF, WellFounded.fix) in Batteries/WF by writing @[csimp] lemmas for them

[Paradoxy]

Aaron Liu said:

not sure if this is good

/-- Find the smallest `n` satisfying `p n`. Returns a subtype. -/
protected def findX : { n // p n ∧ ∀ m < n, ¬p m } :=
  go H 0 fun _ h => absurd h (Nat.not_lt_zero _)
where
  go (H : ∃ n, p n) (k : Nat) (hk : ∀ n < k, ¬p n) : { n // p n ∧ ∀ m < n, ¬p m } :=
    if pk : p k then ⟨k, pk, hk⟩
    else
      have : ∀ n ≤ k, ¬p n := fun n h =>
        Or.elim (Nat.lt_or_eq_of_le h) (hk n) fun e => by rw [e]; exact pk
      go H (k + 1) fun n h => this n <| Nat.le_of_succ_le_succ h
  termination_by (wf_lbp H).wrap k
  decreasing_by exact ⟨rfl, this⟩

Thanks, this is educational. But can you also tell me why exactly e1 and e2 are computable?

[Aaron Liu]

oh that's because types are erased at runtime

[Aaron Liu]

so there's no data there

[Paradoxy]

Aaron Liu said:

so there's no data there

Can you please tell me where can I learn more about this? To my untrained eyes, if e1 and e2 are computable, then so must be e4 and e5.

[Aaron Liu]

it's the same reason you don't have to mark your proofs as noncomputable

[Aaron Liu]

there's nothing to compute

[Aaron Liu]

but for e3 you compute a Nat and for e4 you compute a t

[Paradoxy]

Aaron Liu said:

there's nothing to compute

What are we computing in e4 and e5 exactly that makes things noncomputable, that we don't compute in e1 and e2, making them computable? Sorry if I sound too stupid

[Aaron Liu]

we are computing the term of type t

[Aaron Liu]

for example, I could specialize t := Nat

[Paradoxy]

Aaron Liu said:

for example, I could specialize t := Nat

Thank you very much, I understand it now