Non-dependent recursor

Stream: lean4

[Florent Schaffhauser]

Using the dependent recursorNat.rec for Lean's natural numbers, one gets a definition of the non-dependent recursor as a special case:

#check Nat.rec  -- Nat.rec.{u} {motive : Nat → Sort u} (zero : motive Nat.zero) (succ : (n : Nat) → motive n → motive n.succ) (t : Nat) : motive t

def Nat.elim {X : Sort l} : X → (Nat → X → X) → Nat → X :=
  Nat.rec.{l} (motive := fun _ => X)

#check Nat.elim. -- Nat.elim.{l} {X : Sort l} : X → (Nat → X → X) → Nat → X

However, if I try to define the natural numbers myself, I can follow the same method and it seems to type check, but an error message appears that says code generator does not support recursor 'myNat.rec' yet.

inductive myNat
  | zero : myNat
  | succ : myNat → myNat

#check myNat.rec  -- myNat.rec.{u} {motive : myNat → Sort u} (zero : motive myNat.zero) (succ : (a : myNat) → motive a → motive a.succ) (t : myNat) : motive t

def myNat.elim {X : Sort l} : X → (myNat → X → X) → myNat → X :=
 -- code generator does not support recursor 'myNat.rec' yet, consider using 'match ... with' and/or structural recursion
  myNat.rec.{l} (motive := fun _ => X)

#check myNat.elim  -- myNat.elim.{l} {X : Sort l} : X → (myNat → X → X) → myNat → X

Is there a way to fix this so I do not get the error message? Or should I not expect myNat.rec to work like this?

[Marcus Rossel]

I believe this is expected, and the reason is stated exactly in the error message. You can fix this by writing elim as a recursive function over the myNat argument (using match).

[Junyan Xu]

Or import Mathlib and

suppress_compilation in
def myNat.elim {X : Sort l} : X → (myNat → X → X) → myNat → X :=

[François G. Dorais]

No need to import Mathlib, using noncomputable def is enough.

[Florent Schaffhauser]

Thank you all :blush: But why does this not happen with Natonly with myNat?

[Floris van Doorn]

I expect because of these lines in Lean/Init/Data/Nat/Basic.lean:

/-- Compiled version of `Nat.rec` so that we can define `Nat.recAux` to be defeq to `Nat.rec`.
This is working around the fact that the compiler does not currently support recursors. -/
private def recCompiled {motive : Nat → Sort u} (zero : motive zero) (succ : (n : Nat) → motive n → motive (Nat.succ n)) : (t : Nat) → motive t
  | .zero => zero
  | .succ n => succ n (recCompiled zero succ n)

@[csimp]
private theorem rec_eq_recCompiled : @Nat.rec = @Nat.recCompiled :=
  funext fun _ => funext fun _ => funext fun succ => funext fun t =>
    Nat.recOn t rfl (fun n ih => congrArg (succ n) ih)

[Floris van Doorn]

@[csimp] theorem foo : a = b means that the compiler will replace a by b everywhere, before actually compiling a definition.

[Kyle Miller]

(This isn't answering any questions here, but I'll mention that Mathlib has a compile_inductive% command for constructing an auxiliary definition using match and auto-proving the csimp lemma.)

[Florent Schaffhauser]

Oh, nice! Is the plan for this to eventually become part of the core commands?

[François G. Dorais]

It's more likely that the compiler will just support recursors.

[Florent Schaffhauser]

Right, that makes more sense. But I'm curious: does support recursors mean more than having a command that creates the auxiliary definition and proves the csimp lemma?

[Henrik Böving]

In general we do not have recursors because they can easily be used to generate bad code with unforseen performance characteristics. If you inspect e.g. Nat.rec you will see that the Nat.succ n case always expects the result of the computation for the n already. This means that you can never early abort a computation that's done with a recursor. So if you say, implement List.isEmtpy with a recursor you will always iterate through the entire list despite knowing it is indeed empty (or not) after the first step.

The way to fix this properly would be to have support in the code generator for a transformation that defers this recursive call(s) until they are actually required by the code that is using them. But that would be work for basically no result so that's why the state is like it currently is..

[Florent Schaffhauser]

Thanks for the explanation! :pray: