RFC: Nested inductives: rewrite the recursor, too

I have been tossing ideas around on how to work towards nested structural recursion, and this idea may reach the bar for worth-noting-as-an-RFC.

Summary

The kernel’s approach to compiling nested inductive (e.g. Tree nested under List) is

• Create a non-nested mutual inductive, by copying the structure of the inductive that we nest under (List), creating an auxillary inductive (ListTree).
• In the types and reduction rules of the generated recursors, replace the type former and constructors of the auxillary inductive with the ones expected by the user.

This way they get their Tree type with the expected types in the constructor and recursors, but they do get an extra recursor Tree.rec_1 (stemming from ListTree.rec), and it’s all disconnected from List.rec.

So I wonder: Can’t we also rewrite ListTree.rec with (a suitable instantiation of) List.rec in the rules for Tree.rec, and hopefully gain extra definitional equalities?

To rewrite the auxillary recursor, define a helper definition with the same type as the auxillary recursor, but implemented using the recursor of the nested-under inductive:

• pass the motives corresponding to the desired type through to its recursor
• pass through the F-args, but for x_ih parameter that isn't provided by the desired recursor, instantiated that with the that type’s .rec and full set of motives/F-args.

(This paragraph isn’t really helpful, I know, the example below is maybe better, and at some point this needs to be specified precisely).

Example with some code

import Lean.Elab.Command

inductive Tree where | node : List Tree → Tree

open Lean Meta

set_option pp.explicit true
set_option pp.funBinderTypes true

-- This the generated rule's RHS.
-- The type and constructors of the auxillary `ListTree` have been replaced
-- by their `List Tree` counterpats, but we still see `Tree.rec_1`.
-- Can we replace that with `List.rec`?

/--
info: fun
    (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 (@List.nil Tree))
    (cons : (head : Tree) → (tail : List Tree) → motive_1 head → motive_2 tail → motive_2 (@List.cons Tree head tail))
    (a : List Tree) =>
  node a (@Tree.rec_1 motive_1 motive_2 node nil cons a)
-/
#guard_msgs(whitespace:=lax) in
run_meta do
  let recVal ← getConstInfoRec ``Tree.rec
  logInfo recVal.rules[0]!.rhs

-- Here is a definition with the same type as `Tree.rec_1`, but referring to `List.rec` instead.

noncomputable
def Tree.rec_1_impl
    {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 (@List.nil Tree))
    (cons : (head : Tree) → (tail : List Tree) → motive_1 head → motive_2 tail → motive_2 (@List.cons Tree head tail))
    (ts : List Tree) :=
  @List.rec Tree motive_2 nil (fun (head : Tree) (tail : List Tree) ih_tail => cons head tail (@Tree.rec motive_1 motive_2 node nil cons head) ih_tail) ts


-- With this, I could imagine the following rule RHS'

noncomputable
def proposedRuleRHS
    (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 (@List.nil Tree))
    (cons : (head : Tree) → (tail : List Tree) → motive_1 head → motive_2 tail → motive_2 (@List.cons Tree head tail))
    (a : List Tree) :=
    node a (@Tree.rec_1_impl motive_1 motive_2 node nil cons a)

Is this sound?

Most crucial is of course the question of whether this is sound, a question which I cannot answer easily. (Intuitively it ought to be.)

In the example above the replacement recursor is at least provabily equal:

theorem Tree.rec_1_eq_rec1_impl : @Tree.rec_1 = @Tree.rec_1_impl := by
  funext motive_1 motive_2 node nil cons ts
  induction ts
  next => rfl
  next t ts ih => simp [ih, Tree.rec_1_impl]

so that is reason for optimism that this will hold for more complicated types.

(Actually, it seems that any parametric definition with the same type as @Tree.rec_1 is going to be equal to it, for a suitable definition of parametric.)

But that theorem like isn’t sufficient, as there are metatheoretic properties to worry about.

Happy to hear expert advise here, either about how to argue that it is, or show why it isn’t.

Does this help?

The hope is that with this we can construct

def Tree.size : Tree → Nat | node ts => ts.foldl (. + .size) 0

in a way that this this equation holds definitionally.

I did not work it through yet if that’s actually true, given our course-of-value recursion strategy.

Also the interaction with smart unfolding is unclear. Can there be useful a smart unfolding for a function like this?

Start with the Tree/List example and the generated recursor output obtained through getConstInfoRec, then inspect how nested inductive recursors are constructed. Done requires a precise soundness argument or counterexample for rewriting the auxiliary recursor, including whether the proposed definitional equalities and smart unfolding behavior hold.