refactor: IndGroupInst.brecOn (#4787)

this logic fits nicely within `IndGroupInst`.

Also makes `isAuxRecursorWithSuffix` recognize `brecOn_<n>`.

src/Lean/AuxRecursor.lean

@@ -37,7 +37,7 @@ def isAuxRecursor (env : Environment) (declName : Name) : Bool :=
 
 def isAuxRecursorWithSuffix (env : Environment) (declName : Name) (suffix : String) : Bool :=
   match declName with
-  | .str _ s => s == suffix && isAuxRecursor env declName
+  | .str _ s => (s == suffix || s.startsWith s!"{suffix}_") && isAuxRecursor env declName
   | _ => false
 
 def isCasesOnRecursor (env : Environment) (declName : Name) : Bool :=

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

@@ -245,18 +245,7 @@ def mkBRecOnConst (recArgInfos : Array RecArgInfo) (positions : Positions)
       decLevel brecOnUniv
     else
       pure brecOnUniv
-  let brecOnCons := fun idx  =>
-    let brecOn :=
-      if let .some n := indGroup.all[idx]? then
-        if useBInductionOn then .const (mkBInductionOnName n) indGroup.levels
-        else                    .const (mkBRecOnName n) (brecOnUniv :: indGroup.levels)
-      else
-        let n := indGroup.all[0]!
-        let j := idx - indGroup.all.size + 1
-        if useBInductionOn then .const (mkBInductionOnName n |>.appendIndexAfter j) indGroup.levels
-        else                    .const (mkBRecOnName n |>.appendIndexAfter j) (brecOnUniv :: indGroup.levels)
-    mkAppN brecOn indGroup.params
-
+  let brecOnCons := fun idx => indGroup.brecOn useBInductionOn brecOnUniv idx
   -- Pick one as a prototype
   let brecOnAux := brecOnCons 0
   -- Infer the type of the packed motive arguments

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

@@ -62,6 +62,19 @@ def IndGroupInst.isDefEq (igi1 igi2 : IndGroupInst) : MetaM Bool := do
   unless (← (igi1.params.zip igi2.params).allM (fun (e₁, e₂) => Meta.isDefEqGuarded e₁ e₂)) do return false
   return true
 
+/-- Instantiates the right `.brecOn` or `.bInductionOn` for the given type former index,
+including universe parameters and fixed prefix.  -/
+def IndGroupInst.brecOn (group : IndGroupInst) (ind : Bool) (lvl : Level) (idx : Nat) : Expr :=
+  let e := if let .some n := group.all[idx]? then
+      if ind then .const (mkBInductionOnName n) group.levels
+      else        .const (mkBRecOnName n)      (lvl :: group.levels)
+    else
+      let n := group.all[0]!
+      let j := idx - group.all.size + 1
+      if ind then .const (mkBInductionOnName n |>.appendIndexAfter j) group.levels
+      else        .const (mkBRecOnName n |>.appendIndexAfter j)       (lvl :: group.levels)
+  mkAppN e group.params
+
 /--
 Figures out the nested type formers of an inductive group, with parameters instantiated
 and indices still forall-abstracted.

tests/lean/run/funind_structural.lean

@@ -1,6 +1,3 @@
-import Lean.Elab.Command
-import Lean.Elab.PreDefinition.Structural.Eqns
-
 /-!
 This module tests functional induction principles on *structurally* recursive functions.
 -/
@@ -8,6 +5,7 @@ This module tests functional induction principles on *structurally* recursive fu
 def fib : Nat → Nat
   | 0 | 1 => 0
   | n+2 => fib n + fib (n+1)
+termination_by structural x => x
 
 /--
 info: fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
@@ -20,6 +18,7 @@ info: fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
 def binary : Nat → Nat → Nat
   | 0, acc | 1, acc => 1 + acc
   | n+2, acc => binary n (binary (n+1) acc)
+termination_by structural x => x
 
 /--
 info: binary.induct (motive : Nat → Nat → Prop) (case1 : ∀ (acc : Nat), motive 0 acc) (case2 : ∀ (acc : Nat), motive 1 acc)
@@ -34,6 +33,7 @@ info: binary.induct (motive : Nat → Nat → Prop) (case1 : ∀ (acc : Nat), mo
 def binary' : Bool → Nat → Bool
   | acc, 0 | acc , 1 => not acc
   | acc, n+2 => binary' (binary' acc (n+1)) n
+termination_by structural _ x => x
 
 /--
 info: binary'.induct (motive : Bool → Nat → Prop) (case1 : ∀ (acc : Bool), motive acc 0)
@@ -48,6 +48,7 @@ def zip {α β} : List α → List β → List (α × β)
   | [], _ => []
   | _, [] => []
   | x::xs, y::ys => (x, y) :: zip xs ys
+termination_by structural x => x
 
 /--
 info: zip.induct.{u_1, u_2} {α : Type u_1} {β : Type u_2} (motive : List α → List β → Prop)
@@ -84,6 +85,7 @@ def Finn.min (x : Bool) {n : Nat} (m : Nat) : Finn n → (f : Finn n) → Finn n
   | fzero, _ => fzero
   | _, fzero => fzero
   | fsucc i, fsucc j => fsucc (Finn.min (not x) (m + 1) i j)
+termination_by structural n
 
 /--
 info: Finn.min.induct (motive : Bool → {n : Nat} → Nat → Finn n → Finn n → Prop)
@@ -95,8 +97,6 @@ info: Finn.min.induct (motive : Bool → {n : Nat} → Nat → Finn n → Finn n
 #guard_msgs in
 #check Finn.min.induct
 
-
-
 namespace TreeExample
 
 inductive Tree (β : Type v) where
@@ -113,6 +113,7 @@ def Tree.insert (t : Tree β) (k : Nat) (v : β) : Tree β :=
       node left key value (right.insert k v)
     else
       node left k v right
+termination_by structural t
 
 /--
 info: TreeExample.Tree.insert.induct.{u_1} {β : Type u_1} (motive : Tree β → Nat → β → Prop)
@@ -174,6 +175,7 @@ def Term.denote : Term ctx ty → HList Ty.denote ctx → ty.denote
   | .app f a,   env => f.denote env (a.denote env)
   | .lam b,     env => fun x => b.denote (.cons x env)
   | .let a b,   env => b.denote (.cons (a.denote env) env)
+termination_by structural x => x
 
 /--
 info: TermDenote.Term.denote.induct (motive : {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Prop)

tests/lean/run/structuralMutual.lean

@@ -215,6 +215,8 @@ namespace EvenOdd
 
 -- Mutual structural recursion over a non-mutual inductive type
 
+-- (The functions don't actually implement even/odd, but that isn't the point here.)
+
 mutual
   def Even : Nat → Prop
     | 0 => True
@@ -518,13 +520,13 @@ Too many possible combinations of parameters of type Nattish (or please indicate
 Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
-Call from ManyCombinations.f to ManyCombinations.g at 550:15-29:
+Call from ManyCombinations.f to ManyCombinations.g at 552:15-29:
    #1 #2 #3 #4
 #5  ?  ?  ?  ?
 #6  ?  =  ?  ?
 #7  ?  ?  =  ?
 #8  ?  ?  ?  =
-Call from ManyCombinations.g to ManyCombinations.f at 553:15-29:
+Call from ManyCombinations.g to ManyCombinations.f at 555:15-29:
    #5 #6 #7 #8
 #1  _  _  _  _
 #2  _  =  _  _