RFC: Nested inductives: rewrite the recursor, too

[nomeata]

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?

[nomeata]

Ha, with addDeclWithoutChecking I can easily experiment with this, very nice.

At least if the functions are defined via .rec we get the desired definitional equality`

-- Let’s replace `Tree.rec_1` with a term defined via `List.rec`:

run_meta do
  let decl ← getConstInfoDefn ``Tree.rec_1_impl
  let decl := { decl with name := ``Tree.rec_1}
  let env ← getEnv
  let .ok env' := env.addDeclWithoutChecking (.defnDecl decl) | throwError "addDeclWithoutChecking failed"
  modifyEnv (fun _ => env')

-- A variant of List.map defined directly with the recursor
noncomputable
def List.map' (f : α → β) : List α → List β :=
  List.rec [] (fun x xs xs_ih => (f x) :: xs_ih)

noncomputable
def Tree.id : Tree → Tree :=
  Tree.rec (fun ts ts_ih => .node ts_ih) [] (fun _x _xs x_ih xs_ih => x_ih :: xs_ih)

theorem Tree.id_eq_1 : 
  Tree.id (.node ts) = .node (List.map' Tree.id ts) := rfl

With the existing .below/.brecOn construction, this does not work right away:

-- Now using brecOn

mutual
def Tree.id2 : Tree → Tree
  | .node ts => .node (Tree.id2_aux ts)
def Tree.id2_aux : List Tree → List Tree
  | [] => []
  | x::xs => Tree.id2 x :: Tree.id2_aux xs
end

theorem Tree.id2_aux_eq : Tree.id2_aux = List.map Tree.id2 := by
  funext ts
  induction ts
  next => rfl
  next t ts ts_ih => rw [id2_aux, List.map, ts_ih]

/--
error: type mismatch
  rfl
has type
  id2_aux = id2_aux : Prop
but is expected to have type
  id2_aux = List.map id2 : Prop
-/
#guard_msgs in
theorem Tree.id2_aux_deq : Tree.id2_aux = List.map Tree.id2 := rfl

And it seems to me that while I can express Tree.rec_1 in terms of List.rec, I don't yet see how to similarly express Tree.below_1 in terms of List.below. So maybe we only get nested primitive recusion this way? Or maybe there is a generalization of the course-of-value construction that admits such nested recursion?