nested inductives in the kernel

Stream: lean4

[Joachim Breitner]

(This is mostly an inner monologue, I mostly answer my own questions as I go.)

---

I was, for some reason, under the impression that the Lean4 kernel has support for mutual inductives, but not nested inductive, and that the fronend elaborates nested inductives such as

inductive Tree where
 | node : List Tree → Tree

to mutual inductives such as

mutual
inductive Tree where
 | node : ListTree → Tree
inductive ListTree where
 | nil : ListTree
 | cons : Tree → ListTree → ListTree
end

so that the kernel sees the latter only.

But if I do the nested induction and look at the type of the recursor, I get

recursor Tree.rec.{u} : {motive_1 : Tree → Sort u} →
  {motive_2 : List Tree → Sort u} →
    ((a : List Tree) → motive_2 a → motive_1 (Tree.node a)) →
      motive_2 [] →
        ((head : Tree) → (tail : List Tree) → motive_1 head → motive_2 tail → motive_2 (head :: tail)) →
          (t : Tree) → motive_1 t

and it seems that this is is indeed “primitive” (it’s a recursor, not a def), and that thus the kernel somehow was able to make sense of List Tree without making an artificial copy of the LIst data type.

I tried to consult “The Type Theory of Lean”, but (maybe because that is about lean3?) it says that even mutual induction is not supported.

Looking at the kernel code I see

/* Eliminate nested inductive datatypes by creating a new (auxiliary) declaration which contains and inductive types in `d`
   and copies of the nested inductive datatypes used in `d`. For each nested occurrence `I Ds is` where `I` is a nested inductive
   datatype and `Ds` are the parametric arguments and `is` the indices, we create an auxiliary type `Iaux` in the (mutual) inductive
   declaration `d`, and replace `I Ds is` with `Iaux As is` where `As` are `d`'s parameters.
   Moreover, we add the pair `(I Ds, Iaux)` to `nested_aux`.

   Note that, `As` and `Ds` may have a different sizes. */
struct elim_nested_inductive_fn {

so maybe this means that there is this copying-construction, but it happens purely in the kernel, in a way that the recursor still looks “primitive” to the outside (as opposed to be derived from a primitive constructor that mentiones mentions the copy of List).

Ah, looking some more, it seems that within the kernel, the copied data constructors are used, but then the resulting .rec values and constructors are post-processed and in their types (and rules) the auxillary data types are written back to List Tree instead (using res.restore_nested), and thus outside the kernel these are never seen.

That answers my questions; maybe someone else finds this an interesting investigation.

[Jason Rute]

Does @Sebastian Ullrich‘s dissertation clarify this at all? My understanding was that his dissertation is the Lean 4 update to Mario’s “The Type Theory of Lean” (among other things).

[Henrik Böving]

The part right before 3.3 does explain that this encoding happens in the kernel yes.

[Joachim Breitner]

Ok, follow up thought.

It feels somehow “wrong” that although the Tree type above uses the List type former in the types, and the List constructors in recursor, it doesn’t connect to List.rec. Without hard evidence yet I am curious if, if it would, we might have an easier time defining structurally recursive nested functions.

More concretely, right now you get this reduction rule for the Tree.rec recursor:

inductive Tree where
 | node : List Tree → Tree


noncomputable def Tree.rec_1'.{u}
  {motive_1 : Tree → Sort u} {motive_2 : List Tree → Sort u}
  (node : (a : List Tree) → motive_2 a → motive_1 (Tree.node a)) (nil : motive_2 [])
  (cons : (head : Tree) → (tail : List Tree) → motive_1 head → motive_2 tail → motive_2 (head :: tail))
  (ts : List Tree) : motive_2 ts
    :=
    @List.rec Tree _ nil
      (fun head tail ih_tail => cons head tail (@Tree.rec motive_1 motive_2 node nil cons head) ih_tail)
      ts

theorem Tree.rec_1_eq_rec1'.{u}
  {motive_1 : Tree → Sort u} {motive_2 : List Tree → Sort u}
  (node : (a : List Tree) → motive_2 a → motive_1 (Tree.node a)) (nil : motive_2 [])
  (cons : (head : Tree) → (tail : List Tree) → motive_1 head → motive_2 tail → motive_2 (head :: tail))
  (ts : List Tree) :
    @Tree.rec_1 motive_1 motive_2 node nil cons ts = @Tree.rec_1' motive_1 motive_2 node nil cons ts := by
  induction ts
  next => rfl
  next x xs ih => dsimp; congr

theorem Tree.rec_rule'  {motive_1 : Tree → Sort u} {motive_2 : List Tree → Sort u}
  (node : (a : List Tree) → motive_2 a → motive_1 (Tree.node a)) (nil : motive_2 [])
  (cons : (head : Tree) → (tail : List Tree) → motive_1 head → motive_2 tail → motive_2 (head :: tail))
  (ts : List Tree) :
  @Tree.rec motive_1 motive_2 node nil cons (.node ts) =
  node ts (@Tree.rec_1' motive_1 motive_2 node nil cons ts) := by dsimp; rw [Tree.rec_1_eq_rec1']

(This on its won probably doesn’t suffice to be able to do nested recursion through, say, List.map.)