(Temporarily) guard against nested inductives in structural recursion

Co-authored-by: Tobias Grosser <tobias@grosser.es>

src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean

@@ -52,6 +52,8 @@ def getRecArgInfo (fnName : Name) (numFixed : Nat) (xs : Array Expr) (i : Nat) :
       throwError "its type {indInfo.name} does not have a recursor"
     else if indInfo.isReflexive && !(← hasConst (mkBInductionOnName indInfo.name)) && !(← isInductivePredicate indInfo.name) then
       throwError "its type {indInfo.name} is a reflexive inductive, but {mkBInductionOnName indInfo.name} does not exist and it is not an inductive predicate"
+    else if indInfo.isNested then
+      throwError "its type {indInfo.name} is a nested inductive, which is not yet supported"
     else
       let indArgs    : Array Expr := xType.getAppArgs
       let indParams  : Array Expr := indArgs[0:indInfo.numParams]

src/Lean/Meta/Constructions/BRecOn.lean

@@ -85,9 +85,8 @@ of type
 ```
 α → List α → Sort (max 1 u_1) → Sort (max 1 u_1)
 ```
-The parameter `typeFormers` are the `motive`s.
 -/
-private def buildBelowMinorPremise (rlvl : Level) (typeFormers : Array Expr) (minorType : Expr) : MetaM Expr :=
+private def buildBelowMinorPremise (rlvl : Level) (motives : Array Expr) (minorType : Expr) : MetaM Expr :=
   forallTelescope minorType fun minor_args _ => do go #[] minor_args.toList
 where
   ibelow := rlvl matches .zero
@@ -96,7 +95,7 @@ where
   | arg::args => do
     let argType ← inferType arg
     forallTelescope argType fun arg_args arg_type => do
-      if typeFormers.contains arg_type.getAppFn then
+      if motives.contains arg_type.getAppFn then
         let name ← arg.fvarId!.getUserName
         let type' ← forallTelescope argType fun args _ => mkForallFVars args (.sort rlvl)
         withLocalDeclD name type' fun arg' => do
@@ -124,81 +123,100 @@ fun {α} {motive} t =>
   List.rec True (fun head tail tail_ih => (motive tail ∧ tail_ih) ∧ True) t
 ```
 -/
-private def mkBelowOrIBelow (indName : Name) (ibelow : Bool) : MetaM Unit := do
-  let .inductInfo indVal ← getConstInfo indName | return
-  unless indVal.isRec do return
-  if ← isPropFormerType indVal.type then return
-
-  let recName := mkRecName indName
+private def mkBelowFromRec (recName : Name) (ibelow reflexive : Bool) (nParams : Nat)
+  (belowName : Name) : MetaM Unit := do
   -- The construction follows the type of `ind.rec`
   let .recInfo recVal ← getConstInfo recName
     | throwError "{recName} not a .recInfo"
   let lvl::lvls := recVal.levelParams.map (Level.param ·)
     | throwError "recursor {recName} has no levelParams"
   let lvlParam := recVal.levelParams.head!
-  -- universe parameter names of ibelow/below
-  let blvls :=
-    -- For ibelow we instantiate the first universe parameter of `.rec` to `.zero`
-    if ibelow then recVal.levelParams.tail!
-              else recVal.levelParams
-  let .some ilvl ← typeFormerTypeLevel indVal.type
-    | throwError "type {indVal.type} of inductive {indVal.name} not a type former?"
-
-  -- universe level of the resultant type
-  let rlvl : Level :=
-    if ibelow then
-      0
-    else if indVal.isReflexive then
-      if let .max 1 ilvl' := ilvl then
-        mkLevelMax' (.succ lvl) ilvl'
-      else
-        mkLevelMax' (.succ lvl) ilvl
-    else
-      mkLevelMax' 1 lvl
 
   let refType :=
     if ibelow then
       recVal.type.instantiateLevelParams [lvlParam] [0]
-    else if indVal.isReflexive then
+    else if reflexive then
       recVal.type.instantiateLevelParams [lvlParam] [lvl.succ]
     else
       recVal.type
 
   let decl ← forallTelescope refType fun refArgs _ => do
-    assert! refArgs.size == indVal.numParams + recVal.numMotives + recVal.numMinors + indVal.numIndices + 1
-    let params      : Array Expr := refArgs[:indVal.numParams]
-    let typeFormers : Array Expr := refArgs[indVal.numParams:indVal.numParams + recVal.numMotives]
-    let minors      : Array Expr := refArgs[indVal.numParams + recVal.numMotives:indVal.numParams + recVal.numMotives + recVal.numMinors]
-    let remaining   : Array Expr := refArgs[indVal.numParams + recVal.numMotives + recVal.numMinors:]
+    assert! refArgs.size > nParams + recVal.numMotives + recVal.numMinors
+    let params  : Array Expr := refArgs[:nParams]
+    let motives : Array Expr := refArgs[nParams:nParams + recVal.numMotives]
+    let minors  : Array Expr := refArgs[nParams + recVal.numMotives:nParams + recVal.numMotives + recVal.numMinors]
+    let indices : Array Expr := refArgs[nParams + recVal.numMotives + recVal.numMinors:refArgs.size - 1]
+    let major   : Expr       := refArgs[refArgs.size - 1]!
+
+    -- universe parameter names of ibelow/below
+    let blvls :=
+      -- For ibelow we instantiate the first universe parameter of `.rec` to `.zero`
+      if ibelow then recVal.levelParams.tail!
+                else recVal.levelParams
+    -- universe parameter of the type fomer.
+    -- same as `typeFormerTypeLevel indVal.type`, but we want to infer it from the
+    -- type of the recursor, to be more robust when facing nested induction
+    let majorTypeType ← inferType (← inferType major)
+    let .some ilvl ← typeFormerTypeLevel majorTypeType
+      | throwError "type of type of major premise {major} not a type former"
+
+    -- universe level of the resultant type
+    let rlvl : Level :=
+      if ibelow then
+        0
+      else if reflexive then
+        if let .max 1 ilvl' := ilvl then
+          mkLevelMax' (.succ lvl) ilvl'
+        else
+          mkLevelMax' (.succ lvl) ilvl
+      else
+        mkLevelMax' 1 lvl
 
     let mut val := .const recName (rlvl.succ :: lvls)
     -- add parameters
     val := mkAppN val params
     -- add type formers
-    for typeFormer in typeFormers do
-      let arg ← forallTelescope (← inferType typeFormer) fun targs _ =>
+    for motive in motives do
+      let arg ← forallTelescope (← inferType motive) fun targs _ =>
         mkLambdaFVars targs (.sort rlvl)
       val := .app val arg
     -- add minor premises
     for minor in minors do
-      let arg ← buildBelowMinorPremise rlvl typeFormers (← inferType minor)
+      let arg ← buildBelowMinorPremise rlvl motives (← inferType minor)
       val := .app val arg
     -- add indices and major premise
-    val := mkAppN val remaining
+    val := mkAppN val indices
+    val := mkApp val major
 
     -- All paramaters of `.rec` besides the `minors` become parameters of `.below`
-    let below_params := params ++ typeFormers ++ remaining
+    let below_params := params ++ motives ++ indices ++ #[major]
     let type ← mkForallFVars below_params (.sort rlvl)
     val ← mkLambdaFVars below_params val
 
-    let name := if ibelow then mkIBelowName indName else mkBelowName indName
-    mkDefinitionValInferrringUnsafe name blvls type val .abbrev
+    mkDefinitionValInferrringUnsafe belowName blvls type val .abbrev
 
   addDecl (.defnDecl decl)
   setReducibleAttribute decl.name
   modifyEnv fun env => markAuxRecursor env decl.name
   modifyEnv fun env => addProtected env decl.name
 
+private def mkBelowOrIBelow (indName : Name) (ibelow : Bool) : MetaM Unit := do
+  let .inductInfo indVal ← getConstInfo indName | return
+  unless indVal.isRec do return
+  if ← isPropFormerType indVal.type then return
+
+  let recName := mkRecName indName
+  let belowName := if ibelow then mkIBelowName indName else mkBelowName indName
+  mkBelowFromRec recName ibelow indVal.isReflexive indVal.numParams belowName
+
+  -- If this is the first inductive in a mutual group with nested inductives,
+  -- generate the constructions for the nested inductives now
+  if indVal.all[0]! = indName then
+    for i in [:indVal.numNested] do
+      let recName := recName.appendIndexAfter (i + 1)
+      let belowName := belowName.appendIndexAfter (i + 1)
+      mkBelowFromRec recName ibelow indVal.isReflexive indVal.numParams belowName
+
 def mkBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName true
 def mkIBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName false
 
@@ -219,22 +237,21 @@ of type
   PProd (motive tail) (List.below tail) →
   PProd (motive (head :: tail)) (PProd (PProd (motive tail) (List.below tail)) PUnit)
 ```
-The parameter `typeFormers` are the `motive`s.
 -/
-private def buildBRecOnMinorPremise (rlvl : Level) (typeFormers : Array Expr)
+private def buildBRecOnMinorPremise (rlvl : Level) (motives : Array Expr)
     (belows : Array Expr) (fs : Array Expr) (minorType : Expr) : MetaM Expr :=
   forallTelescope minorType fun minor_args minor_type => do
     let rec go (prods : Array Expr) : List Expr → MetaM Expr
       | [] => minor_type.withApp fun minor_type_fn minor_type_args => do
           let b ← mkNProdMk rlvl prods
-          let .some ⟨idx, _⟩ := typeFormers.indexOf? minor_type_fn
-            | throwError m!"Did not find {minor_type} in {typeFormers}"
+          let .some ⟨idx, _⟩ := motives.indexOf? minor_type_fn
+            | throwError m!"Did not find {minor_type} in {motives}"
           mkPProdMk (mkAppN fs[idx]! (minor_type_args.push b)) b
       | arg::args => do
         let argType ← inferType arg
         forallTelescope argType fun arg_args arg_type => do
           arg_type.withApp fun arg_type_fn arg_type_args => do
-            if let .some idx := typeFormers.indexOf? arg_type_fn then
+            if let .some idx := motives.indexOf? arg_type_fn then
               let name ← arg.fvarId!.getUserName
               let type' ← mkForallFVars arg_args
                 (← mkPProd arg_type (mkAppN belows[idx]! arg_type_args) )
@@ -277,81 +294,72 @@ fun {α} {motive} t F_1 => (
   ).1
 ```
 -/
-def mkBRecOnOrBInductionOn (indName : Name) (ind : Bool) : MetaM Unit := do
-  let .inductInfo indVal ← getConstInfo indName | return
-  unless indVal.isRec do return
-  if ← isPropFormerType indVal.type then return
-  let recName := mkRecName indName
+private def mkBRecOnFromRec (recName : Name) (ind reflexive : Bool) (nParams : Nat)
+    (all : Array Name) (brecOnName : Name) : MetaM Unit := do
   let .recInfo recVal ← getConstInfo recName | return
-  unless recVal.numMotives = indVal.all.length do
-    /-
-    The mutual declaration containing `declName` contains nested inductive datatypes.
-    We don't support this kind of declaration here yet. We probably never will :)
-    To support it, we will need to generate an auxiliary `below` for each nested inductive
-    type since their default `below` is not good here. For example, at
-    ```
-    inductive Term
-    | var : String -> Term
-    | app : String -> List Term -> Term
-    ```
-    The `List.below` is not useful since it will not allow us to recurse over the nested terms.
-    We need to generate another one using the auxiliary recursor `Term.rec_1` for `List Term`.
-    -/
-    return
-
   let lvl::lvls := recVal.levelParams.map (Level.param ·)
     | throwError "recursor {recName} has no levelParams"
   let lvlParam := recVal.levelParams.head!
   -- universe parameter names of brecOn/binductionOn
   let blps := if ind then recVal.levelParams.tail!  else recVal.levelParams
-  -- universe arguments of below/ibelow
-  let blvls := if ind then lvls else lvl::lvls
-
-  let .some ⟨idx, _⟩ := indVal.all.toArray.indexOf? indName
-    | throwError m!"Did not find {indName} in {indVal.all}"
-
-  let .some ilvl ← typeFormerTypeLevel indVal.type
-    | throwError "type {indVal.type} of inductive {indVal.name} not a type former?"
-  -- universe level of the resultant type
-  let rlvl : Level :=
-    if ind then
-      0
-    else if indVal.isReflexive then
-      if let .max 1 ilvl' := ilvl then
-        mkLevelMax' (.succ lvl) ilvl'
-      else
-        mkLevelMax' (.succ lvl) ilvl
-    else
-      mkLevelMax' 1 lvl
 
   let refType :=
     if ind then
       recVal.type.instantiateLevelParams [lvlParam] [0]
-    else if indVal.isReflexive then
+    else if reflexive then
       recVal.type.instantiateLevelParams [lvlParam] [lvl.succ]
     else
       recVal.type
 
-  let decl ← forallTelescope refType fun refArgs _ => do
-    assert! refArgs.size == indVal.numParams + recVal.numMotives + recVal.numMinors + indVal.numIndices + 1
-    let params      : Array Expr := refArgs[:indVal.numParams]
-    let typeFormers : Array Expr := refArgs[indVal.numParams:indVal.numParams + recVal.numMotives]
-    let minors      : Array Expr := refArgs[indVal.numParams + recVal.numMotives:indVal.numParams + recVal.numMotives + recVal.numMinors]
-    let remaining   : Array Expr := refArgs[indVal.numParams + recVal.numMotives + recVal.numMinors:]
+  let decl ← forallTelescope refType fun refArgs refBody => do
+    assert! refArgs.size > nParams + recVal.numMotives + recVal.numMinors
+    let params  : Array Expr := refArgs[:nParams]
+    let motives : Array Expr := refArgs[nParams:nParams + recVal.numMotives]
+    let minors  : Array Expr := refArgs[nParams + recVal.numMotives:nParams + recVal.numMotives + recVal.numMinors]
+    let indices : Array Expr := refArgs[nParams + recVal.numMotives + recVal.numMinors:refArgs.size - 1]
+    let major   : Expr       := refArgs[refArgs.size - 1]!
 
-    -- One `below` for each type former (same parameters)
-    let belows := indVal.all.toArray.map fun n =>
-      let belowName := if ind then mkIBelowName n else mkBelowName n
-      mkAppN (.const belowName blvls) (params ++ typeFormers)
+    let some idx := motives.indexOf? refBody.getAppFn
+      | throwError "result type of {refType} is not one of {motives}"
 
-    -- create types of functionals (one for each type former)
+    -- universe parameter of the type fomer.
+    -- same as `typeFormerTypeLevel indVal.type`, but we want to infer it from the
+    -- type of the recursor, to be more robust when facing nested induction
+    let majorTypeType ← inferType (← inferType major)
+    let .some ilvl ← typeFormerTypeLevel majorTypeType
+      | throwError "type of type of major premise {major} not a type former"
+
+    -- universe level of the resultant type
+    let rlvl : Level :=
+      if ind then
+        0
+      else if reflexive then
+        if let .max 1 ilvl' := ilvl then
+          mkLevelMax' (.succ lvl) ilvl'
+        else
+          mkLevelMax' (.succ lvl) ilvl
+      else
+        mkLevelMax' 1 lvl
+
+    -- One `below` for each motive, with the same motive parameters
+    let blvls := if ind then lvls else lvl::lvls
+    let belows := Array.ofFn (n := motives.size) fun ⟨i,_⟩ =>
+      let belowName :=
+        if let some n := all[i]? then
+          if ind then mkIBelowName n else mkBelowName n
+        else
+          if ind then .str all[0]! s!"ibelow_{i-all.size+1}"
+                 else .str all[0]! s!"below_{i-all.size+1}"
+      mkAppN (.const belowName blvls) (params ++ motives)
+
+    -- create types of functionals (one for each motive)
     --   (F_1 : (t : List α) → (f : List.below t) → motive t)
     -- and bring parameters of that type into scope
     let mut fDecls : Array (Name × (Array Expr -> MetaM Expr)) := #[]
-    for typeFormer in typeFormers, below in belows, i in [:typeFormers.size] do
-      let fType ← forallTelescope (← inferType typeFormer) fun targs _ => do
+    for motive in motives, below in belows, i in [:motives.size] do
+      let fType ← forallTelescope (← inferType motive) fun targs _ => do
         withLocalDeclD `f (mkAppN below targs) fun f =>
-          mkForallFVars (targs.push f) (mkAppN typeFormer targs)
+          mkForallFVars (targs.push f) (mkAppN motive targs)
       let fName := .mkSimple s!"F_{i + 1}"
       fDecls := fDecls.push (fName, fun _ => pure fType)
     withLocalDeclsD fDecls fun fs => do
