Computable WellFounded.fix

Stream: lean4

[Joe Hendrix]

I was looking into manually translating a mutually recursive function into a single non-recursive function and saw the elaborator uses WellFounded.fix even though it is noncomputable.

That got me thinking is there a computable version of WellFounded.fix in Lean?

I didn't see one, buit was able to write a version that uses WellFoundedRelation:

def WellFoundedRelation.fix {α : Sort u} [inst : WellFoundedRelation α] {motive : α → Sort v}
  (ind : ∀x, (∀y, WellFoundedRelation.rel y x → motive y) → motive x)
  (x : α) : motive x :=
  ind x (fun y _ => WellFoundedRelation.fix ind y)
termination_by x

This feels like I may be reinventing something that already exists or there's a performance pitfall. Is there an alternative computable fixpoint definition I should look into?

[Aaron Liu]

I think Batteries has compiled a computable version

[Aaron Liu]

here

[Eric Wieser]

And it's csimp, so importing that file is enough to make WellFounded.fix computable

[Matt Diamond]

might be useful to add a note about Batteries.WF to the WellFounded.fix documentation

[Joe Hendrix]

It also seems like this would be a reasonable candidate to migrate from batteries to core.

[Joe Hendrix]

I made this PR for this.