Wellfounded recursion

Stream: lean4

[Valentin Robert]

What is the recommended way of doing wellfounded recursion in Lean4?

I have been trying to use WellFounded.fix with a proper well-founded relationship, and it all type-checks, but I run into the following message:

failed to compile definition, consider marking it as 'noncomputable' because it depends on 'WellFounded.fix', and it does not have executable code

It turns out that you get this message even with the simplest possible such code:

def dumbNatRec : Nat → Nat :=
  WellFounded.fix Nat.ltWf (λ x f => x)

I have noticed that the WellFounded module uses set_option codegen false which makes the error go away, but I'm not sure I understand the consequences of this option. It seems like this code is fully defined and ought to be runnable/compilable.

Am I using the wrong tool? Am I using the tool wrong?
Thanks for you help!

[David Renshaw]

I too am curious to understand this more.

It seems that mathlib4 uses unsafe as a workaround: https://github.com/leanprover-community/mathlib4/blob/7ac569847b94980d3d668ae6079131f5cd2fe559/Mathlib/Logic/Basic.lean#L50-L55

[Brandon Brown]

My understanding is WF recursion is not implemented in the compiler yet, so it will type check but won’t compute. Just need to wait for it to be fully implemented. See https://github.com/leanprover/lean4/issues/176

[Chris B]

In the meantime if you just want to be able to write recursive functions, you can use the partial prefix.

[Mario Carneiro]

If you want to write a function by well founded recursion that computes and also has provable properties, use WellFounded.fix' (linked above). That's what it's there for. (You might argue that the implementedBy is a cheat, but keep in mind that this is exactly what the compiler will do once leanprover/lean4#176 is addressed.)