@@ -359,35 +367,53 @@ def mkBRecOnOrBInductionOn (indName : Name) (ind : Bool) : MetaM Unit := do
       -- add parameters
       val := mkAppN val params
       -- add type formers
-      for typeFormer in typeFormers, below in belows do
+      for motive in motives, below in belows do
         -- example: (motive := fun t => PProd (motive t) (@List.below α motive t))
-        let arg ← forallTelescope (← inferType typeFormer) fun targs _ => do
-          let cType := mkAppN typeFormer targs
+        let arg ← forallTelescope (← inferType motive) fun targs _ => do
+          let cType := mkAppN motive targs
           let belowType := mkAppN below targs
           let arg ← mkPProd cType belowType
           mkLambdaFVars targs arg
         val := .app val arg
       -- add minor premises
       for minor in minors do
-        let arg ← buildBRecOnMinorPremise rlvl typeFormers belows fs (← inferType minor)
+        let arg ← buildBRecOnMinorPremise rlvl motives belows fs (← inferType minor)
         val := .app val arg
       -- add indices and major premise
-      val := mkAppN val remaining
+      val := mkAppN val indices
+      val := mkApp val major
       -- project out first component
       val ← mkPProdFst val
 
       -- All paramaters of `.rec` besides the `minors` become parameters of `.bRecOn`, and the `fs`
