induction principle is not generated

Stream: general

[Asei Inoue]

def factorial (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | m + 1 => (m + 1) * factorial m

-- induction principle is generated!
#check factorial.induct

inductive Many (α : Type u) where
  | none : Many α
  | more : α → (Unit → Many α) → Many α

def many_map {α β : Type} (f : α → β) : Many α → Many β
  | .none => .none
  | .more x xs => Many.more (f x) (fun () => many_map f <| xs ())

-- why the induction principle of `many_map` is not generated?
/-
unknown identifier 'many_map.induct'
-/
#check many_map.induct

[Asei Inoue]

I thought that for every recursive function, an induction principle is generated. Is that not so?

[Joachim Breitner]

There are more errors when you click on that line, it seems the generation of the induction principle fails. That's a bug that's on me.

[Joachim Breitner]

If you don’t need many_map to be structurally recursive, you can work-around the issue by writing

def many_map {α β : Type} (f : α → β) : Many α → Many β
  | .none => .none
  | .more x xs => Many.more (f x) (fun () => many_map f <| xs ())
termination_by m => m```

[Joachim Breitner]

This uses different code paths in the induction principle generation that don’t hit the bug.

Reported at https://github.com/leanprover/lean4/issues/4320