-      let below_params := params ++ typeFormers ++ remaining ++ fs
-      let type ← mkForallFVars below_params (mkAppN typeFormers[idx]! remaining)
+      let below_params := params ++ motives ++ indices ++ #[major] ++ fs
+      let type ← mkForallFVars below_params (mkAppN motives[idx]! (indices ++ #[major]))
       val ← mkLambdaFVars below_params val
 
-      let name := if ind then mkBInductionOnName indName else mkBRecOnName indName
-      mkDefinitionValInferrringUnsafe name blps type val .abbrev
+      mkDefinitionValInferrringUnsafe brecOnName blps type val .abbrev
 
   addDecl (.defnDecl decl)
   setReducibleAttribute decl.name
   modifyEnv fun env => markAuxRecursor env decl.name
   modifyEnv fun env => addProtected env decl.name
 
+def mkBRecOnOrBInductionOn (indName : Name) (ind : Bool) : MetaM Unit := do
+  let .inductInfo indVal ← getConstInfo indName | return
+  unless indVal.isRec do return
+  if ← isPropFormerType indVal.type then return
+
+  let recName := mkRecName indName
+  let brecOnName := if ind then mkBInductionOnName indName else mkBRecOnName indName
+  mkBRecOnFromRec recName ind indVal.isReflexive indVal.numParams indVal.all.toArray brecOnName
+
+  -- If this is the first inductive in a mutual group with nested inductives,
+  -- generate the constructions for the nested inductives now.
+  if indVal.all[0]! = indName then
+    for i in [:indVal.numNested] do
+      let recName := recName.appendIndexAfter (i + 1)
+      let brecOnName := brecOnName.appendIndexAfter (i + 1)
+      mkBRecOnFromRec recName ind indVal.isReflexive indVal.numParams indVal.all.toArray brecOnName
+
+
 def mkBRecOn (declName : Name) : MetaM Unit := mkBRecOnOrBInductionOn declName false
 def mkBInductionOn (declName : Name) : MetaM Unit := mkBRecOnOrBInductionOn declName true

tests/lean/run/nestedInductiveConstructions.lean

@@ -0,0 +1,214 @@
+/-!
+Checks the `.below` and `.brecOn` constructions for nested inductives.
+-/
+
+set_option pp.universes true
+
+namespace Ex1
+
+inductive Tree where | node  : List Tree → Tree
+
+/--
+info: @[reducible] protected def Ex1.Tree.below.{u} : {motive_1 : Tree → Sort u} →
+  {motive_2 : List.{0} Tree → Sort u} → Tree → Sort (max 1 u) :=
+fun {motive_1} {motive_2} t =>
+  Tree.rec.{(max 1 u) + 1}
+    (fun a a_ih => PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) PUnit.{max 1 u}) PUnit.{max 1 u}
+    (fun head tail head_ih tail_ih =>
+      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih)
+        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u}))
+    t
+-/
+#guard_msgs in
+#print Tree.below
+
+/--
+info: @[reducible] protected def Ex1.Tree.below_1.{u} : {motive_1 : Tree → Sort u} →
+  {motive_2 : List.{0} Tree → Sort u} → List.{0} Tree → Sort (max 1 u) :=
+fun {motive_1} {motive_2} t =>
+  Tree.rec_1.{(max 1 u) + 1}
+    (fun a a_ih => PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) PUnit.{max 1 u}) PUnit.{max 1 u}
+    (fun head tail head_ih tail_ih =>
+      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih)
+        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u}))
+    t
+-/
+#guard_msgs in
+#print Tree.below_1
+
+/--
+info: @[reducible] protected def Ex1.Tree.ibelow_1 : {motive_1 : Tree → Prop} →
+  {motive_2 : List.{0} Tree → Prop} → List.{0} Tree → Prop :=
+fun {motive_1} {motive_2} t =>
+  Tree.rec_1.{1} (fun a a_ih => And (And (motive_2 a) a_ih) True) True
+    (fun head tail head_ih tail_ih => And (And (motive_1 head) head_ih) (And (And (motive_2 tail) tail_ih) True)) t
+-/
+#guard_msgs in
+#print Tree.ibelow_1
+
+/--
+info: Ex1.Tree.brecOn.{u} {motive_1 : Tree → Sort u} {motive_2 : List.{0} Tree → Sort u} (t : Tree)
+  (F_1 : (t : Tree) → Tree.below.{u} t → motive_1 t) (F_2 : (t : List.{0} Tree) → Tree.below_1.{u} t → motive_2 t) :
+  motive_1 t
+-/
+#guard_msgs in
+#check Tree.brecOn
+
+/--
+info: Ex1.Tree.brecOn_1.{u} {motive_1 : Tree → Sort u} {motive_2 : List.{0} Tree → Sort u} (t : List.{0} Tree)
+  (F_1 : (t : Tree) → Tree.below.{u} t → motive_1 t) (F_2 : (t : List.{0} Tree) → Tree.below_1.{u} t → motive_2 t) :
+  motive_2 t
+-/
+#guard_msgs in
+#check Tree.brecOn_1
+
+/--
+info: Ex1.Tree.binductionOn_1 {motive_1 : Tree → Prop} {motive_2 : List.{0} Tree → Prop} (t : List.{0} Tree)
+  (F_1 : ∀ (t : Tree), Tree.ibelow t → motive_1 t) (F_2 : ∀ (t : List.{0} Tree), Tree.ibelow_1 t → motive_2 t) :
+  motive_2 t
+-/
+#guard_msgs in
+#check Tree.binductionOn_1
+
+end Ex1
+
+namespace Ex2
+
+inductive Tree where | node  : List (List Tree) → List Tree → Tree
+
+/--
+info: @[reducible] protected def Ex2.Tree.below.{u} : {motive_1 : Tree → Sort u} →
+  {motive_2 : List.{0} (List.{0} Tree) → Sort u} → {motive_3 : List.{0} Tree → Sort u} → Tree → Sort (max 1 u) :=
+fun {motive_1} {motive_2} {motive_3} t =>
+  Tree.rec.{(max 1 u) + 1}
+    (fun a a_1 a_ih a_ih_1 =>
+      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih)
+        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1) PUnit.{max 1 u}))
+    PUnit.{max 1 u}
+    (fun head tail head_ih tail_ih =>
+      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 head) head_ih)
+        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u}))
+    PUnit.{max 1 u}
+    (fun head tail head_ih tail_ih =>
+      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih)
+        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 tail) tail_ih) PUnit.{max 1 u}))
+    t
+-/
+#guard_msgs in
+#print Tree.below
+
+/--
+info: @[reducible] protected def Ex2.Tree.below_1.{u} : {motive_1 : Tree → Sort u} →
+  {motive_2 : List.{0} (List.{0} Tree) → Sort u} →
+    {motive_3 : List.{0} Tree → Sort u} → List.{0} (List.{0} Tree) → Sort (max 1 u) :=
+fun {motive_1} {motive_2} {motive_3} t =>
+  Tree.rec_1.{(max 1 u) + 1}
+    (fun a a_1 a_ih a_ih_1 =>
+      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih)
+        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1) PUnit.{max 1 u}))
+    PUnit.{max 1 u}
+    (fun head tail head_ih tail_ih =>
+      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 head) head_ih)
+        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u}))
+    PUnit.{max 1 u}
+    (fun head tail head_ih tail_ih =>
+      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih)
+        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 tail) tail_ih) PUnit.{max 1 u}))
+    t
+-/
+#guard_msgs in
+#print Tree.below_1
+
+/--
+info: @[reducible] protected def Ex2.Tree.below_2.{u} : {motive_1 : Tree → Sort u} →
+  {motive_2 : List.{0} (List.{0} Tree) → Sort u} →
+    {motive_3 : List.{0} Tree → Sort u} → List.{0} Tree → Sort (max 1 u) :=
+fun {motive_1} {motive_2} {motive_3} t =>
+  Tree.rec_2.{(max 1 u) + 1}
+    (fun a a_1 a_ih a_ih_1 =>
+      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih)
+        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1) PUnit.{max 1 u}))
+    PUnit.{max 1 u}
+    (fun head tail head_ih tail_ih =>
+      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 head) head_ih)
+        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u}))
+    PUnit.{max 1 u}
+    (fun head tail head_ih tail_ih =>
+      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih)
+        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 tail) tail_ih) PUnit.{max 1 u}))
+    t
+-/
+#guard_msgs in
+#print Tree.below_2
+
+/--
+info: Ex2.Tree.brecOn_2.{u} {motive_1 : Tree → Sort u} {motive_2 : List.{0} (List.{0} Tree) → Sort u}
+  {motive_3 : List.{0} Tree → Sort u} (t : List.{0} Tree) (F_1 : (t : Tree) → Tree.below.{u} t → motive_1 t)
+  (F_2 : (t : List.{0} (List.{0} Tree)) → Tree.below_1.{u} t → motive_2 t)
+  (F_3 : (t : List.{0} Tree) → Tree.below_2.{u} t → motive_3 t) : motive_3 t
+-/
+#guard_msgs in
+#check Tree.brecOn_2
+
+/--
+info: Ex2.Tree.binductionOn_2 {motive_1 : Tree → Prop} {motive_2 : List.{0} (List.{0} Tree) → Prop}
+  {motive_3 : List.{0} Tree → Prop} (t : List.{0} Tree) (F_1 : ∀ (t : Tree), Tree.ibelow t → motive_1 t)
+  (F_2 : ∀ (t : List.{0} (List.{0} Tree)), Tree.ibelow_1 t → motive_2 t)
+  (F_3 : ∀ (t : List.{0} Tree), Tree.ibelow_2 t → motive_3 t) : motive_3 t
+-/
+#guard_msgs in
+#check Tree.binductionOn_2
+
+end Ex2
+
+namespace Ex3
+
+inductive Tree : Type u where | node : List Tree → Tree
+
+/--
+info: @[reducible] protected def Ex3.Tree.below.{u_1, u} : {motive_1 : Tree.{u} → Sort u_1} →
+  {motive_2 : List.{u} Tree.{u} → Sort u_1} → Tree.{u} → Sort (max 1 u_1) :=
+fun {motive_1} {motive_2} t =>
+  Tree.rec.{(max 1 u_1) + 1, u}
+    (fun a a_ih => PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_2 a) a_ih) PUnit.{max 1 u_1})
+    PUnit.{max 1 u_1}
+    (fun head tail head_ih tail_ih =>
+      PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_1 head) head_ih)
+        (PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_2 tail) tail_ih) PUnit.{max 1 u_1}))
+    t
+-/
+#guard_msgs in
+#print Tree.below
+
+/--
+info: @[reducible] protected def Ex3.Tree.below_1.{u_1, u} : {motive_1 : Tree.{u} → Sort u_1} →
+  {motive_2 : List.{u} Tree.{u} → Sort u_1} → List.{u} Tree.{u} → Sort (max 1 u_1) :=
+fun {motive_1} {motive_2} t =>
+  Tree.rec_1.{(max 1 u_1) + 1, u}
+    (fun a a_ih => PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_2 a) a_ih) PUnit.{max 1 u_1})
+    PUnit.{max 1 u_1}
+    (fun head tail head_ih tail_ih =>
+      PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_1 head) head_ih)
+        (PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_2 tail) tail_ih) PUnit.{max 1 u_1}))
+    t
+-/
+#guard_msgs in
+#print Tree.below_1
+
+/--
+info: Ex3.Tree.brecOn_1.{u_1, u} {motive_1 : Tree.{u} → Sort u_1} {motive_2 : List.{u} Tree.{u} → Sort u_1}
+  (t : List.{u} Tree.{u}) (F_1 : (t : Tree.{u}) → Tree.below.{u_1, u} t → motive_1 t)
+  (F_2 : (t : List.{u} Tree.{u}) → Tree.below_1.{u_1, u} t → motive_2 t) : motive_2 t
+-/
+#guard_msgs in
+#check Tree.brecOn_1
+
+/--
+info: Ex3.Tree.binductionOn_1.{u} {motive_1 : Tree.{u} → Prop} {motive_2 : List.{u} Tree.{u} → Prop} (t : List.{u} Tree.{u})
+  (F_1 : ∀ (t : Tree.{u}), Tree.ibelow.{u} t → motive_1 t)
+  (F_2 : ∀ (t : List.{u} Tree.{u}), Tree.ibelow_1.{u} t → motive_2 t) : motive_2 t
+-/
+#guard_msgs in
+#check Tree.binductionOn_1
+
+end Ex3

tests/lean/run/structuralMutual.lean

@@ -327,39 +327,15 @@ inductive Tree where
   | leaf
   | node : (Tree × Tree) → Tree
 
-def Tree.below_1 (motive : Tree → Sort u) : Tree → Sort (max 1 u) :=
-  @Tree.below motive (fun _tt => PUnit)
+-- Nested recursion does not work (yet)
 
--- Assume we had this construction:
-@[reducible] protected noncomputable def Tree.brecOn.{u}
-  {motive : Tree → Sort u}
-  (t : Tree)
-  (F : (t : Tree) → Tree.below_1 motive t → motive t) :
-  motive t :=
-  let motive_below := fun t => PProd (motive t) (Tree.below_1 motive t)
-  (@Tree.rec
-    motive_below
-    -- This is the hypthetical `Pair_Tree.below tt` unfolded
-    (fun ⟨t₁,t₂⟩ => PProd PUnit.{u} (PProd (motive_below t₁) (PProd (motive_below t₂) PUnit)))
-    ⟨F Tree.leaf PUnit.unit, PUnit.unit⟩
-    (fun ⟨a₁,a₂⟩ a_ih => ⟨F (Tree.node ⟨a₁, a₂⟩) ⟨a_ih, PUnit.unit⟩, ⟨a_ih, PUnit.unit⟩⟩)
-    (fun _a _a_1 a_ih a_ih_1 => ⟨PUnit.unit, ⟨a_ih, ⟨a_ih_1, PUnit.unit⟩⟩⟩)
-    t).1
-
--- Then the decrecursifier works just fine! (and FunInd too, see below)
+/-- error: its type NestedWithTuple.Tree is a nested inductive, which is not yet supported -/
 #guard_msgs in
 def Tree.size : Tree → Nat
   | leaf => 0
   | node (t₁, t₂) => t₁.size + t₂.size
 termination_by structural t => t
 
-/--
-info: theorem NestedWithTuple.Tree.size.eq_2 : ∀ (t₁ t₂ : Tree), (Tree.node (t₁, t₂)).size = t₁.size + t₂.size :=
-fun t₁ t₂ => Eq.refl (Tree.node (t₁, t₂)).size
--/
-#guard_msgs in
-#print Tree.size.eq_2
-
 end NestedWithTuple
 
 
@@ -617,12 +593,4 @@ error: unknown identifier 'EvenOdd.isEven.induct'
 run_meta
   Lean.modifyEnv fun env => Lean.markAuxRecursor env ``NestedWithTuple.Tree.brecOn
 
-/--
-info: NestedWithTuple.Tree.size.induct (motive : NestedWithTuple.Tree → Prop) (case1 : motive NestedWithTuple.Tree.leaf)
-  (case2 : ∀ (t₁ t₂ : NestedWithTuple.Tree), motive t₁ → motive t₂ → motive (NestedWithTuple.Tree.node (t₁, t₂))) :
-  ∀ (a : NestedWithTuple.Tree), motive a
--/
-#guard_msgs in
-#check NestedWithTuple.Tree.size.induct
-
 end FunIndTests