Like this

src/Lean/Elab/PreDefinition/FixedParams.lean

@@ -0,0 +1,496 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+prelude
+import Lean.Elab.PreDefinition.Basic
+
+/-!
+This module contains the logic for figuring out, given mutually recursive predefinitions,
+which parameters are “fixed”. This used to be a simple task when we only considered a fixed prefix,
+but becomes a quite involved task if we allow fixed parameters also later in the parameter list,
+and possibly in a different order in different modules.
+
+The main components of this module are
+
+ * The pure `Info` data type for the bookkeeping during analysis
+ * The `FixedParamPerm` type, with the analysis result for one function
+   (effectively a mask and a permutation)
+ * The `FixedParamPerms` data type, with the data for a whole recursive group.
+ * The `getFixedParamPerms` function that calculates the fixed parameters
+ * Various `MetaM` functions for bringing into scope fixed and varying paramters, assembling
+   argument lists etc.
+
+-/
+
+namespace Lean.Elab.FixedParams
+
+
+/--
+To determine which parameters in mutually recursive predefinitions are fixed, and how they
+correspond to each other, we run an analysis that aggregates information in the `Info` data type.
+
+Abstractly, this represents
+* a set `varying` of `(funIdx × paramIdx)` pairs known to be varying, initially empty
+* a directed graph whose nodes are `(funIdx × paramIdx)` pairs, initially empty
+
+We find the largest set and graph that satisfies these rules:
+* Every parameter has to be related to itself: `(funIdx, paramIdx) → (funIdx, paramIdx)`.
+* whenever the function with index `caller` calls `callee` and the `argIdx`'s argument is reducibly
+  defeq to `paramIdx`, then we have an edge `(caller, paramIdx) → (callee, argIdx)`.
+* whenever the function with index `caller` calls `callee` and the `argIdx`'s argument is not reducibly
+  defeq to any of the `caller`'s parameters, then `(callee, argIdx) ∈ varying`.
+* If we have `(caller, paramIdx₁) → (callee, argIdx)` and `(caller, paramIdx₂) → (callee, argIdx)`
+  with `paramIdx₁ ≠ paramIdx₂`, then `(callee, argIdx) ∈ varying`.
+* The graph is transitive
+* If we have `(caller, paramIdx) → (callee, argIdx)` and `(caller, paramIdx) ∈ varying`, then
+  `(callee, argIdx) ∈ varying`
+* If the type of `funIdx`’s parameter `paramIdx₂ depends on the `paramIdx₁` and
+  `(funIdx, paramIdx₁) ∈ varying`, then `(funIdx, paramIdx₁) ∈ varying`
+* For structural recursion: The target and all its indices are `varying`.
+  (This is taking into account post-hoc, using `FixedParamPerms.erase`)
+
+Under the assumption that the predefintions indeed are mutually recursive, then the resulting graph,
+restricted to the non-`varying` nodes, should partition into cliques that have one member from each
+function. Every such clique becomes a fixed parameter.
+
+-/
+structure Info where
+  /-
+  The concrete data structure for set and graph exploits some of the invariants:
+  * Once we know a parameter is varying, it's incoming edges are irrelevant.
+  * There can be at most one incoming edge
+
+  So we have
+
+  * `graph[callee][argIdx] = none`: `(callee, argIdx) ∈ varying`
+  * `graph[callee][argIdx] = some a`:
+    * `(callee, argIdx) ∉ varying` (yet) and
+    * `a[callerIdx] = none`: we have no edge to `(callee, argIdx)`
+    * `a[callerIdx] = some paramIdx`: we have edge `(callerIdx, paramIdx) → (callee, argIdx)`
+  -/
+  graph : Array (Array (Option (Array (Option Nat))))
+  /--
+  The dependency structure of the function parameter.
+  If `paramIdx₂ ∈ revDeps[funIdx][paraIdx₁]`, then the type of `paramIdx₂` depends on `parmaIdx₁`
+  -/
+  revDeps : Array (Array (Array Nat))
+
+
+def Info.init (revDeps : Array (Array (Array Nat))) : Info where
+  graph := revDeps.map fun deps =>
+    mkArray deps.size (some (mkArray revDeps.size none))
+  revDeps
+
+def Info.addSelfCalls (info : Info) : Info :=
+  { info with graph := info.graph.mapIdx fun funIdx paramInfos =>
+    paramInfos.mapIdx fun paramIdx paramInfo? =>
+      paramInfo?.map fun callers =>
+        callers.set! funIdx (some paramIdx) }
+
+/--
+Is this parameter still plausibly a fixed parameter?
+-/
+def Info.mayBeFixed (callerIdx paramIdx : Nat) (info : Info) : Bool :=
+  info.graph[callerIdx]![paramIdx]!.isSome
+
+/--
+This parameter is varying. Set and propagate that information.
+-/
+partial def Info.setVarying (funIdx paramIdx : Nat) (info : Info) : Info := Id.run do
+  let mut info : Info := info
+  if info.mayBeFixed funIdx paramIdx then
+    -- Set this as varying
+    info := { info with graph := info.graph.modify funIdx (·.set! paramIdx none) }
+    -- Propagate along edges for already observed calls
+    for otherFunIdx in [:info.graph.size] do
+      for otherParamIdx in [:info.graph[otherFunIdx]!.size] do
+        if let some otherParamInfo := info.graph[otherFunIdx]![otherParamIdx]! then
+          if otherParamInfo[funIdx]! = some paramIdx then
+            info := Info.setVarying otherFunIdx otherParamIdx info
+    -- Propagate along type dependencies edges
+    for dependingParam in info.revDeps[funIdx]![paramIdx]! do
+      info := Info.setVarying funIdx dependingParam info
+  info
+
+def Info.getCallerParam? (calleeIdx argIdx callerIdx : Nat) (info : Info) : Option Nat :=
+  info.graph[calleeIdx]![argIdx]!.bind (·[callerIdx]!)
+
+/--
+We observe a possibly valid edge.
+-/
+partial def Info.setCallerParam (calleeIdx argIdx callerIdx paramIdx : Nat) (info : Info) : Info :=
+  if info.mayBeFixed calleeIdx argIdx then
+    if info.mayBeFixed callerIdx paramIdx then
+      if let some paramIdx' := info.getCallerParam? calleeIdx argIdx callerIdx then
+      -- We already have an etry
+      if paramIdx = paramIdx' then
+        -- all good
+        info
+      else
+        -- Inconsistent information
+        info.setVarying calleeIdx argIdx
+    else
+      -- Set the new entry
+      let info := { info with graph := info.graph.modify calleeIdx (·.modify argIdx (·.map (·.set! callerIdx (some paramIdx)))) }
+      Id.run do
+        -- Propagate information about the caller
+        let mut info : Info := info
+        if let some callerParamInfo := info.graph[callerIdx]![paramIdx]! then
+          for h : otherFunIdx in [:callerParamInfo.size] do
+            if let some otherParamIdx := callerParamInfo[otherFunIdx] then
+              info := info.setCallerParam calleeIdx argIdx otherFunIdx otherParamIdx
+        -- Propagate information about the callee
+        for otherFunIdx in [:info.graph.size] do
+          for otherArgIdx in [:info.graph[otherFunIdx]!.size] do
+            if let some otherArgsInfo := info.graph[otherFunIdx]![otherArgIdx]! then
+              if let some paramIdx' := otherArgsInfo[calleeIdx]! then
+                if paramIdx' = argIdx then
+                  info := info.setCallerParam otherFunIdx otherArgIdx callerIdx paramIdx
+
+        return info
+    else
+      -- Param not fixed, so argument isn't either
+      info.setVarying calleeIdx argIdx
+  else
+    info
+
+def Info.format (info : Info) : Format := Format.line.joinSep <|
+  info.graph.toList.map fun paramInfos =>
+    (f!"• " ++ ·) <| f!" ".joinSep <| paramInfos.toList.map fun
+      | .none => f!"❌"
+      | .some callerInfos => .sbracket <| f!" ".joinSep <| callerInfos.toList.map fun
+        | Option.none => f!"?"
+        | .some idx => f!"#{idx+1}"
+
+
+instance : ToFormat Info := ⟨Info.format⟩
+
+end FixedParams
+
+open Lean Meta FixedParams
+
+def getParamRevDeps (preDefs : Array PreDefinition) : MetaM (Array (Array (Array Nat))) := do
+  preDefs.mapM fun preDef =>
+    lambdaTelescope preDef.value (cleanupAnnotations := true) fun xs _ => do
+      let mut revDeps := #[]
+      for h : i in [:xs.size] do
+        let mut deps := #[]
+        for h : j in [i+1:xs.size] do
+          if (← dependsOn (← inferType xs[j]) xs[i].fvarId!) then
+            deps := deps.push j
+        revDeps := revDeps.push deps
+      pure revDeps
+
+def getFixedParamsInfo (preDefs : Array PreDefinition) : MetaM FixedParams.Info := do
+  let revDeps ← getParamRevDeps preDefs
+  let arities := revDeps.map (·.size)
+  let ref ← IO.mkRef (Info.init revDeps)
+
+  ref.modify .addSelfCalls
+
+  for h : callerIdx in [:preDefs.size] do
+    let preDef := preDefs[callerIdx]
+    lambdaTelescope preDef.value fun params body => do
+      assert! params.size = arities[callerIdx]!
+
+      -- TODO: transform is overkill, a simple visit-all-subexpression that takes applications
+      -- as whole suffices
+      discard <| Meta.transform (skipConstInApp := true) body fun e => e.withApp fun f args => do
+        unless f.isConst do
+          return .continue
+        let n := f.constName!
+        let some calleeIdx := preDefs.findIdx? (·.declName = n) | return .continue
+        for argIdx in [:arities[calleeIdx]!] do
+          if (← ref.get).mayBeFixed calleeIdx argIdx then
+            if h : argIdx < args.size then
+              let arg := args[argIdx]
+              -- We have seen this before (or it is a self-call), so only check that one param
+              if let some paramIdx := (← ref.get).getCallerParam? calleeIdx argIdx callerIdx then
+                let param := params[paramIdx]!
+                unless (← withoutProofIrrelevance <| withReducible <| isDefEq param arg) do
+                  trace[Elab.definition.fixedParams] "getFixedParams: notFixed {calleeIdx} {argIdx}:\nIn {e}\n{param} =/= {arg}"
+                  ref.modify (Info.setVarying calleeIdx argIdx)
+              else
+              -- Try all parameters
+              let mut any := false
+              for h : paramIdx in [:params.size] do
+                if (← ref.get).mayBeFixed callerIdx paramIdx then
+                  let param := params[paramIdx]
+                  if (← withoutProofIrrelevance <| withReducible <| isDefEq param arg) then
+                    ref.modify (Info.setCallerParam calleeIdx argIdx callerIdx paramIdx)
+                    any := true
+              unless any do
+                trace[Elab.definition.fixedParams] "getFixedParams: notFixed {calleeIdx} {argIdx}:\nIn {e}\n{arg} not matched"
+                -- Argument is none of the plausible parameters, so it cannot be a fixed argument
+                ref.modify (Info.setVarying calleeIdx argIdx)
+            else
+              -- Underapplication
+              trace[Elab.definition.fixedParams] "getFixedParams: notFixed {calleeIdx} {argIdx}:\nIn {e}\ntoo few arguments for {argIdx}"
+              ref.modify (Info.setVarying calleeIdx argIdx)
+        return .continue
+
+  let info ← ref.get
+  trace[Elab.definition.fixedParams] "getFixedParams:{info.format.indentD}"
+  return info
+
+/--
+For a given function, a mapping from its parameters to the (indices of the) fixed parameters of the
+recursive group.
+The length of the array is the arity of the function, as determined from its body, consistent
+with the arity used by well-founded recursion.
+For the first function, they appear in order; for other functions they may be reordered.
+-/
+abbrev FixedParamPerm := Array (Option Nat)
+
+/--
+This data structure stores the result of the fixed parameter analysis. See `FixedParams.Info` for
+details on the analysis.
+-/
+structure FixedParamPerms where
+  /-- Number of fixed parameters -/
+  numFixed : Nat
+  /--
+  For each function in the clique, a mapping from its parameters to the fixed parameters.
+  For the first function, they appear in order; for other functions they may be reordered.
+   -/
+  perms : Array FixedParamPerm
+  /--
+  The dependencies among the parameters. See `FixedParams.Info.revDeps`.
+  We need this for the `FixedParamsPerm.erase` operation.
+  -/
+  revDeps : Array (Array (Array Nat))
+deriving Inhabited, Repr
+
+def getFixedParamPerms (preDefs : Array PreDefinition) : MetaM FixedParamPerms := do
+  let info ← getFixedParamsInfo preDefs
+  lambdaTelescope preDefs[0]!.value fun xs _ => do
+    let paramInfos := info.graph[0]!
+    assert! xs.size = paramInfos.size
+
+    let mut firstPerm := #[]
+    let mut numFixed := 0
+    for paramIdx in [:xs.size], x in xs, paramInfo? in paramInfos do
+      if let some paramInfo := paramInfo? then
+        assert! paramInfo[0]! = some paramIdx
+        firstPerm := firstPerm.push (some numFixed)
+        numFixed := numFixed + 1
+      else
+        firstPerm := firstPerm.push none
+
+    let mut perms := #[firstPerm]
+    for h : funIdx in [1:info.graph.size] do
+      let paramInfos := info.graph[funIdx]
+      let mut perm := #[]
+      for paramInfo? in paramInfos do
+        if let some paramInfo := paramInfo? then
+          if let some firstParamIdx := paramInfo[0]! then
+            assert! firstPerm[firstParamIdx]!.isSome
+            perm := perm.push firstPerm[firstParamIdx]!
+          else
+            panic! "Incomplete paramInfo"
+        else
+          perm := perm.push none
+      perms := perms.push perm
+
+    return { numFixed, perms, revDeps := info.revDeps }
+
+def FixedParamPerm.numFixed (perm : FixedParamPerm) : Nat :=
+  perm.countP Option.isSome
+
+def FixedParamPerm.isFixed (perm : FixedParamPerm) (i : Nat) : Bool :=
+  perm[i]?.join.isSome
+
+/--
+Brings the fixed parameters from `type`, which should the the type of the `funIdx`'s function, into
+scope.
+-/
+private partial def FixedParamPerm.forallTelescopeImpl (perm : FixedParamPerm)
+    (type : Expr) (k : Array Expr → MetaM α) : MetaM α := do
+  go 0 type (mkArray perm.numFixed (mkSort 0))
+where
+  go i type xs := do
+    match perm[i]? with
+    | .some (Option.some fixedParamIdx) =>
+      forallBoundedTelescope type (some 1) (cleanupAnnotations := true) fun xs' type => do
+        assert! xs'.size = 1
+        let x := xs'[0]!
+        assert! !(← inferType x).hasLooseBVars
+        assert! fixedParamIdx < xs.size
+        go (i + 1) type (xs.set! fixedParamIdx x)
+    | .some .none =>
+      let type ← whnf type
+      assert! type.isForall
+      go (i + 1) type.bindingBody! xs
+    | .none =>
+      k xs
+
+def FixedParamPerm.forallTelescope [MonadControlT MetaM n] [Monad n]
+    (perm : FixedParamPerm) (type : Expr) (k : Array Expr → n α) : n α := do
+  map1MetaM (fun k => perm.forallTelescopeImpl type k) k
+
+
+/--
+If `type` is the type of the `funIdx`'s function, instantiate the fixed paramters.
+-/
+def FixedParamPerm.instantiateForall (perm: FixedParamPerm) (type₀ : Expr) (xs : Array Expr) : MetaM Expr := do
+  assert! xs.size = perm.numFixed
+  let mask := perm.toList
+  go mask type₀
+where
+  go | [], type => pure type
+     | (.some fixedParamIdx)::mask, type => do
+        assert! fixedParamIdx < xs.size
+        go mask (← Meta.instantiateForall type #[xs[fixedParamIdx]!])
+     | .none::mask, type =>
+        forallBoundedTelescope type (some 1) fun ys type => do
+          assert! ys.size = 1
+          mkForallFVars ys (← go mask type)
+
+/--
+If `value` is the body of the `funIdx`'s function, instantiate the fixed paramters.
+Expects enough manifest lambdas to instantiate all fixed parameters, but can handle
+eta-contracted definitions beyond that.
+-/
+def FixedParamPerm.instantiateLambda (perm : FixedParamPerm) (value₀ : Expr) (xs : Array Expr) : MetaM Expr := do
+  assert! xs.size = perm.numFixed
+  let mask := perm.toList
+  go mask value₀
+where
+  go | [], value => pure value
+     | (.some fixedParamIdx)::mask, value => do
+        assert! fixedParamIdx < xs.size
+        go mask (← Meta.instantiateLambda value #[xs[fixedParamIdx]!])
+     | .none::mask, value =>
+        if mask.all Option.isNone then
+          -- Nothing left to do. Also helpful if we may encounter an eta-contracted value
+          return value
+        else
+          lambdaBoundedTelescope value 1 fun ys value => do
+            assert! ys.size = 1
+            mkLambdaFVars ys (← go mask value)
+
+/--
+If `xs` are arguments to the `funIdx`'s function, pick only the fixed ones, and reorder appropriately.
+Expects `xs` to match the arity of the function.
+-/
+def FixedParamPerm.pickFixed (perm : FixedParamPerm) (xs : Array α) : Array α := Id.run do
+  assert! xs.size = perm.size
+  if h : xs.size = 0 then
+    pure #[]
+  else
+    let dummy := xs[0]
+    let ys := mkArray perm.numFixed dummy
+    go (perm.zip xs).toList ys
+where
+  go | [], ys => return ys
+     | (.some fixedParamIdx, x)::xs, ys => do
+        assert! fixedParamIdx < ys.size
+        go xs (ys.set! fixedParamIdx x)
+     | (.none, _) :: perm, ys =>
+        go perm ys
+
+/--
+If `xs` are arguments to the `funIdx`'s function, pick only the varying ones.
+Unlike `pickFixed`, this function can handle over- or under-application.
+-/
+def FixedParamPerm.pickVarying (perm : FixedParamPerm) (xs : Array α) : Array α := Id.run do
+  let mut ys := #[]
+  for h : i in [:xs.size] do
+    if perm[i]?.join.isNone then ys := ys.push xs[i]
+  pure ys
+
+/--
+Intersperses the fixed and varying parameters to be in the original parameter order.
+Can handle over- or und-application (extra or missing varying args), as long
+as there are all varying parameters that go before fixed parameters.
+(We expect to always find all fixed parameters, else they woudn't be fixed parameters.)
+-/
+partial def FixedParamPerm.buildArgs (perm : FixedParamPerm) (fixedArgs varyingArgs : Array α) : Array α :=
+  assert! fixedArgs.size = perm.numFixed
+  go 0 0 #[]
+where
+  go i j (xs : Array α) :=
+    if _ : i < perm.size then
+      if let some fixedParamIdx := perm[i] then
+        if _ : fixedParamIdx < fixedArgs.size then
+          go (i + 1) j (xs.push fixedArgs[fixedParamIdx])
+        else
+          panic! "FixedParams.buildArgs: too few fixed args"
+      else
+        if _ : j < varyingArgs.size then
+          go (i + 1) (j + 1) (xs.push varyingArgs[j])
+        else
+          if perm[i:].all Option.isNone then
+            xs -- Under-application
+          else
+            panic! "FixedParams.buildArgs: too few varying args"
+    else
+      xs ++ varyingArgs[j:] -- (Possibly) over-application
+
+/--
+Are all fixed parameters a non-reordered prefix?
+-/
+def FixedParamPerms.fixedArePrefix (fixedParamPerms : FixedParamPerms) : Bool :=
+  fixedParamPerms.perms.all fun paramInfos =>
+    paramInfos ==
+      (Array.range fixedParamPerms.numFixed).map Option.some ++
+      mkArray (paramInfos.size - fixedParamPerms.numFixed) .none
+
+/--
+If `xs` are the fixed parameters that are in scope, and `toErase` are, for each function, the
+positions of arguments that must no longer be fixed parameters, then this function splits partitions
+`xs` into those to keep and those to erase, and updates `FixedParams` accordingly.
+
+This is used in structural recursion, where we may discover that some fixed parameters are actually
+indices and need to be treated as varying, including all parameters that depend on them.
+-/
+def FixedParamPerms.erase  (fixedParamPerms : FixedParamPerms) (xs : Array Expr)
+    (toErase : Array (Array Nat)) : (FixedParamPerms × Array Expr × Array FVarId) := Id.run do
+  assert! xs.all (·.isFVar)
+  assert! fixedParamPerms.numFixed  = xs.size
+  assert! toErase.size = fixedParamPerms.perms.size
+  -- Calculate a mask on the fixed parameters of variables to erase
+  let mut mask := mkArray fixedParamPerms.numFixed false
+  for funIdx in [:toErase.size], paramIdxs in toErase, mapping in fixedParamPerms.perms do
+    for paramIdx in paramIdxs do
+      assert! paramIdx < mapping.size
+      if let some fixedParamIdx := mapping[paramIdx]! then
+        mask := mask.set! fixedParamIdx true
+  -- Take the transitive closure under under `fixedParamPerms.revDeps`.
+  let mut changed := true
+  while changed do
+    changed := false
+    for h : funIdx in [:fixedParamPerms.perms.size] do
+      for h : paramIdx₁ in [:fixedParamPerms.perms[funIdx].size] do
+        if let some fixedParamIdx₁ := fixedParamPerms.perms[funIdx][paramIdx₁] then
+          if mask[fixedParamIdx₁]! then
+            for paramIdx₂ in fixedParamPerms.revDeps[funIdx]![paramIdx₁]! do
+              if let some fixedParamIdx₂ := fixedParamPerms.perms[funIdx][paramIdx₂]! then
+                if !mask[fixedParamIdx₂]! then
+                  mask := mask.set! fixedParamIdx₂ true
+                  changed := true
+  -- Calculate reindexing map, variables to keep, variables to erase
+  let mut reindex := #[]
+  let mut fvarsToErase :=#[]
+  let mut toKeep :=#[]
+  for i in [:mask.size], erase in mask, x in xs do
+    if erase then
+      reindex := reindex.push none
+      fvarsToErase := fvarsToErase.push x.fvarId!
+    else
+      reindex := reindex.push (Option.some toKeep.size)
+      toKeep := toKeep.push x
+  let fixedParamPerms' : FixedParamPerms := {
+    numFixed := toKeep.size
+    perms := fixedParamPerms.perms.map (·.map (·.bind (reindex[·]!)))
+    revDeps := fixedParamPerms.revDeps
+  }
+  return (fixedParamPerms', toKeep, fvarsToErase)
+
+end Lean.Elab
+
+builtin_initialize
+  Lean.registerTraceClass `Elab.definition.fixedParams

src/Lean/Elab/PreDefinition/Mutual.lean

@@ -26,24 +26,6 @@ where
       withLocalDecl vals[0]!.bindingName! vals[0]!.binderInfo vals[0]!.bindingDomain! fun x =>
         go (fvars.push x) (vals.map fun val => val.bindingBody!.instantiate1 x)
 
-def getFixedPrefix (preDefs : Array PreDefinition) : MetaM Nat :=
-  withCommonTelescope preDefs fun xs vals => do
-    let resultRef ← IO.mkRef xs.size
-    for val in vals do
-      if (← resultRef.get) == 0 then return 0
-      forEachExpr' val fun e => do
-        if preDefs.any fun preDef => e.isAppOf preDef.declName then
-          let args := e.getAppArgs
-          resultRef.modify (min args.size ·)
-          for arg in args, x in xs do
-            if !(← withoutProofIrrelevance <| withReducible <| isDefEq arg x) then
-              -- We continue searching if e's arguments are not a prefix of `xs`
-              return true
-          return false
-        else
-          return true
-    resultRef.get
-
 def addPreDefsFromUnary (preDefs : Array PreDefinition) (preDefsNonrec : Array PreDefinition)
     (unaryPreDefNonRec : PreDefinition) : TermElabM Unit := do
   /-

src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean

@@ -9,6 +9,7 @@ import Lean.Meta.Tactic.Rewrite
 import Lean.Meta.Tactic.Split
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Eqns
+import Lean.Elab.PreDefinition.FixedParams
 import Lean.Meta.ArgsPacker.Basic
 import Init.Data.Array.Basic
 import Init.Internal.Order.Basic
@@ -20,12 +21,13 @@ open Eqns
 structure EqnInfo extends EqnInfoCore where
   declNames       : Array Name
   declNameNonRec  : Name
-  fixedPrefixSize : Nat
+  fixedParamPerms : FixedParamPerms
   deriving Inhabited
 
 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
-def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat) : MetaM Unit := do
+def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name)
+    (fixedParamPerms : FixedParamPerms) : MetaM Unit := do
   preDefs.forM fun preDef => ensureEqnReservedNamesAvailable preDef.declName
   unless preDefs.all fun p => p.kind.isTheorem do
     unless (← preDefs.allM fun p => isProp p.type) do
@@ -33,7 +35,7 @@ def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fi
       modifyEnv fun env =>
         preDefs.foldl (init := env) fun env preDef =>
           eqnInfoExt.insert env preDef.declName { preDef with
-            declNames, declNameNonRec, fixedPrefixSize }
+            declNames, declNameNonRec, fixedParamPerms }
 
 private def deltaLHSUntilFix (declName declNameNonRec : Name) (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
   let target ← mvarId.getType'

src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean

@@ -70,21 +70,21 @@ def deriveInduction (name : Name) : MetaM Unit := do
 
     let infos ← eqnInfo.declNames.mapM getConstInfoDefn
     -- First open up the fixed parameters everywhere
-    let e' ← lambdaBoundedTelescope infos[0]!.value eqnInfo.fixedPrefixSize fun xs _ => do
+    let e' ← eqnInfo.fixedParamPerms.perms[0]!.forallTelescope infos[0]!.type fun xs => do
       -- Now look at the body of an arbitrary of the functions (they are essentially the same
       -- up to the final projections)
-      let body ← instantiateLambda infos[0]!.value xs
+      let body ← eqnInfo.fixedParamPerms.perms[0]!.instantiateLambda infos[0]!.value xs
 
       -- The body should now be of the form of the form (fix … ).2.2.1
       -- We strip the projections (if present)
-      let body' := PProdN.stripProjs body
+      let body' := PProdN.stripProjs body.eta -- TODO: Eta more carefully?
       let some fixApp ← whnfUntil body' ``fix
-        | throwError "Unexpected function body {body}"
+        | throwError "Unexpected function body {body}, could not whnfUntil fix"
       let_expr fix α instCCPOα F hmono := fixApp
-        | throwError "Unexpected function body {body'}"
+        | throwError "Unexpected function body {body'}, not an application of fix"
 
       let instCCPOs := CCPOProdProjs infos.size instCCPOα
-      let types ← infos.mapM (instantiateForall ·.type xs)
+      let types ← infos.mapIdxM (eqnInfo.fixedParamPerms.perms[·]!.instantiateForall ·.type xs)
       let packedType ← PProdN.pack 0 types
       let motiveTypes ← types.mapM (mkArrow · (.sort 0))
       let motiveNames := numberNames motiveTypes.size "motive"
@@ -135,7 +135,11 @@ def deriveInduction (name : Name) : MetaM Unit := do
             let packedConclusion ← PProdN.pack 0 <| ←
               motives.mapIdxM fun i motive => do
                 let f ← mkConstWithLevelParams infos[i]!.name
-                return mkApp motive (mkAppN f xs)
+                let fEtaExpanded ← lambdaTelescope infos[i]!.value fun ys _ =>
+                  mkLambdaFVars ys (mkAppN f ys)
+                let fInst ← eqnInfo.fixedParamPerms.perms[i]!.instantiateLambda fEtaExpanded xs
+                let fInst := fInst.eta
+                return mkApp motive fInst
             let e' ← mkExpectedTypeHint e' packedConclusion
             let e' ← mkLambdaFVars hs e'
             let e' ← mkLambdaFVars adms e'
@@ -228,9 +232,10 @@ def derivePartialCorrectness (name : Name) : MetaM Unit := do
       throwError "{name} is not defined by partial_fixpoint"
 
     let infos ← eqnInfo.declNames.mapM getConstInfoDefn
+    let fixedParamPerm0 := eqnInfo.fixedParamPerms.perms[0]!
     -- First open up the fixed parameters everywhere
-    let e' ← lambdaBoundedTelescope infos[0]!.value eqnInfo.fixedPrefixSize fun xs _ => do
-      let types ← infos.mapM (instantiateForall ·.type xs)
+    let e' ← fixedParamPerm0.forallTelescope infos[0]!.type fun xs => do
+      let types ← infos.mapIdxM (eqnInfo.fixedParamPerms.perms[·]!.instantiateForall ·.type xs)
 
       -- for `f : α → β → Option γ`, we expect a `motive : α → β → γ → Prop`
       let motiveTypes ← types.mapM fun type =>

src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean

@@ -18,33 +18,44 @@ open Monotonicity
 
 open Lean.Order
 
-private def replaceRecApps (recFnNames : Array Name) (fixedPrefixSize : Nat) (f : Expr) (e : Expr) : MetaM Expr := do
+private def replaceRecApps (recFnNames : Array Name) (fixedParamPerms : FixedParamPerms) (f : Expr) (e : Expr) : MetaM Expr := do
+  assert! recFnNames.size = fixedParamPerms.perms.size
   let t ← inferType f
-  return e.replace fun e =>
-    if let some idx := recFnNames.findIdx? (e.isAppOfArity · fixedPrefixSize) then
-      some <| PProdN.proj recFnNames.size idx t f
-    else
-      none
+  return e.replace fun e => do
+    let fn := e.getAppFn
+    guard fn.isConst
+    let idx ← recFnNames.idxOf? fn.constName!
+    let args := e.getAppArgs
+    let varying := fixedParamPerms.perms[idx]!.pickVarying args
+    return mkAppN (PProdN.proj recFnNames.size idx t f) varying
 
 /--
 For pretty error messages:
 Takes `F : (fun f => e)`, where `f` is the packed function, and replaces `f` in `e` with the user-visible
 constants, which are added to the environment temporarily.
 -/
-private def unReplaceRecApps {α} (preDefs : Array PreDefinition) (fixedArgs : Array Expr)
+private def unReplaceRecApps {α} (preDefs : Array PreDefinition) (fixedParamPerms : FixedParamPerms) (fixedArgs : Array Expr)
     (F : Expr) (k : Expr → MetaM α) : MetaM α := do
   unless F.isLambda do throwError "Expected lambda:{indentExpr F}"
   withoutModifyingEnv do
     preDefs.forM addAsAxiom
-    let fns := preDefs.map fun d =>
-      mkAppN (.const d.declName (d.levelParams.map mkLevelParam)) fixedArgs
+    let fns ← preDefs.mapIdxM fun funIdx preDef => do
+      let value ← fixedParamPerms.perms[funIdx]!.instantiateLambda preDef.value fixedArgs
+      lambdaTelescope value fun xs _ =>
+        let args := fixedParamPerms.perms[funIdx]!.buildArgs fixedArgs xs
+        let call := mkAppN (.const preDef.declName (preDef.levelParams.map mkLevelParam)) args
+        mkLambdaFVars (etaReduce := true) xs call
     let packedFn ← PProdN.mk 0 fns
     let e ← lambdaBoundedTelescope F 1 fun f e => do
       let f := f[0]!
       -- Replace f with calls to the constants
-      let e := e.replace fun e => do if e == f then return packedFn else none
-      -- And reduce projection redexes
+      let e := e.replace fun e => do
+        if e == f then return packedFn else none
+      -- And reduce projection and beta redexes
+      -- (This is a bit blunt; we could try harder to only replace the projection and beta-redexes
+      -- introduced above)
       let e ← PProdN.reduceProjs e
+      let e ← Core.betaReduce e
       pure e
     k e
 
@@ -81,15 +92,12 @@ def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do
           mkAppOptM ``FlatOrder.instCCPO #[none, classicalWitness]
       mkLambdaFVars xs inst
 
-  let fixedPrefixSize ← Mutual.getFixedPrefix preDefs
-  trace[Elab.definition.partialFixpoint] "fixed prefix size: {fixedPrefixSize}"
-
   let declNames := preDefs.map (·.declName)
-
-  forallBoundedTelescope preDefs[0]!.type fixedPrefixSize fun fixedArgs _ => do
+  let fixedParamPerms ← getFixedParamPerms preDefs
+  fixedParamPerms.perms[0]!.forallTelescope preDefs[0]!.type fun fixedArgs => do
     -- ∀ x y, CCPO (rᵢ x y)
-    let ccpoInsts := ccpoInsts.map (·.beta fixedArgs)
-    let types ← preDefs.mapM (instantiateForall ·.type fixedArgs)
+    let ccpoInsts ← ccpoInsts.mapIdxM (fixedParamPerms.perms[·]!.instantiateLambda · fixedArgs)
+    let types ← preDefs.mapIdxM (fixedParamPerms.perms[·]!.instantiateForall ·.type fixedArgs)
 
     -- (∀ x y, r₁ x y) ×' (∀ x y, r₂ x y)
     let packedType ← PProdN.pack 0 types
@@ -108,7 +116,7 @@ def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do
 
     -- Error reporting hook, presenting monotonicity errors in terms of recursive functions
     let failK {α} f (monoThms : Array Name) : MetaM α := do
-      unReplaceRecApps preDefs fixedArgs f fun t => do
+      unReplaceRecApps preDefs fixedParamPerms fixedArgs f fun t => do
         let extraMsg := if monoThms.isEmpty then m!"" else
           m!"Tried to apply {.andList (monoThms.toList.map (m!"'{.ofConstName ·}'"))}, but failed.\n\
              Possible cause: A missing `{.ofConstName ``MonoBind}` instance.\n\
@@ -122,13 +130,13 @@ def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do
 
     -- Adjust the body of each function to take the other functions as a
     -- (packed) parameter
-    let Fs ← preDefs.mapM fun preDef => do
-      let body ← instantiateLambda preDef.value fixedArgs
+    let Fs ← preDefs.mapIdxM fun funIdx preDef => do
+      let body ← fixedParamPerms.perms[funIdx]!.instantiateLambda preDef.value fixedArgs
       withLocalDeclD (← mkFreshUserName `f) packedType fun f => do
         let body' ← withoutModifyingEnv do
           -- replaceRecApps needs the constants in the env to typecheck things
           preDefs.forM (addAsAxiom ·)
-          replaceRecApps declNames fixedPrefixSize f body
+          replaceRecApps declNames fixedParamPerms f body
         mkLambdaFVars #[f] body'
 
     -- Construct and solve monotonicity goals for each function separately
@@ -160,7 +168,7 @@ def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do
     trace[Elab.definition.partialFixpoint] "packedValue: {packedValue}"
 
     let declName :=
-      if preDefs.size = 1 then
+      if preDefs.size = 1 && fixedParamPerms.fixedArePrefix then
         preDefs[0]!.declName
       else
         preDefs[0]!.declName ++ `mutual
@@ -170,17 +178,22 @@ def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do
       declName := declName
       type := packedType'
       value := packedValue'}
+
     let preDefsNonrec ← preDefs.mapIdxM fun fidx preDef => do
-      let us := preDefNonRec.levelParams.map mkLevelParam
-      let value := mkConst preDefNonRec.declName us
-      let value := mkAppN value fixedArgs
-      let value := PProdN.proj preDefs.size fidx packedType value
-      let value ← mkLambdaFVars fixedArgs value
-      pure { preDef with value }
+      forallBoundedTelescope preDef.type fixedParamPerms.perms[fidx]!.size fun params _ => do
+        let fixed := fixedParamPerms.perms[fidx]!.pickFixed params
+        let varying := fixedParamPerms.perms[fidx]!.pickVarying params
+        let us := preDefNonRec.levelParams.map mkLevelParam
+        let value := mkConst preDefNonRec.declName us
+        let value := mkAppN value fixed
+        let value := PProdN.proj preDefs.size fidx packedType value
+        let value := mkAppN value varying
+        let value ← mkLambdaFVars (etaReduce := true) params value
+        pure { preDef with value }
 
     Mutual.addPreDefsFromUnary preDefs preDefsNonrec preDefNonRec
     let preDefs ← Mutual.cleanPreDefs preDefs
-    PartialFixpoint.registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize
+    PartialFixpoint.registerEqnsInfo preDefs preDefNonRec.declName fixedParamPerms
     Mutual.addPreDefAttributes preDefs
 
 end Lean.Elab

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

@@ -155,7 +155,8 @@ private partial def replaceRecApps (recArgInfos : Array RecArgInfo) (positions :
               try toBelow below recArgInfo.indGroupInst.params.size positions fnIdx recArg
               catch _ => throwError "failed to eliminate recursive application{indentExpr e}"
             -- We don't pass the fixed parameters, the indices and the major arg to `f`, only the rest
-            let (_, fArgs) := recArgInfo.pickIndicesMajor args[recArgInfo.numFixed:]
+            let ys := recArgInfo.fixedParamPerm.pickVarying args
+            let (_, fArgs) := recArgInfo.pickIndicesMajor ys
             let fArgs ← fArgs.mapM (replaceRecApps recArgInfos positions below ·)
             return mkAppN f fArgs
           else

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

@@ -10,6 +10,7 @@ import Lean.Meta.Tactic.Simp.Main
 import Lean.Meta.Tactic.Apply
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Eqns
+import Lean.Elab.PreDefinition.FixedParams
 import Lean.Elab.PreDefinition.Structural.Basic
 
 namespace Lean.Elab
@@ -21,7 +22,7 @@ namespace Structural
 structure EqnInfo extends EqnInfoCore where
   recArgPos : Nat
   declNames : Array Name
-  numFixed  : Nat
+  fixedParamPerms : FixedParamPerms
   deriving Inhabited
 
 private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
@@ -85,10 +86,10 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
 def registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (recArgPos : Nat)
-    (numFixed : Nat) : CoreM Unit := do
+    (fixedParamPerms : FixedParamPerms) : CoreM Unit := do
   ensureEqnReservedNamesAvailable preDef.declName
   modifyEnv fun env => eqnInfoExt.insert env preDef.declName
-    { preDef with recArgPos, declNames, numFixed }
+    { preDef with recArgPos, declNames, fixedParamPerms }
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if let some info := eqnInfoExt.find? (← getEnv) declName then

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

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Joachim Breitner
 -/
 prelude
 import Lean.Elab.PreDefinition.TerminationMeasure
+import Lean.Elab.PreDefinition.FixedParams
 import Lean.Elab.PreDefinition.Structural.Basic
 import Lean.Elab.PreDefinition.Structural.RecArgInfo
 
@@ -58,9 +59,10 @@ private def hasBadParamDep? (ys : Array Expr) (indParams : Array Expr) : MetaM (
 Assemble the `RecArgInfo` for the `i`th parameter in the parameter list `xs`. This performs
 various sanity checks on the parameter (is it even of inductive type etc).
 -/
-def getRecArgInfo (fnName : Name) (numFixed : Nat) (xs : Array Expr) (i : Nat) : MetaM RecArgInfo := do
+def getRecArgInfo (fnName : Name) (fixedParamPerm : FixedParamPerm) (xs : Array Expr) (i : Nat) : MetaM RecArgInfo := do
+  assert! fixedParamPerm.size = xs.size
   if h : i < xs.size then
-    if i < numFixed then
+    if fixedParamPerm.isFixed i then
       throwError "it is unchanged in the recursive calls"
     let x := xs[i]
     let localDecl ← getFVarLocalDecl x
@@ -79,16 +81,14 @@ def getRecArgInfo (fnName : Name) (numFixed : Nat) (xs : Array Expr) (i : Nat) :
       else if !indIndices.allDiff then
         throwError "its type {indInfo.name} is an inductive family and indices are not pairwise distinct{indentExpr xType}"
       else
-        let indexMinPos := getIndexMinPos xs indIndices
-        let numFixed    := if indexMinPos < numFixed then indexMinPos else numFixed
-        let ys          := xs[numFixed:]
+        let ys := fixedParamPerm.pickVarying xs
         match (← hasBadIndexDep? ys indIndices) with
         | some (index, y) =>
           throwError "its type {indInfo.name} is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}"
         | none =>
           match (← hasBadParamDep? ys indParams) with
           | some (indParam, y) =>
-            throwError "its type is an inductive datatype{indentExpr xType}\nand the datatype parameter{indentExpr indParam}\ndepends on the function parameter{indentExpr y}\nwhich does not come before the varying parameters and before the indices of the recursion parameter."
+            throwError "its type is an inductive datatype{indentExpr xType}\nand the datatype parameter{indentExpr indParam}\ndepends on the function parameter{indentExpr y}\nwhich is not fixed."
           | none =>
             let indAll := indInfo.all.toArray
             let .some indIdx := indAll.idxOf? indInfo.name | panic! "{indInfo.name} not in {indInfo.all}"
@@ -98,7 +98,7 @@ def getRecArgInfo (fnName : Name) (numFixed : Nat) (xs : Array Expr) (i : Nat) :
               levels := us
               params := indParams }
             return { fnName       := fnName
-                     numFixed     := numFixed
+                     fixedParamPerm := fixedParamPerm
                      recArgPos    := i
                      indicesPos   := indicesPos
                      indGroupInst := indGroupInst
@@ -115,25 +115,27 @@ The `xs` are the fixed parameters, `value` the body with the fixed prefix instan
 Takes the optional user annotation into account (`termMeasure?`). If this is given and the measure
 is unsuitable, throw an error.
 -/
-def getRecArgInfos (fnName : Name) (xs : Array Expr) (value : Expr)
-    (termMeasure? : Option TerminationMeasure) : MetaM (Array RecArgInfo × MessageData) := do
+def getRecArgInfos (fnName : Name) (fixedParamPerm : FixedParamPerm) (xs : Array Expr)
+    (value : Expr) (termMeasure? : Option TerminationMeasure) : MetaM (Array RecArgInfo × MessageData) := do
   lambdaTelescope value fun ys _ => do
     if let .some termMeasure := termMeasure? then
       -- User explicitly asked to use a certain measure, so throw errors eagerly
       let recArgInfo ← withRef termMeasure.ref do
         mapError (f := (m!"cannot use specified measure for structural recursion:{indentD ·}")) do
-          getRecArgInfo fnName xs.size (xs ++ ys) (← termMeasure.structuralArg)
+          let args := fixedParamPerm.buildArgs xs ys
+          getRecArgInfo fnName fixedParamPerm args (← termMeasure.structuralArg)
       return (#[recArgInfo], m!"")
     else
+      let args := fixedParamPerm.buildArgs xs ys
       let mut recArgInfos := #[]
       let mut report : MessageData := m!""
       -- No `termination_by`, so try all, and remember the errors
-      for idx in [:xs.size + ys.size] do
+      for idx in [:args.size] do
         try
-          let recArgInfo ← getRecArgInfo fnName xs.size (xs ++ ys) idx
+          let recArgInfo ← getRecArgInfo fnName fixedParamPerm args idx
           recArgInfos := recArgInfos.push recArgInfo
         catch e =>
-          report := report ++ (m!"Not considering parameter {← prettyParam (xs ++ ys) idx} of {fnName}:" ++
+          report := report ++ (m!"Not considering parameter {← prettyParam args idx} of {fnName}:" ++
             indentD e.toMessageData) ++ "\n"
       trace[Elab.definition.structural] "getRecArgInfos report: {report}"
       return (recArgInfos, report)
@@ -211,7 +213,7 @@ def argsInGroup (group : IndGroupInst) (xs : Array Expr) (value : Expr)
           let indicesPos := indIndices.map fun index => match (xs++ys).idxOf? index with | some i => i | none => unreachable!
           return .some
             { fnName       := recArgInfo.fnName
-              numFixed     := recArgInfo.numFixed
+              fixedParamPerm  := recArgInfo.fixedParamPerm
               recArgPos    := recArgInfo.recArgPos
               indicesPos   := indicesPos
               indGroupInst := group
@@ -232,13 +234,13 @@ def allCombinations (xss : Array (Array α)) : Option (Array (Array α)) :=
     some (go 0 #[])
 
 
-def tryAllArgs (fnNames : Array Name) (xs : Array Expr) (values : Array Expr)
-   (termMeasure?s : Array (Option TerminationMeasure)) (k : Array RecArgInfo → M α) : M α := do
+def tryAllArgs (fnNames : Array Name) (fixedParamPerms : FixedParamPerms) (xs : Array Expr)
+   (values : Array Expr) (termMeasure?s : Array (Option TerminationMeasure)) (k : Array RecArgInfo → M α) : M α := do
   let mut report := m!""
   -- Gather information on all possible recursive arguments
   let mut recArgInfoss := #[]
-  for fnName in fnNames, value in values, termMeasure? in termMeasure?s do
-    let (recArgInfos, thisReport) ← getRecArgInfos fnName xs value termMeasure?
+  for fnName in fnNames, value in values, termMeasure? in termMeasure?s, fixedParamPerm in fixedParamPerms.perms do
+    let (recArgInfos, thisReport) ← getRecArgInfos fnName fixedParamPerm xs value termMeasure?
     report := report ++ thisReport
     recArgInfoss := recArgInfoss.push recArgInfos
   -- Put non-indices first
@@ -266,8 +268,6 @@ def tryAllArgs (fnNames : Array Name) (xs : Array Expr) (values : Array Expr)
           -- are ok in a nested group. This logic can maybe simplified)
           unless (← hasConst (group.brecOnName false 0)) do
             throwError "the type {group} does not have a `.brecOn` recursor"
-          -- TODO: Here we used to save and restore the state. But should the `try`-`catch`
-          -- not suffice?
           let r ← k comb
           trace[Elab.definition.structural] "tryAllArgs report:\n{report}"
           return r

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

@@ -12,23 +12,24 @@ import Lean.Elab.PreDefinition.Structural.RecArgInfo
 namespace Lean.Elab.Structural
 open Meta
 
-private def replaceIndPredRecApp (numFixed : Nat) (funType : Expr) (e : Expr) : M Expr := do
+private def replaceIndPredRecApp (fixedParamPerm : FixedParamPerm) (funType : Expr) (e : Expr) : M Expr := do
   withoutProofIrrelevance do
   withTraceNode `Elab.definition.structural (fun _ => pure m!"eliminating recursive call {e}") do
     -- We want to replace `e` with an expression of the same type
     let main ← mkFreshExprSyntheticOpaqueMVar (← inferType e)
-    let args : Array Expr := e.getAppArgs[numFixed:]
+    let args : Array Expr := e.getAppArgs
+    let ys := fixedParamPerm.pickVarying args
     let lctx ← getLCtx
     let r ← lctx.anyM fun localDecl => do
       if localDecl.isAuxDecl then return false
       let (mvars, _, t) ← forallMetaTelescope localDecl.type -- NB: do not reduce, we want to see the `funType`
       unless t.getAppFn == funType do return false
       withTraceNodeBefore `Elab.definition.structural (do pure m!"trying {mkFVar localDecl.fvarId} : {localDecl.type}") do
-        if args.size < t.getAppNumArgs then
-          trace[Elab.definition.structural] "too few arguments. Underapplied recursive call?"
+        if ys.size < t.getAppNumArgs then
+          trace[Elab.definition.structural] "too few arguments, expected {t.getAppNumArgs}, found {ys.size}. Underapplied recursive call?"
           return false
-        if (← (t.getAppArgs.zip args).allM (fun (t,s) => isDefEq t s)) then
-          main.mvarId!.assign (mkAppN (mkAppN localDecl.toExpr mvars) args[t.getAppNumArgs:])
+        if (← (t.getAppArgs.zip ys).allM (fun (t,s) => isDefEq t s)) then
+          main.mvarId!.assign (mkAppN (mkAppN localDecl.toExpr mvars) ys[t.getAppNumArgs:])
           return ← mvars.allM fun v => do
             unless (← v.mvarId!.isAssigned) do
               trace[Elab.definition.structural] "Cannot use {mkFVar localDecl.fvarId}: parameter {v} remains unassigned"
@@ -62,7 +63,7 @@ private partial def replaceIndPredRecApps (recArgInfo : RecArgInfo) (funType : E
       let processApp (e : Expr) : M Expr := do
         e.withApp fun f args => do
           if f.isConstOf recArgInfo.fnName then
-            replaceIndPredRecApp recArgInfo.numFixed funType e
+            replaceIndPredRecApp recArgInfo.fixedParamPerm funType e
           else
             return mkAppN (← loop f) (← args.mapM loop)
       match (← matchMatcherApp? e) with
@@ -100,7 +101,7 @@ def mkIndPredBRecOn (recArgInfo : RecArgInfo) (value : Expr) : M Expr := do
   lambdaTelescope value fun ys value => do
     let type  := (← inferType value).headBeta
     let (indexMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor ys
-    trace[Elab.definition.structural] "numFixed: {recArgInfo.numFixed}, indexMajorArgs: {indexMajorArgs}, otherArgs: {otherArgs}"
+    trace[Elab.definition.structural] "indexMajorArgs: {indexMajorArgs}, otherArgs: {otherArgs}"
     let funType ← mkLambdaFVars ys type
     withLetDecl `funType (← inferType funType) funType fun funType => do
       let motive ← mkForallFVars otherArgs (mkAppN funType ys)

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

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Joachim Breitner
 -/
 prelude
 import Lean.Elab.PreDefinition.TerminationMeasure
+import Lean.Elab.PreDefinition.Mutual
 import Lean.Elab.PreDefinition.Structural.Basic
 import Lean.Elab.PreDefinition.Structural.FindRecArg
 import Lean.Elab.PreDefinition.Structural.Preprocess
@@ -71,27 +72,9 @@ where
       withLocalDecl vals[0]!.bindingName! vals[0]!.binderInfo vals[0]!.bindingDomain! fun x =>
         go (fvars.push x) (vals.map fun val => val.bindingBody!.instantiate1 x)
 
-def getMutualFixedPrefix (preDefs : Array PreDefinition) : M Nat :=
-  withCommonTelescope preDefs fun xs vals => do
-    let resultRef ← IO.mkRef xs.size
-    for val in vals do
-      if (← resultRef.get) == 0 then return 0
-      forEachExpr' val fun e => do
-        if preDefs.any fun preDef => e.isAppOf preDef.declName then
-          let args := e.getAppArgs
-          resultRef.modify (min args.size ·)
-          for arg in args, x in xs do
-            if !(← withoutProofIrrelevance <| withReducible <| isDefEq arg x) then
-              -- We continue searching if e's arguments are not a prefix of `xs`
-              return true
-          return false
-        else
-          return true
-    resultRef.get
-
-private def elimMutualRecursion (preDefs : Array PreDefinition) (xs : Array Expr)
-    (recArgInfos : Array RecArgInfo) : M (Array PreDefinition) := do
-  let values ← preDefs.mapM (instantiateLambda ·.value xs)
+private def elimMutualRecursion (preDefs : Array PreDefinition) (fixedParamPerms : FixedParamPerms)
+    (xs : Array Expr) (recArgInfos : Array RecArgInfo) : M (Array PreDefinition) := do
+  let values ← preDefs.mapIdxM (fixedParamPerms.perms[·]!.instantiateLambda ·.value xs)
   let indInfo ← getConstInfoInduct recArgInfos[0]!.indGroupInst.all[0]!
   if ← isInductivePredicate indInfo.name then
     -- Here we branch off to the IndPred construction, but only for non-mutual functions
@@ -102,7 +85,8 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (xs : Array Expr
     let recArgInfo := recArgInfos[0]!
     let value := values[0]!
     let valueNew ← mkIndPredBRecOn recArgInfo value
-    let valueNew ← mkLambdaFVars xs valueNew
+    let valueNew ← lambdaTelescope value fun ys _ => do
+      mkLambdaFVars (etaReduce := true) (fixedParamPerms.perms[0]!.buildArgs xs ys) (mkAppN valueNew ys)
     trace[Elab.definition.structural] "Nonrecursive value:{indentExpr valueNew}"
     check valueNew
     return #[{ preDef with value := valueNew }]
@@ -123,12 +107,16 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (xs : Array Expr
   -- Assemble the individual `.brecOn` applications
   let valuesNew ← (Array.zip recArgInfos values).mapIdxM fun i (r, v) =>
     mkBrecOnApp positions i brecOnConst FArgs r v
-  -- Abstract over the fixed prefixed
-  let valuesNew ← valuesNew.mapM (mkLambdaFVars xs ·)
+  -- Abstract over the fixed prefixed, preserving the original parameter order
+  let valuesNew ← (values.zip valuesNew).mapIdxM fun i ⟨value, valueNew⟩ =>
+    lambdaTelescope value fun ys _ => do
+      -- NB: Do not eta-contract here, other code (e.g. FunInd) expects this to have the
+      -- same number of head lambdas as the original definition
+      mkLambdaFVars (fixedParamPerms.perms[i]!.buildArgs xs ys) (valueNew.beta ys)
   return (Array.zip preDefs valuesNew).map fun ⟨preDef, valueNew⟩ => { preDef with value := valueNew }
 
 private def inferRecArgPos (preDefs : Array PreDefinition) (termMeasure?s : Array (Option TerminationMeasure)) :
-    M (Array Nat × (Array PreDefinition) × Nat) := do
+    M (Array Nat × (Array PreDefinition) × FixedParamPerms) := do
   withoutModifyingEnv do
     preDefs.forM (addAsAxiom ·)
     let fnNames := preDefs.map (·.declName)
@@ -136,25 +124,39 @@ private def inferRecArgPos (preDefs : Array PreDefinition) (termMeasure?s : Arra
       return { preDef with value := (← preprocess preDef.value fnNames) }
 
     -- The syntactically fixed arguments
-    let maxNumFixed ← getMutualFixedPrefix preDefs
+    let fixedParamPerms ← getFixedParamPerms preDefs
 
-    lambdaBoundedTelescope preDefs[0]!.value maxNumFixed fun xs _ => do
-      assert! xs.size = maxNumFixed
-      let values ← preDefs.mapM (instantiateLambda ·.value xs)
+    fixedParamPerms.perms[0]!.forallTelescope preDefs[0]!.type fun xs => do
+      let values ← preDefs.mapIdxM (fixedParamPerms.perms[·]!.instantiateLambda ·.value xs)
 
-      tryAllArgs fnNames xs values termMeasure?s fun recArgInfos => do
+      tryAllArgs fnNames fixedParamPerms xs values termMeasure?s fun recArgInfos => do
         let recArgPoss := recArgInfos.map (·.recArgPos)
         trace[Elab.definition.structural] "Trying argument set {recArgPoss}"
-        let numFixed := recArgInfos.foldl (·.min ·.numFixed) maxNumFixed
-        if numFixed < maxNumFixed then
-          trace[Elab.definition.structural] "Reduced numFixed from {maxNumFixed} to {numFixed}"
-        -- We may have decreased the number of arguments we consider fixed, so update
-        -- the recArgInfos, remove the extra arguments from local environment, and recalculate value
-        let recArgInfos := recArgInfos.map ({· with numFixed := numFixed })
-        withErasedFVars (xs.extract numFixed xs.size |>.map (·.fvarId!)) do
-          let xs := xs[:numFixed]
-          let preDefs' ← elimMutualRecursion preDefs xs recArgInfos
-          return (recArgPoss, preDefs', numFixed)
+        let (fixedParamPerms', xs', toErase) := fixedParamPerms.erase xs (recArgInfos.map (·.indicesAndRecArgPos))
+        -- We may have to turn some fixed parameters into varying parameters
+        let recArgInfos := recArgInfos.mapIdx fun i recArgInfo =>
+          {recArgInfo with fixedParamPerm := fixedParamPerms'.perms[i]!}
+        if xs'.size != xs.size then
+          trace[Elab.definition.structural] "Reduced fixed params from {xs} to {xs'}, erasing {toErase.map mkFVar}"
+          trace[Elab.definition.structural] "New recArgInfos {repr recArgInfos}"
+        -- Check that the parameters of the IndGroupInsts are still fine
+          for recArgInfo in recArgInfos do
+            for indParam in recArgInfo.indGroupInst.params do
+              for y in toErase do
+                if (← dependsOn indParam y) then
+                  if indParam.isFVarOf y then
+                    throwError "its type is an inductive datatype and the datatype parameter\
+                      {indentExpr indParam}\n\
+                      which cannot be fixed as it is an index or depends on an index, and indices \
+                      cannot be fixed parameters when using structural recursion."
+                  else
+                    throwError "its type is an inductive datatype and the datatype parameter\
+                      {indentExpr indParam}\ndepends on the function parameter{indentExpr (mkFVar y)}\n\
+                      which cannot be fixed as it is an index or depends on an index, and indices \
+                      cannot be fixed parameters when using structural recursion."
+        withErasedFVars toErase do
+          let preDefs' ← elimMutualRecursion preDefs fixedParamPerms' xs' recArgInfos
+          return (recArgPoss, preDefs', fixedParamPerms')
 
 def reporttermMeasure (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit := do
   if let some ref := preDef.termination.terminationBy?? then
@@ -167,7 +169,7 @@ def reporttermMeasure (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit :=
 
 def structuralRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option TerminationMeasure)) : TermElabM Unit := do
   let names := preDefs.map (·.declName)
-  let ((recArgPoss, preDefsNonRec, numFixed), state) ← run <| inferRecArgPos preDefs termMeasure?s
+  let ((recArgPoss, preDefsNonRec, fixedParamPerms), state) ← run <| inferRecArgPos preDefs termMeasure?s
   for recArgPos in recArgPoss, preDef in preDefs do
     reporttermMeasure preDef recArgPos
   state.addMatchers.forM liftM
@@ -190,7 +192,7 @@ def structuralRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (
         for theorems and definitions that are propositions.
         See issue #2327
         -/
-        registerEqnsInfo preDef (preDefs.map (·.declName)) recArgPos numFixed
+        registerEqnsInfo preDef (preDefs.map (·.declName)) recArgPos fixedParamPerms
     addSmartUnfoldingDef preDef recArgPos
     markAsRecursive preDef.declName
   for preDef in preDefs do

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

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Joachim Breitner
 prelude
 import Lean.Meta.Basic
 import Lean.Meta.ForEachExpr
+import Lean.Elab.PreDefinition.FixedParams
 import Lean.Elab.PreDefinition.Structural.IndGroupInfo
 
 namespace Lean.Elab.Structural
@@ -14,18 +15,18 @@ namespace Lean.Elab.Structural
 /--
 Information about the argument of interest of a structurally recursive function.
 
-The `Expr`s in this data structure expect the `fixedParams` to be in scope, but not the other
+The `Expr`s in this data structure expect the fixed parameters to be in scope, but not the other
 parameters of the function. This ensures that this data structure makes sense in the other functions
 of a mutually recursive group.
 -/
 structure RecArgInfo where
   /-- the name of the recursive function -/
   fnName       : Name
-  /-- the fixed prefix of arguments of the function we are trying to justify termination using structural recursion. -/
-  numFixed     : Nat
-  /-- position (counted including fixed prefix) of the argument we are recursing on -/
+  /-- Information which arguments are fixed -/
+  fixedParamPerm : FixedParamPerm
+  /-- position of the argument we are recursing on, among all parameters -/
   recArgPos    : Nat
-  /-- position (counted including fixed prefix) of the indices of the inductive datatype we are recursing on -/
+  /-- position of the indices of the inductive datatype we are recursing on, among all parameters -/
   indicesPos   : Array Nat
   /-- The inductive group (with parameters) of the argument's type -/
   indGroupInst : IndGroupInst
@@ -36,23 +37,29 @@ structure RecArgInfo where
   indIdx       : Nat
 deriving Inhabited, Repr
 
+  /-- position of the argument and its indices we are recursing on, among all parameters -/
+def RecArgInfo.indicesAndRecArgPos (info : RecArgInfo) : Array Nat :=
+  info.indicesPos.push info.recArgPos
+
 /--
-If `xs` are the parameters of the functions (excluding fixed prefix), partitions them
-into indices and major arguments, and other parameters.
+If `xs` are the varing parameters of the functions, partitions them into indices and major
+arguments, and other parameters.
 -/
 def RecArgInfo.pickIndicesMajor (info : RecArgInfo) (xs : Array Expr) : (Array Expr × Array Expr) := Id.run do
+  -- To simplify the index calculation, pad xs with dummy values where fixed parameters are
+  let xs := info.fixedParamPerm.buildArgs (mkArray info.fixedParamPerm.numFixed (mkSort 0)) xs
   -- First indices and major arg, using the order they appear in `info.indicesPos`
   let mut indexMajorArgs := #[]
   let indexMajorPos := info.indicesPos.push info.recArgPos
   for j in indexMajorPos do
-    assert! info.numFixed ≤ j && j - info.numFixed < xs.size
-    indexMajorArgs := indexMajorArgs.push xs[j - info.numFixed]!
+    indexMajorArgs := indexMajorArgs.push xs[j]!
   -- Then the other arguments, in the order they appear in `xs`
-  let mut otherArgs := #[]
+  let mut otherVaryingArgs := #[]
   for h : i in [:xs.size] do
-    unless indexMajorPos.contains (i + info.numFixed) do
-      otherArgs := otherArgs.push xs[i]
-  return (indexMajorArgs, otherArgs)
+    unless indexMajorPos.contains i do
+      unless info.fixedParamPerm.isFixed i do
+        otherVaryingArgs := otherVaryingArgs.push xs[i]
+  return (indexMajorArgs, otherVaryingArgs)
 
 /--
 Name of the recursive data type. Assumes that it is not one of the auxiliary ones.

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -10,6 +10,7 @@ import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Eqns
 import Lean.Meta.ArgsPacker.Basic
 import Lean.Elab.PreDefinition.WF.Unfold
+import Lean.Elab.PreDefinition.FixedParams
 import Init.Data.Array.Basic
 
 namespace Lean.Elab.WF
@@ -21,13 +22,15 @@ structure EqnInfo extends EqnInfoCore where
   declNameNonRec  : Name
   fixedPrefixSize : Nat
   argsPacker      : ArgsPacker
+  fixedParamPerms : FixedParamPerms
   deriving Inhabited
 
 
 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
-def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat)
+def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedParamPerms : FixedParamPerms)
     (argsPacker : ArgsPacker) : MetaM Unit := do
+  let fixedPrefixSize := fixedParamPerms.numFixed
   preDefs.forM fun preDef => ensureEqnReservedNamesAvailable preDef.declName
   /-
   See issue #2327.
@@ -40,7 +43,7 @@ def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fi
       modifyEnv fun env =>
         preDefs.foldl (init := env) fun env preDef =>
           eqnInfoExt.insert env preDef.declName { preDef with
-            declNames, declNameNonRec, fixedPrefixSize, argsPacker }
+            declNames, declNameNonRec, fixedPrefixSize, argsPacker, fixedParamPerms }
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if let some info := eqnInfoExt.find? (← getEnv) declName then

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -13,8 +13,10 @@ import Lean.Meta.ArgsPacker
 import Lean.Elab.Quotation
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
+import Lean.Elab.PreDefinition.Mutual
 import Lean.Elab.PreDefinition.Structural.Basic
 import Lean.Elab.PreDefinition.TerminationMeasure
+import Lean.Elab.PreDefinition.FixedParams
 import Lean.Elab.PreDefinition.WF.Basic
 import Lean.Data.Array
 
@@ -169,24 +171,25 @@ def withUserNames {α} (xs : Array Expr) (ns : Array Name) (k : MetaM α) : Meta
   withLCtx' lctx k
 
 /-- Create one measure for each (eligible) parameter of the given predefintion.  -/
-def simpleMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
+def simpleMeasures (preDefs : Array PreDefinition) (fixedParamPerms : FixedParamPerms)
     (userVarNamess : Array (Array Name)) : MetaM (Array (Array BasicMeasure)) := do
   let is_mutual : Bool := preDefs.size > 1
   preDefs.mapIdxM fun funIdx preDef => do
-    lambdaTelescope preDef.value fun xs _ => do
-      withUserNames xs[fixedPrefixSize:] userVarNamess[funIdx]! do
+    lambdaTelescope preDef.value fun params _ => do
+      let xs := fixedParamPerms.perms[funIdx]!.pickVarying params
+      withUserNames xs userVarNamess[funIdx]! do
         let mut ret : Array BasicMeasure := #[]
-        for x in xs[fixedPrefixSize:] do
+        for x in xs do
           -- If the `SizeOf` instance produces a constant (e.g. because it's type is a `Prop` or
           -- `Type`), then ignore this parameter
           let sizeOf ← whnfD (← mkAppM ``sizeOf #[x])
           if sizeOf.isLit then continue
 
-          let natFn ← mkLambdaFVars xs (← mkAppM ``sizeOf #[x])
+          let natFn ← mkLambdaFVars params (← mkAppM ``sizeOf #[x])
           -- Determine if we need to exclude `sizeOf` in the measure we show/pass on.
           let fn ←
-            if  ← mayOmitSizeOf is_mutual xs[fixedPrefixSize:] x
-            then mkLambdaFVars xs x
+            if  ← mayOmitSizeOf is_mutual xs x
+            then mkLambdaFVars params x
             else pure natFn
           ret := ret.push { ref := .missing, structural := false, fn, natFn }
         return ret
@@ -339,24 +342,26 @@ def filterSubsumed (rcs : Array RecCallWithContext ) : Array RecCallWithContext
 Traverse a unary `PreDefinition`, and returns a `WithRecCall` closure for each recursive
 call site.
 -/
-def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat)
+def collectRecCalls (unaryPreDef : PreDefinition) (fixedParamPerms : FixedParamPerms)
     (argsPacker : ArgsPacker) : MetaM (Array RecCallWithContext) := withoutModifyingState do
   addAsAxiom unaryPreDef
-  lambdaBoundedTelescope unaryPreDef.value (fixedPrefixSize + 1) fun xs body => do
-    unless xs.size == fixedPrefixSize + 1 do
+  lambdaBoundedTelescope unaryPreDef.value (fixedParamPerms.numFixed + 1) fun xs body => do
+    unless xs.size == fixedParamPerms.numFixed + 1 do
       throwError "Unexpected number of lambdas in unary pre-definition"
-    let ys := xs[:fixedPrefixSize]
-    let param := xs[fixedPrefixSize]!
-    withRecApps unaryPreDef.declName fixedPrefixSize param body fun param args => do
-      unless args.size ≥ fixedPrefixSize + 1 do
+    let ys := xs[:fixedParamPerms.numFixed]
+    let param := xs[fixedParamPerms.numFixed]!
+    withRecApps unaryPreDef.declName fixedParamPerms.numFixed param body fun param args => do
+      unless args.size ≥ fixedParamPerms.numFixed + 1 do
         throwError "Insufficient arguments in recursive call"
-      let arg := args[fixedPrefixSize]!
+      let arg := args[fixedParamPerms.numFixed]!
       trace[Elab.definition.wf] "collectRecCalls: {unaryPreDef.declName} ({param}) → {unaryPreDef.declName} ({arg})"
       let some (caller, params) := argsPacker.unpack param
         | throwError "Cannot unpack param, unexpected expression:{indentExpr param}"
       let some (callee, args) := argsPacker.unpack arg
         | throwError "Cannot unpack arg, unexpected expression:{indentExpr arg}"
-      RecCallWithContext.create (← getRef) caller (ys ++ params) callee (ys ++ args)
+      let callerParams := fixedParamPerms.perms[caller]!.buildArgs ys params
+      let calleeArgs := fixedParamPerms.perms[callee]!.buildArgs ys args
+      RecCallWithContext.create (← getRef) caller callerParams callee calleeArgs
 
 /-- Is the expression a `<`-like comparison of `Nat` expressions -/
 def isNatCmp (e : Expr) : Option (Expr × Expr) :=
@@ -367,7 +372,7 @@ def isNatCmp (e : Expr) : Option (Expr × Expr) :=
   | GE.ge α _ e₁ e₂ => if α.isConstOf ``Nat then some (e₂, e₁) else none
   | _ => none
 
-def complexMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
+def complexMeasures (preDefs : Array PreDefinition) (fixedParamPerms : FixedParamPerms)
     (userVarNamess : Array (Array Name)) (recCalls : Array RecCallWithContext) :
     MetaM (Array (Array BasicMeasure)) := do
   preDefs.mapIdxM fun funIdx _preDef => do
@@ -377,20 +382,21 @@ def complexMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
       unless rc.caller = funIdx do continue
       -- Only look at calls where the parameters have not been refined
       unless rc.params.all (·.isFVar) do continue
-      let xs := rc.params.map (·.fvarId!)
-      let varyingParams : Array FVarId := xs[fixedPrefixSize:]
+      let varyingParams := fixedParamPerms.perms[funIdx]!.pickVarying rc.params
+      let varyingFVars := varyingParams.map (·.fvarId!)
+      let params := rc.params.map (·.fvarId!)
       measures ← rc.ctxt.run do
-        withUserNames rc.params[fixedPrefixSize:] userVarNamess[funIdx]! do
+        withUserNames varyingParams userVarNamess[funIdx]! do
         trace[Elab.definition.wf] "rc: {rc.caller} ({rc.params}) → {rc.callee} ({rc.args})"
         let mut measures := measures
         for ldecl in ← getLCtx do
           if let some (e₁, e₂) := isNatCmp ldecl.type then
             -- We only want to consider these expressions if they depend only on the function's
             -- immediate arguments, so check that
-            if e₁.hasAnyFVar (! xs.contains ·) then continue
-            if e₂.hasAnyFVar (! xs.contains ·) then continue
+            if e₁.hasAnyFVar (! params.contains ·) then continue
+            if e₂.hasAnyFVar (! params.contains ·) then continue
             -- If e₁ does not depend on any varying parameters, simply ignore it
-            let e₁_is_const := ! e₁.hasAnyFVar (varyingParams.contains ·)
+            let e₁_is_const := ! e₁.hasAnyFVar (varyingFVars.contains ·)
             let body := if e₁_is_const then e₂ else mkNatSub e₂ e₁
             -- Avoid adding simple measures
             unless body.isFVar do
@@ -742,17 +748,18 @@ def mkProdElem (xs : Array Expr) : MetaM Expr := do
     let n := xs.size
     xs[0:n-1].foldrM (init:=xs[n-1]!) fun x p => mkAppM ``Prod.mk #[x,p]
 
-def toTerminationMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
+def toTerminationMeasures (preDefs : Array PreDefinition) (fixedParamPerms : FixedParamPerms)
     (userVarNamess : Array (Array Name)) (measuress : Array (Array BasicMeasure))
     (solution : Array MutualMeasure) : MetaM TerminationMeasures := do
   preDefs.mapIdxM fun funIdx preDef => do
     let measures := measuress[funIdx]!
-    lambdaTelescope preDef.value fun xs _ => do
-      withUserNames xs[fixedPrefixSize:] userVarNamess[funIdx]! do
+    lambdaTelescope preDef.value fun params _ => do
+      let xs := fixedParamPerms.perms[funIdx]!.pickVarying params
+      withUserNames xs userVarNamess[funIdx]! do
         let args := solution.map fun
-          | .args tmIdxs => measures[tmIdxs[funIdx]!]!.fn.beta xs
+          | .args tmIdxs => measures[tmIdxs[funIdx]!]!.fn.beta params
           | .func funIdx' => mkNatLit <| if funIdx' == funIdx then 1 else 0
-        let fn ← mkLambdaFVars xs (← mkProdElem args)
+        let fn ← mkLambdaFVars params (← mkProdElem args)
         return { ref := .missing, structural := false, fn}
 
 /--
@@ -780,19 +787,19 @@ terminates. See the module doc string for a high-level overview.
 The `preDefs` are used to determine arity and types of parameters; the bodies are ignored.
 -/
 def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
-    (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) :
+    (fixedParamPerms : FixedParamPerms) (argsPacker : ArgsPacker) :
     MetaM TerminationMeasures := do
   let userVarNamess ← argsPacker.varNamess.mapM (naryVarNames ·)
   trace[Elab.definition.wf] "varNames is: {userVarNamess}"
 
   -- Collect all recursive calls and extract their context
-  let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize argsPacker
+  let recCalls ← collectRecCalls unaryPreDef fixedParamPerms argsPacker
   let recCalls := filterSubsumed recCalls
 
   -- For every function, the measures we want to use
   -- (One for each non-forbiddend arg)
-  let basicMeassures₁ ← simpleMeasures preDefs fixedPrefixSize userVarNamess
-  let basicMeassures₂ ← complexMeasures preDefs fixedPrefixSize userVarNamess recCalls
+  let basicMeassures₁ ← simpleMeasures preDefs fixedParamPerms userVarNamess
+  let basicMeassures₂ ← complexMeasures preDefs fixedParamPerms userVarNamess recCalls
   let basicMeasures := Array.zipWith (· ++ ·) basicMeassures₁ basicMeassures₂
 
   -- The list of measures, including the measures that order functions.
@@ -801,7 +808,7 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
 
   -- If there is only one plausible measure, use that
   if let #[solution] := mutualMeasures then
-    let termMeasures ← toTerminationMeasures preDefs fixedPrefixSize userVarNamess basicMeasures #[solution]
+    let termMeasures ← toTerminationMeasures preDefs fixedParamPerms userVarNamess basicMeasures #[solution]
     reportTerminationMeasures preDefs termMeasures
     return termMeasures
 
@@ -810,7 +817,7 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
 
   match ← liftMetaM <| solve mutualMeasures callMatrix with
   | .some solution => do
-    let termMeasures ← toTerminationMeasures preDefs fixedPrefixSize userVarNamess basicMeasures solution
+    let termMeasures ← toTerminationMeasures preDefs fixedParamPerms userVarNamess basicMeasures solution
     reportTerminationMeasures preDefs termMeasures
     return termMeasures
   | .none =>

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -23,12 +23,11 @@ def wfRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option T
   let termMeasures? := termMeasure?s.mapM id -- Either all or none, checked by `elabTerminationByHints`
   let preDefs ← preDefs.mapM fun preDef =>
     return { preDef with value := (← floatRecApp preDef.value) }
-  let (fixedPrefixSize, argsPacker, unaryPreDef, wfPreprocessProofs) ← withoutModifyingEnv do
+  let (fixedParamPerms, argsPacker, unaryPreDef, wfPreprocessProofs) ← withoutModifyingEnv do
     for preDef in preDefs do
       addAsAxiom preDef
-    let fixedPrefixSize ← Mutual.getFixedPrefix preDefs
-    trace[Elab.definition.wf] "fixed prefix: {fixedPrefixSize}"
-    let varNamess ← preDefs.mapM (varyingVarNames fixedPrefixSize ·)
+    let fixedParamPerms ← getFixedParamPerms preDefs
+    let varNamess ← preDefs.mapIdxM fun i preDef => varyingVarNames fixedParamPerms i preDef
     for varNames in varNamess, preDef in preDefs do
       if varNames.isEmpty then
         throwError "well-founded recursion cannot be used, '{preDef.declName}' does not take any (non-fixed) arguments"
@@ -36,33 +35,35 @@ def wfRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option T
     let (preDefsAttached, wfPreprocessProofs) ← Array.unzip <$> preDefs.mapM fun preDef => do
       let result ← preprocess preDef.value
       return ({preDef with value := result.expr}, result)
-    return (fixedPrefixSize, argsPacker, ← packMutual fixedPrefixSize argsPacker preDefsAttached, wfPreprocessProofs)
+    let unaryPreDef ← packMutual fixedParamPerms argsPacker preDefsAttached
+    return (fixedParamPerms, argsPacker, unaryPreDef, wfPreprocessProofs)
+  trace[Elab.definition.wf] "unaryPreDef:{indentD unaryPreDef.value}"
 
   let wf : TerminationMeasures ← do
     if let some tms := termMeasures? then pure tms else
     -- No termination_by here, so use GuessLex to infer one
-    guessLex preDefs unaryPreDef fixedPrefixSize argsPacker
+    guessLex preDefs unaryPreDef fixedParamPerms argsPacker
 
-  let preDefNonRec ← forallBoundedTelescope unaryPreDef.type fixedPrefixSize fun prefixArgs type => do
+  let preDefNonRec ← forallBoundedTelescope unaryPreDef.type fixedParamPerms.numFixed fun fixedArgs type => do
     let type ← whnfForall type
     unless type.isForall do
       throwError "wfRecursion: expected unary function type: {type}"
     let packedArgType := type.bindingDomain!
-    elabWFRel (preDefs.map (·.declName)) unaryPreDef.declName prefixArgs argsPacker packedArgType wf fun wfRel => do
+    elabWFRel (preDefs.map (·.declName)) unaryPreDef.declName fixedParamPerms fixedArgs argsPacker packedArgType wf fun wfRel => do
       trace[Elab.definition.wf] "wfRel: {wfRel}"
       let (value, envNew) ← withoutModifyingEnv' do
         addAsAxiom unaryPreDef
-        let value ← mkFix unaryPreDef prefixArgs argsPacker wfRel (preDefs.map (·.declName)) (preDefs.map (·.termination.decreasingBy?))
+        let value ← mkFix unaryPreDef fixedArgs argsPacker wfRel (preDefs.map (·.declName)) (preDefs.map (·.termination.decreasingBy?))
         eraseRecAppSyntaxExpr value
       /- `mkFix` invokes `decreasing_tactic` which may add auxiliary theorems to the environment. -/
       let value ← unfoldDeclsFrom envNew value
       return { unaryPreDef with value }
 
   trace[Elab.definition.wf] ">> {preDefNonRec.declName} :=\n{preDefNonRec.value}"
-  let preDefsNonrec ← preDefsFromUnaryNonRec fixedPrefixSize argsPacker preDefs preDefNonRec
+  let preDefsNonrec ← preDefsFromUnaryNonRec fixedParamPerms argsPacker preDefs preDefNonRec
   Mutual.addPreDefsFromUnary preDefs preDefsNonrec preDefNonRec
   let preDefs ← Mutual.cleanPreDefs preDefs
-  registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker
+  registerEqnsInfo preDefs preDefNonRec.declName fixedParamPerms argsPacker
   for preDef in preDefs, wfPreprocessProof in wfPreprocessProofs do
     unless preDef.kind.isTheorem do
       unless (← isProp preDef.type) do

src/Lean/Elab/PreDefinition/WF/PackMutual.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Joachim Breitner
 prelude
 import Lean.Meta.ArgsPacker
 import Lean.Elab.PreDefinition.Basic
+import Lean.Elab.PreDefinition.FixedParams
 import Lean.Elab.PreDefinition.WF.Eqns
 
 /-!
@@ -38,7 +39,7 @@ def withAppN (n : Nat) (e : Expr) (k : Array Expr → MetaM Expr) : MetaM Expr :
 /--
 Processes the expression and replaces calls to  the `preDefs` with calls to `f`.
 -/
-def packCalls (fixedPrefix : Nat) (argsPacker : ArgsPacker) (funNames : Array Name) (newF : Expr)
+def packCalls (fixedParamPerms : FixedParamPerms) (argsPacker : ArgsPacker) (funNames : Array Name) (newF : Expr)
   (e : Expr) : MetaM Expr := do
   let fType ← inferType newF
   unless fType.isForall do
@@ -49,16 +50,19 @@ def packCalls (fixedPrefix : Nat) (argsPacker : ArgsPacker) (funNames : Array Na
     if !f.isConst then
       return TransformStep.done e
     if let some fidx := funNames.idxOf? f.constName! then
-      let arity := fixedPrefix + argsPacker.varNamess[fidx]!.size
+      assert! fidx < fixedParamPerms.perms.size
+      let mask := fixedParamPerms.perms[fidx]!.map Option.isSome
+      let arity := mask.size
       let e' ← withAppN arity e fun args => do
-        let packedArg ← argsPacker.pack domain fidx args[fixedPrefix:]
+        let varying := fixedParamPerms.perms[fidx]!.pickVarying args
+        let packedArg ← argsPacker.pack domain fidx varying
         return mkApp newF packedArg
       return TransformStep.done e'
     return TransformStep.done e
     )
 
-def mutualName (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) : Name :=
-  if argsPacker.onlyOneUnary then
+def mutualName (fixedParamPerms : FixedParamPerms) (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) : Name :=
+  if fixedParamPerms.fixedArePrefix && argsPacker.onlyOneUnary then
     preDefs[0]!.declName
   else
     if argsPacker.numFuncs > 1 then
@@ -70,13 +74,16 @@ def mutualName (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) : Name
 Creates a single unary function from the given `preDefs`, using the machinery in the `ArgPacker`
 module.
 -/
-def packMutual (fixedPrefix : Nat) (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) : MetaM PreDefinition := do
-  if argsPacker.onlyOneUnary then return preDefs[0]!
-  let newFn := mutualName argsPacker preDefs
+def packMutual (fixedParamPerms : FixedParamPerms) (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) : MetaM PreDefinition := do
+  let newFn := mutualName fixedParamPerms argsPacker preDefs
+  if newFn = preDefs[0]!.declName then
+    return preDefs[0]!
   -- Bring the fixed prefix into scope
-  forallBoundedTelescope preDefs[0]!.type (some fixedPrefix) fun ys _ => do
-    let types ← preDefs.mapM (instantiateForall ·.type ys)
-    let vals ← preDefs.mapM (instantiateLambda ·.value ys)
+  fixedParamPerms.perms[0]!.forallTelescope preDefs[0]!.type fun ys => do
+    let types ← preDefs.mapIdxM fun i preDef =>
+      fixedParamPerms.perms[i]!.instantiateForall preDef.type ys
+    let vals ← preDefs.mapIdxM fun i preDef =>
+      fixedParamPerms.perms[i]!.instantiateLambda preDef.value ys
 
     let type ← argsPacker.uncurryType types
 
@@ -90,12 +97,12 @@ def packMutual (fixedPrefix : Nat) (argsPacker : ArgsPacker) (preDefs : Array Pr
     let f := mkAppN (mkConst newFn us) ys
 
     let value ← argsPacker.uncurry vals
-    let value ← packCalls fixedPrefix argsPacker (preDefs.map (·.declName)) f value
+    let value ← packCalls fixedParamPerms argsPacker (preDefs.map (·.declName)) f value
     let value ← mkLambdaFVars ys value
     return { preDefNew with value }
 
 /--
-Collect the names of the varying variables (after the fixed prefix); this also determines the
+Collect the names of the varying variables (excluding the fixed parameters); this also determines the
 arity for the well-founded translations, and is turned into an `ArgsPacker`.
 We use the term to determine the arity, but take the name from the type, for better names in the
 ```
@@ -103,26 +110,33 @@ fun : (n : Nat) → Nat | 0 => 0 | n+1 => fun n
 ```
 idiom.
 -/
-def varyingVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Name) := do
+def varyingVarNames (fixedParamPerms : FixedParamPerms) (preDefIdx : Nat) (preDef : PreDefinition) : MetaM (Array Name) := do
   -- We take the arity from the term, but the names from the types
   let arity ← lambdaTelescope preDef.value fun xs _ => return xs.size
-  assert! fixedPrefixSize ≤ arity
   forallBoundedTelescope preDef.type arity fun xs _ => do
     assert! xs.size = arity
-    let xs : Array Expr := xs[fixedPrefixSize:]
-    xs.mapM (·.fvarId!.getUserName)
+    assert! fixedParamPerms.perms[preDefIdx]!.size = arity
+    let mut ns := #[]
+    for x in xs, paramInfo in fixedParamPerms.perms[preDefIdx]! do
+      if paramInfo.isSome then continue -- skip fixed parameters
+      ns := ns.push (← x.fvarId!.getUserName)
+    return ns
 
-
-def preDefsFromUnaryNonRec (fixedPrefixSize : Nat) (argsPacker : ArgsPacker)
+def preDefsFromUnaryNonRec (fixedParamPerms : FixedParamPerms) (argsPacker : ArgsPacker)
     (preDefs : Array PreDefinition) (unaryPreDefNonRec : PreDefinition) : MetaM (Array PreDefinition) := do
   withoutModifyingEnv do
     let us := unaryPreDefNonRec.levelParams.map mkLevelParam
     addAsAxiom unaryPreDefNonRec
     preDefs.mapIdxM fun fidx preDef => do
-      let value ← forallBoundedTelescope preDef.type (some fixedPrefixSize) fun xs _ => do
+      let arity := fixedParamPerms.perms[fidx]!.size
+      let value ← forallBoundedTelescope preDef.type (some arity) fun params _ => do
+        assert! arity = params.size
+        let xs := fixedParamPerms.perms[fidx]!.pickFixed params
+        let ys := fixedParamPerms.perms[fidx]!.pickVarying params
         let value := mkAppN (mkConst unaryPreDefNonRec.declName us) xs
         let value ← argsPacker.curryProj value fidx
-        mkLambdaFVars xs value
+        let value := value.beta ys
+        mkLambdaFVars params value
       trace[Elab.definition.wf] "{preDef.declName} := {value}"
       pure { preDef with value }
 

src/Lean/Elab/PreDefinition/WF/Rel.lean

@@ -10,6 +10,7 @@ import Lean.Meta.Tactic.Rename
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.TerminationMeasure
+import Lean.Elab.PreDefinition.FixedParams
 import Lean.Meta.ArgsPacker
 
 namespace Lean.Elab.WF
@@ -22,16 +23,18 @@ a mutual clique, they must be the same for all functions.
 
 This ensures the preconditions for `ArgsPacker.uncurryND`.
 -/
-def checkCodomains (names : Array Name) (prefixArgs : Array Expr) (arities : Array Nat)
+def checkCodomains (names : Array Name) (fixedParamPerms : FixedParamPerms) (fixedArgs : Array Expr) (arities : Array Nat)
     (termMeasures : TerminationMeasures) : TermElabM Expr := do
   let mut codomains := #[]
-  for name in names, arity in arities, termMeasure in termMeasures do
-    let type ← inferType (termMeasure.fn.beta prefixArgs)
-    let codomain ← forallBoundedTelescope type arity fun xs codomain => do
+  for name in names, funIdx in [:names.size], arity in arities, termMeasure in termMeasures do
+    let measureType ← inferType termMeasure.fn
+    let measureType ← fixedParamPerms.perms[funIdx]!.instantiateForall measureType fixedArgs
+    let codomain ← forallBoundedTelescope measureType arity fun xs codomain => do
+      assert! xs.size = arity
       let fvars := xs.map (·.fvarId!)
       if codomain.hasAnyFVar (fvars.contains ·) then
         throwErrorAt termMeasure.ref  m!"The termination measure's type must not depend on the " ++
-          m!"function's varying parameters, but {name}'s termination measure does:{indentExpr type}\n" ++
+          m!"function's varying parameters, but {name}'s termination measure does:{indentExpr measureType}\n" ++
           "Try using `sizeOf` explicitly"
       pure codomain
     codomains := codomains.push codomain
@@ -51,14 +54,16 @@ If the `termMeasures` map the packed argument `argType` to `β`, then this funct
 continuation a value of type `WellFoundedRelation argType` that is derived from the instance
 for `WellFoundedRelation β` using `invImage`.
 -/
-def elabWFRel (declNames : Array Name) (unaryPreDefName : Name) (prefixArgs : Array Expr)
-    (argsPacker : ArgsPacker) (argType : Expr) (termMeasures : TerminationMeasures)
+def elabWFRel (declNames : Array Name) (unaryPreDefName : Name) (fixedParamPerms : FixedParamPerms)
+    (fixedArgs : Array Expr) (argsPacker : ArgsPacker) (argType : Expr) (termMeasures : TerminationMeasures)
     (k : Expr → TermElabM α) : TermElabM α := withDeclName unaryPreDefName do
   let α := argType
   let u ← getLevel α
-  let β ← checkCodomains declNames prefixArgs argsPacker.arities termMeasures
+  let β ← checkCodomains declNames fixedParamPerms fixedArgs argsPacker.arities termMeasures
   let v ← getLevel β
-  let packedF ← argsPacker.uncurryND (termMeasures.map (·.fn.beta prefixArgs))
+  let fns ← termMeasures.mapIdxM fun i measure =>
+    fixedParamPerms.perms[i]!.instantiateLambda measure.fn fixedArgs
+  let packedF ← argsPacker.uncurryND fns
   let inst ← synthInstance (.app (.const ``WellFoundedRelation [v]) β)
   let rel ← instantiateMVars (mkApp4 (.const ``invImage [u,v]) α β packedF inst)
   k rel

src/Lean/Meta/ArgsPacker.lean

@@ -328,6 +328,8 @@ if they are all the same.
 
 -/
 def uncurryType (types : Array Expr) : MetaM Expr := do
+  if types.size = 1 then
+    return types[0]!
   let types ← types.mapM whnfForall
   types.forM fun type => do
     unless type.isForall do

src/Lean/Meta/Tactic/FunInd.lean

@@ -695,10 +695,10 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do
     | fix@WellFounded.fix α _motive rel wf body target =>
       unless params.back! == target do
         throwError "functional induction: expected the target as last parameter{indentExpr e}"
-      let fixedParams := params.pop
+      let fixedParamPerms := params.pop
       let motiveType ← mkForallFVars #[target] (.sort levelZero)
       withLocalDeclD `motive motiveType fun motive => do
-        let fn := mkAppN (← mkConstWithLevelParams name) fixedParams
+        let fn := mkAppN (← mkConstWithLevelParams name) fixedParamPerms
         let isRecCall : Expr → Option Expr := fun e =>
           if e.isApp && e.appFn!.isFVarOf motive.fvarId! then
             mkApp fn e.appArg!
@@ -732,7 +732,7 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do
         -- induction principle match the type of the function better.
         -- But this leads to avoidable parameters that make functional induction strictly less
         -- useful (e.g. when the unsued parameter mentions bound variables in the users' goal)
-        let (paramMask, e') ← mkLambdaFVarsMasked fixedParams e'
+        let (paramMask, e') ← mkLambdaFVarsMasked fixedParamPerms e'
         let e' ← instantiateMVars e'
         return (e', paramMask)
     | _ =>
@@ -787,16 +787,25 @@ def projectMutualInduct (names : Array Name) (mutualInduct : Name) : MetaM Unit
 For a (non-mutual!) definition of `name`, uses the `FunIndInfo` associated with the `unaryInduct` and
 derives the one for the n-ary function.
 -/
-def setNaryFunIndInfo (name : Name) (arity : Nat) (unaryInduct : Name) : MetaM Unit := do
-    let inductName := getFunInductName name
-    unless inductName = unaryInduct do
-      let some unaryFunIndInfo ← getFunIndInfoForInduct? unaryInduct
-        | throwError "Expected {unaryInduct} to have FunIndInfo"
-      setFunIndInfo {
-        unaryFunIndInfo with
-        funIndName := inductName
-        params := unaryFunIndInfo.params.filter (· != .target) ++ mkArray arity .target
-      }
+def setNaryFunIndInfo (fixedParamPerms : FixedParamPerms) (name : Name) (unaryInduct : Name) : MetaM Unit := do
+  assert!  fixedParamPerms.perms.size = 1 -- only non-mutual for now
+  let funIndName := getFunInductName name
+  unless funIndName = unaryInduct do
+    let some unaryFunIndInfo ← getFunIndInfoForInduct? unaryInduct
+      | throwError "Expected {unaryInduct} to have FunIndInfo"
+    let fixedParamPerm := fixedParamPerms.perms[0]!
+    let mut params := #[]
+    let mut j := 0
+    for h : i in [:fixedParamPerm.size] do
+      if fixedParamPerm[i].isSome then
+        assert! j + 1 < unaryFunIndInfo.params.size
+        params := params.push unaryFunIndInfo.params[j]!
+        j := j + 1
+      else
+        params := params.push .target
+    assert! j + 1 = unaryFunIndInfo.params.size
+
+    setFunIndInfo { unaryFunIndInfo with funIndName, params }
 
 /--
 In the type of `value`, reduces
@@ -920,13 +929,15 @@ Given a recursive definition `foo` defined via structural recursion, derive `foo
 if needed, and `foo.induct` for all functions in the group.
 See module doc for details.
  -/
-def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit := do
+def deriveInductionStructural (names : Array Name) (fixedParamPerms : FixedParamPerms) : MetaM Unit := do
   let infos ← names.mapM getConstInfoDefn
+  assert! infos.size > 0
   -- First open up the fixed parameters everywhere
-  let (e', paramMask, motiveArities) ← lambdaBoundedTelescope infos[0]!.value numFixed fun xs _ => do
+  let (e', paramMask, motiveArities) ← fixedParamPerms.perms[0]!.forallTelescope infos[0]!.type fun xs => do
     -- Now look at the body of an arbitrary of the functions (they are essentially the same
     -- up to the final projections)
-    let body ← instantiateLambda infos[0]!.value xs
+    let body ← fixedParamPerms.perms[0]!.instantiateLambda infos[0]!.value xs
+    let body := body.eta
 
     lambdaTelescope body fun ys body => do
       -- The body is of the form (brecOn … ).2.2.1 extra1 extra2 etc; ignore the
@@ -938,7 +949,7 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit
 
       let body := PProdN.stripProjs body
       let .const brecOnName us := f |
-        throwError "{infos[0]!.name}: unexpected body:{indentExpr infos[0]!.value}"
+        throwError "{infos[0]!.name}: unexpected body:{indentExpr infos[0]!.value}\ninstantiated to{indentExpr body}"
       unless isBRecOnRecursor (← getEnv) brecOnName do
         throwError "{infos[0]!.name}: expected .brecOn application, found:{indentExpr body}"
 
@@ -975,12 +986,13 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit
         motives.mapM fun motive =>
           forallTelescopeReducing motive fun xs _ => pure xs.size
 
-
-      let recArgInfos ← infos.mapM fun info => do
+      -- Recreate the recArgInfos. Maybe more robust and simpler to store relevant parts in the EqnInfos?
+      let recArgInfos ← infos.mapIdxM fun funIdx info => do
         let some eqnInfo := Structural.eqnInfoExt.find? (← getEnv) info.name | throwError "{info.name} missing eqnInfo"
-        let value ← instantiateLambda info.value xs
+        let value ← fixedParamPerms.perms[funIdx]!.instantiateLambda info.value xs
         let recArgInfo' ← lambdaTelescope value fun ys _ =>
-          Structural.getRecArgInfo info.name numFixed (xs ++ ys) eqnInfo.recArgPos
+          let args := fixedParamPerms.perms[funIdx]!.buildArgs xs ys
+          Structural.getRecArgInfo info.name fixedParamPerms.perms[funIdx]! args eqnInfo.recArgPos
         let #[recArgInfo] ← Structural.argsInGroup group xs value #[recArgInfo']
           | throwError "Structural.argsInGroup did not return a recArgInfo"
         pure recArgInfo
@@ -998,23 +1010,24 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit
         -- context, and are the parts relevant for every function in the mutual group
 
         -- Calculate the types of the induction motives (natural argument order) for each function
-        let motiveTypes ← infos.mapM fun info => do
-          lambdaTelescope (← instantiateLambda info.value xs) fun ys _ =>
+        let motiveTypes ← infos.mapIdxM fun funIdx info => do
+          lambdaTelescope (← fixedParamPerms.perms[funIdx]!.instantiateLambda info.value xs) fun ys _ =>
             mkForallFVars ys (.sort levelZero)
-        let motiveArities ← infos.mapM fun info => do
-          lambdaTelescope (← instantiateLambda info.value xs) fun ys _ => pure ys.size
+        let motiveArities ← infos.mapIdxM fun funIdx info => do
+          lambdaTelescope (← fixedParamPerms.perms[funIdx]!.instantiateLambda info.value xs) fun ys _ =>
+            pure ys.size
         let motiveNames := Array.ofFn (n := infos.size) fun ⟨i, _⟩ =>
           if infos.size = 1 then .mkSimple "motive" else .mkSimple s!"motive_{i+1}"
 
         withLocalDeclsDND (motiveNames.zip motiveTypes) fun motives => do
 
           -- Prepare the `isRecCall` that recognizes recursive calls
-          let fns := infos.map fun info =>
-            mkAppN (.const info.name (info.levelParams.map mkLevelParam)) xs
           let isRecCall : Expr → Option Expr := fun e => do
-            if let .some i := motives.idxOf? e.getAppFn then
-              if e.getAppNumArgs = motiveArities[i]! then
-                return mkAppN fns[i]! e.getAppArgs
+            if let .some funIdx := motives.idxOf? e.getAppFn then
+              if e.getAppNumArgs = motiveArities[funIdx]! then
+                let info := infos[funIdx]!
+                let args := fixedParamPerms.perms[funIdx]!.buildArgs xs e.getAppArgs
+                return mkAppN (.const info.name (info.levelParams.map mkLevelParam)) args
             .none
 
           -- Motives with parameters reordered, to put indices and major first
@@ -1062,8 +1075,8 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit
             for info in infos, recArgInfo in recArgInfos, idx in [:infos.size] do
               -- Take care to pick the `ys` from the type, to get the variable names expected
               -- by the user, but use the value arity
-              let arity ← lambdaTelescope (← instantiateLambda info.value xs) fun ys _ => pure ys.size
-              let e ← forallBoundedTelescope (← instantiateForall info.type xs) arity fun ys _ => do
+              let arity ← lambdaTelescope (← fixedParamPerms.perms[idx]!.instantiateLambda info.value xs) fun ys _ => pure ys.size
+              let e ← forallBoundedTelescope (← fixedParamPerms.perms[idx]!.instantiateForall info.type xs) arity fun ys _ => do
                 let (indicesMajor, rest) := recArgInfo.pickIndicesMajor ys
                 -- Find where in the function packing we are (TODO: abstract out)
                 let some indIdx := positions.findIdx? (·.contains idx) | panic! "invalid positions"
@@ -1205,9 +1218,9 @@ def deriveInduction (name : Name) : MetaM Unit := do
       let unpackedInductName ← unpackMutualInduction eqnInfo unaryInductName
       projectMutualInduct eqnInfo.declNames unpackedInductName
       if eqnInfo.argsPacker.numFuncs = 1 then
-        setNaryFunIndInfo eqnInfo.declNames[0]! eqnInfo.argsPacker.arities[0]! unaryInductName
+        setNaryFunIndInfo eqnInfo.fixedParamPerms eqnInfo.declNames[0]! unaryInductName
     else if let some eqnInfo := Structural.eqnInfoExt.find? (← getEnv) name then
-      deriveInductionStructural eqnInfo.declNames eqnInfo.numFixed
+      deriveInductionStructural eqnInfo.declNames eqnInfo.fixedParamPerms
     else
       throwError "constant '{name}' is not structurally or well-founded recursive"
 

src/Lean/Meta/Tactic/FunIndInfo.lean

@@ -21,7 +21,7 @@ inductive FunIndParamKind where
   | dropped
   | param
   | target
-deriving BEq, Repr
+deriving BEq, Repr, Inhabited
 
 /--
 A `FunIndInfo` indicates how a function's arguments map to the arguments of the functional induction

tests/lean/1673.lean.expected.out

@@ -4,7 +4,7 @@ with errors
 failed to infer structural recursion:
 Not considering parameter n of foo.a:
   it is unchanged in the recursive calls
-Not considering parameter nope of foo.a:
+Not considering parameter #2 of foo.a:
   it is unchanged in the recursive calls
 no parameters suitable for structural recursion
 

tests/lean/guessLexFailures.lean.expected.out

@@ -49,7 +49,7 @@ Please use `termination_by` to specify a decreasing measure.
 guessLexFailures.lean:37:0-43:31: error: Could not find a decreasing measure.
 The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
-           n m x4
+           n m x3
 1) 39:6-27 = =  =
 2) 40:6-25 = <  _
 3) 41:6-25 < _  _

tests/lean/run/4928.lean

@@ -1,17 +1,16 @@
 /--
 error: tactic 'fail' failed
-x y : Nat
-⊢ x - 1 < x
+z : Nat
+⊢ z - 1 < z
 -/
 #guard_msgs in
-def g (x : Nat) (y : Nat) : Nat := g (x - 1) y
-termination_by x
+def g (z : Nat) (y : Nat) : Nat := g (z - 1) y
+termination_by z
 decreasing_by fail
 
 /--
 error: tactic 'fail' failed
 x : List Nat
-y : Nat
 ⊢ sizeOf x.tail < sizeOf x
 -/
 #guard_msgs in
@@ -22,7 +21,6 @@ decreasing_by fail
 /--
 error: tactic 'fail' failed
 x : List Nat
-y : Nat
 ⊢ x.tail.length < x.length
 -/
 #guard_msgs in
@@ -33,7 +31,6 @@ decreasing_by fail
 /--
 error: tactic 'fail' failed
 x : List Nat
-y : Nat
 ⊢ x.tail.length < x.length
 -/
 #guard_msgs in
@@ -49,13 +46,8 @@ end
 /--
 error: tactic 'fail' failed
 x : List Nat
-y : Nat
-⊢ (invImage
-        (fun x =>
-          PSum.casesOn x (fun _x => PSigma.casesOn _x fun x y => x.length) fun _x =>
-            PSigma.casesOn _x fun x y => x.length)
-        instWellFoundedRelationOfSizeOf).1
-    (PSum.inr ⟨x.tail, y⟩) (PSum.inl ⟨x, y⟩)
+⊢ (invImage (fun x => PSum.casesOn x (fun x => x.length) fun x => x.length) instWellFoundedRelationOfSizeOf).1
+    (PSum.inr x.tail) (PSum.inl x)
 -/
 #guard_msgs in
 set_option debug.rawDecreasingByGoal true in

tests/lean/run/fixedParams.lean

@@ -0,0 +1,101 @@
+private axiom test_sorry : ∀ {α}, α
+
+set_option trace.Elab.definition.fixedParams true
+
+namespace Ex1
+
+/--
+error: well-founded recursion cannot be used, 'Ex1.foo' does not take any (non-fixed) arguments
+---
+info: [Elab.definition.fixedParams] getFixedParams:
+      • ⏎
+      •
+-/
+#guard_msgs in
+mutual
+def foo : Nat := bar
+def bar : Nat := foo
+decreasing_by exact test_sorry
+end
+
+end Ex1
+
+
+namespace Ex2
+/--
+error: well-founded recursion cannot be used, 'Ex2.foo' does not take any (non-fixed) arguments
+---
+info: [Elab.definition.fixedParams] getFixedParams:
+      • [#1 #1]
+      • [#1 #1]
+-/
+#guard_msgs in
+mutual
+def foo (n : Nat) : Nat := bar n
+def bar (n : Nat) : Nat := foo n
+decreasing_by exact test_sorry
+end
+end Ex2
+
+namespace Ex3
+/--
+error: well-founded recursion cannot be used, 'Ex3.foo' does not take any (non-fixed) arguments
+---
+info: [Elab.definition.fixedParams] getFixedParams:
+      • [#1 #2] [#2 #1]
+      • [#2 #1] [#1 #2]
+-/
+#guard_msgs in
+mutual
+def foo (n : Nat) (m : Nat) : Nat := bar m n
+decreasing_by all_goals exact test_sorry
+def bar (n : Nat) (m : Nat) : Nat := foo m n
+decreasing_by all_goals exact test_sorry
+end
+end Ex3
+
+namespace Ex4
+/--
+info: [Elab.definition.fixedParams] getFixedParams: notFixed 0 3:
+    In foo c n b m
+    m not matched
+[Elab.definition.fixedParams] getFixedParams: • [#1 #3] ❌ [#3 #1] ❌ • [#3 #1] ❌ [#1 #3] ❌
+-/
+#guard_msgs in
+mutual
+def foo (a : Nat) (n : Nat) (d : Nat) (m : Nat) : Nat := bar d m a n
+decreasing_by exact test_sorry
+def bar (b : Nat) (n : Nat) (c : Nat) (m : Nat) : Nat := foo c n b m
+decreasing_by exact test_sorry
+end
+end Ex4
+
+namespace Append1
+
+/--
+info: [Elab.definition.fixedParams] getFixedParams: notFixed 0 1:
+    In app as bs
+    x✝¹ =/= as
+[Elab.definition.fixedParams] getFixedParams: notFixed 0 2:
+    In app as bs
+    x✝ =/= bs
+[Elab.definition.fixedParams] getFixedParams: • [#1] ❌ ❌
+-/
+#guard_msgs(info) in
+def app : List α → List α → List α
+  | [], bs => bs
+  | a::as, bs => a :: app as bs
+
+/--
+info: [Elab.definition.fixedParams] getFixedParams: notFixed 0 1:
+    In app' as bs
+    as✝ =/= as
+[Elab.definition.fixedParams] getFixedParams: • [#1] ❌ [#3]
+-/
+#guard_msgs(info) in
+def app' (as : List α) (bs : List α) : List α :=
+  match as with
+  | [] => bs
+  | a::as => a :: app' as bs
+
+end Append1

tests/lean/run/fixedParamsAnnot.lean

@@ -0,0 +1,75 @@
+/-!
+This test contains functions with fixed parameter that have dependencies on varying parameter,
+but only in annotations (optional parameters).
+-/
+
+private axiom test_sorry : ∀ {α}, α
+
+namespace Ex1
+
+mutual
+def foo (varying : Nat) (fixed := varying) : Nat := bar fixed (varying + fixed)
+decreasing_by exact test_sorry
+def bar  (fixed : Nat) (varying : Nat) : Nat := foo (varying + fixed) fixed
+decreasing_by exact test_sorry
+end
+
+/--
+info: equations:
+theorem Ex1.foo.eq_1 : ∀ (varying fixed : Nat), foo varying fixed = bar fixed (varying + fixed)
+-/
+#guard_msgs in
+#print equations foo
+
+/--
+info: equations:
+theorem Ex1.bar.eq_1 : ∀ (fixed varying : Nat), bar fixed varying = foo (varying + fixed) fixed
+-/
+#guard_msgs in
+#print equations bar
+
+
+/--
+info: Ex1.foo.induct (fixed : Nat) (motive1 motive2 : Nat → Prop)
+  (case1 : ∀ (varying : Nat), motive2 (varying + fixed) → motive1 varying)
+  (case2 : ∀ (varying : Nat), motive1 (varying + fixed) → motive2 varying) (varying : Nat) : motive1 varying
+-/
+#guard_msgs in
+#check foo.induct
+
+
+end Ex1
+
+namespace Ex2
+
+mutual
+def bar  (fixed : Nat) (varying : Nat) : Nat := foo (varying + fixed) fixed
+decreasing_by exact test_sorry
+def foo (varying : Nat) (fixed := varying) : Nat := bar fixed (varying + fixed)
+decreasing_by exact test_sorry
+end
+
+/--
+info: equations:
+theorem Ex2.foo.eq_1 : ∀ (varying fixed : Nat), foo varying fixed = bar fixed (varying + fixed)
+-/
+#guard_msgs in
+#print equations foo
+
+/--
+info: equations:
+theorem Ex2.bar.eq_1 : ∀ (fixed varying : Nat), bar fixed varying = foo (varying + fixed) fixed
+-/
+#guard_msgs in
+#print equations bar
+
+/--
+info: Ex2.foo.induct (fixed : Nat) (motive1 motive2 : Nat → Prop)
+  (case1 : ∀ (varying : Nat), motive2 (varying + fixed) → motive1 varying)
+  (case2 : ∀ (varying : Nat), motive1 (varying + fixed) → motive2 varying) (varying : Nat) : motive2 varying
+-/
+#guard_msgs in
+#check foo.induct
+
+
+end Ex2

tests/lean/run/fixedParamsDep.lean

@@ -0,0 +1,79 @@
+/-!
+This test contains functions with fixed parameter that have dependencies on varying parameter,
+which can happen when those dependencies reduce away.
+-/
+
+def const (x : α) (_ : β) : α := x
+
+private axiom test_sorry : ∀ {α}, α
+
+namespace Ex1
+
+mutual
+def foo (varying : Nat) (fixed : const Nat varying) : Nat := bar fixed (Nat.add varying fixed)
+decreasing_by exact test_sorry
+def bar  (fixed : Nat) (varying : Nat) : Nat := foo (varying + fixed) fixed
+decreasing_by exact test_sorry
+end
+
+/--
+info: equations:
+theorem Ex1.foo.eq_1 : ∀ (varying : Nat) (fixed : const Nat varying), foo varying fixed = bar fixed (varying.add fixed)
+-/
+#guard_msgs in
+#print equations foo
+
+/--
+info: equations:
+theorem Ex1.bar.eq_1 : ∀ (fixed varying : Nat), bar fixed varying = foo (varying + fixed) fixed
+-/
+#guard_msgs in
+#print equations bar
+
+
+/--
+info: Ex1.foo.induct (motive1 : (varying : Nat) → const Nat varying → Prop) (motive2 : Nat → Nat → Prop)
+  (case1 : ∀ (varying : Nat) (fixed : const Nat varying), motive2 fixed (varying.add fixed) → motive1 varying fixed)
+  (case2 : ∀ (fixed varying : Nat), motive1 (varying + fixed) fixed → motive2 fixed varying) (varying : Nat)
+  (fixed : const Nat varying) : motive1 varying fixed
+-/
+#guard_msgs in
+#check foo.induct
+
+
+end Ex1
+
+namespace Ex2
+
+mutual
+def bar  (fixed : Nat) (varying : Nat) : Nat := foo (varying + fixed) fixed
+decreasing_by exact test_sorry
+def foo (varying : Nat) (fixed : const Nat varying) : Nat := bar fixed (Nat.add varying fixed)
+decreasing_by exact test_sorry
+end
+
+/--
+info: equations:
+theorem Ex2.foo.eq_1 : ∀ (varying : Nat) (fixed : const Nat varying), foo varying fixed = bar fixed (varying.add fixed)
+-/
+#guard_msgs in
+#print equations foo
+
+/--
+info: equations:
+theorem Ex2.bar.eq_1 : ∀ (fixed varying : Nat), bar fixed varying = foo (varying + fixed) fixed
+-/
+#guard_msgs in
+#print equations bar
+
+/--
+info: Ex2.foo.induct (motive1 : Nat → Nat → Prop) (motive2 : (varying : Nat) → const Nat varying → Prop)
+  (case1 : ∀ (fixed varying : Nat), motive2 (varying + fixed) fixed → motive1 fixed varying)
+  (case2 : ∀ (varying : Nat) (fixed : const Nat varying), motive1 fixed (varying.add fixed) → motive2 varying fixed)
+  (varying : Nat) (fixed : const Nat varying) : motive2 varying fixed
+-/
+#guard_msgs in
+#check foo.induct
+
+
+end Ex2

tests/lean/run/fixedParamsReorder.lean

@@ -0,0 +1,34 @@
+/-!
+This test contains functions with fixed parameter that appear in different orders.
+-/
+
+private axiom test_sorry : ∀ {α}, α
+
+mutual
+def foo (a : Nat) (n : Nat) (d : Nat) (m : Int) : Nat := bar d m (a + n + d + m.natAbs) n
+decreasing_by exact test_sorry
+def bar (b : Nat) (n : Int) (c : Nat) (m : Nat) : Nat := foo c m (b + n.natAbs + c + m) n
+decreasing_by exact test_sorry
+end
+
+/--
+info: equations:
+theorem bar.eq_1 : ∀ (b : Nat) (n : Int) (c m : Nat), bar b n c m = foo c m (b + n.natAbs + c + m) n
+-/
+#guard_msgs in
+#print equations bar
+
+/--
+info: foo.induct (n : Nat) (m : Int) (motive1 motive2 : Nat → Nat → Prop)
+  (case1 : ∀ (a d : Nat), motive2 d (a + n + d + m.natAbs) → motive1 a d)
+  (case2 : ∀ (b c : Nat), motive1 c (b + m.natAbs + c + n) → motive2 b c) (a d : Nat) : motive1 a d
+-/
+#guard_msgs in
+#check foo.induct
+/--
+info: bar.induct (n : Nat) (m : Int) (motive1 motive2 : Nat → Nat → Prop)
+  (case1 : ∀ (a d : Nat), motive2 d (a + n + d + m.natAbs) → motive1 a d)
+  (case2 : ∀ (b c : Nat), motive1 c (b + m.natAbs + c + n) → motive2 b c) (b c : Nat) : motive2 b c
+-/
+#guard_msgs in
+#check bar.induct

tests/lean/run/fixedParamsStructDeps.lean

@@ -0,0 +1,33 @@
+/-!
+Testing a few more corner cases related to structural mutual recursion, parameters, indices,
+dependencies.
+-/
+
+def const (x : α) (_ : β) : α := x
+
+private axiom test_sorry : ∀ {α}, α
+
+
+inductive T (p : Nat) : (i : Nat) → Type where
+  | zero : T p i
+  | succ : T p i → T p (i + p) → T p i
+
+/--
+error: failed to infer structural recursion:
+Cannot use parameters #4 of foo and #4 of bar:
+  its type is an inductive datatype and the datatype parameter
+    p1
+  which cannot be fixed as it is an index or depends on an index, and indices cannot be fixed parameters when using structural recursion.
+-/
+#guard_msgs in
+mutual
+def foo (i : Nat) (p1 : Nat) (p2 : const Nat i) : T p1 i → Unit
+  | .zero => ()
+  | .succ t1 _ => bar i p2 p1 t1
+termination_by structural t => t
+
+def bar (i : Nat) (p2 : Nat) (p1 : const Nat p2) : T p1 i → Unit
+  | .zero => ()
+  | .succ t1 _ => foo i p1 p2 t1
+termination_by structural t => t
+end

tests/lean/run/funind_structural.lean

@@ -72,9 +72,10 @@ theorem zip_length {α β} (xs : List α) (ys : List β) :
     simp [Nat.min_def]
     split <;> omega
 
-theorem zip_get?  {α β} (as : List α) (bs : List β) :
-    (List.zip as bs).get? i = match as.get? i, bs.get? i with
-      | some a, some b => some (a, b) | _, _ => none := by
+theorem zip_get? {i : Nat}  {α β} (as : List α) (bs : List β) :
+    (List.zip as bs)[i]? = match as[i]?, bs[i]? with
+      | some a, some b => some (a, b)
+      | _, _ => none := by
   induction as, bs using zip.induct generalizing i
     <;> cases i <;> simp_all
 
@@ -118,18 +119,17 @@ def Tree.insert (t : Tree β) (k : Nat) (v : β) : Tree β :=
 termination_by structural t
 
 /--
-info: TreeExample.Tree.insert.induct.{u_1} {β : Type u_1} (motive : Tree β → Nat → β → Prop)
-  (case1 : ∀ (k : Nat) (v : β), motive Tree.leaf k v)
+info: TreeExample.Tree.insert.induct.{u_1} {β : Type u_1} (k : Nat) (motive : Tree β → Prop) (case1 : motive Tree.leaf)
   (case2 :
-    ∀ (k : Nat) (v : β) (left : Tree β) (key : Nat) (value : β) (right : Tree β),
-      k < key → motive left k v → motive (left.node key value right) k v)
+    ∀ (left : Tree β) (key : Nat) (value : β) (right : Tree β),
+      k < key → motive left → motive (left.node key value right))
   (case3 :
-    ∀ (k : Nat) (v : β) (left : Tree β) (key : Nat) (value : β) (right : Tree β),
-      ¬k < key → key < k → motive right k v → motive (left.node key value right) k v)
+    ∀ (left : Tree β) (key : Nat) (value : β) (right : Tree β),
+      ¬k < key → key < k → motive right → motive (left.node key value right))
   (case4 :
-    ∀ (k : Nat) (v : β) (left : Tree β) (key : Nat) (value : β) (right : Tree β),
-      ¬k < key → ¬key < k → motive (left.node key value right) k v)
-  (t : Tree β) (k : Nat) (v : β) : motive t k v
+    ∀ (left : Tree β) (key : Nat) (value : β) (right : Tree β),
+      ¬k < key → ¬key < k → motive (left.node key value right))
+  (t : Tree β) : motive t
 -/
 #guard_msgs in
 #check Tree.insert.induct

tests/lean/run/funind_tests.lean

@@ -689,8 +689,8 @@ def foo (fixed : Bool := false) (n : Nat) (m : Nat := 0) : Nat :=
 termination_by n
 
 /--
-info: DefaultArgument.foo.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
-  (case2 : ∀ (m n : Nat), motive n m → motive n.succ m) (n m : Nat) : motive n m
+info: DefaultArgument.foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
+  (n : Nat) : motive n
 -/
 #guard_msgs in
 #check foo.induct

tests/lean/run/funinduction_generalize.lean

@@ -7,6 +7,11 @@ In particular that it behaves the same as `induction … using ….induct`.
 variable (xs ys : List Nat)
 variable (P : ∀ {α}, List α → Prop)
 
+-- We re-define this here to avoid stage0 complications
+def zipWith (f : α → β → γ) : (xs : List α) → (ys : List β) → List γ
+  | x::xs, y::ys => f x y :: zipWith f xs ys
+  | _,     _     => []
+
 /--
 error: unsolved goals
 case case1
@@ -28,7 +33,7 @@ x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs
 -/
 #guard_msgs in
 example : P (List.zip xs ys) := by
-  fun_induction List.zipWith _ xs ys
+  fun_induction zipWith _ xs ys
 
 
 /--
@@ -54,7 +59,7 @@ h : t✝.isEmpty = true
 -/
 #guard_msgs in
 example (h : xs.isEmpty) : P (List.zip xs ys) := by
-  fun_induction List.zipWith _ xs ys
+  fun_induction zipWith _ xs ys
 
 
 /--
@@ -80,7 +85,7 @@ h : t✝.isEmpty = true
 -/
 #guard_msgs in
 example (h : xs.isEmpty) : P (List.zip xs ys) := by
-  fun_induction List.zipWith _ xs (ys.take 2)
+  fun_induction zipWith _ xs (ys.take 2)
 
 /--
 error: unsolved goals
@@ -105,7 +110,7 @@ h : t✝.isEmpty = true
 -/
 #guard_msgs in
 example (h : xs.isEmpty) : P (List.zip xs ys) := by
-  induction xs, ys.take 2 using List.zipWith.induct
+  induction xs, ys.take 2 using zipWith.induct
 
 /--
 error: unsolved goals
@@ -130,7 +135,7 @@ x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs
 -/
 #guard_msgs in
 example (h : xs.isEmpty) : P (List.zip xs ys) := by
-  fun_induction List.zipWith _ (xs.take 2) ys
+  fun_induction zipWith _ (xs.take 2) ys
 
 /--
 error: unsolved goals
@@ -155,7 +160,7 @@ x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs
 -/
 #guard_msgs in
 example (h : xs.isEmpty) : P (List.zip xs ys) := by
-  induction xs.take 2, ys using List.zipWith.induct
+  induction xs.take 2, ys using zipWith.induct
 
 /--
 error: unsolved goals
@@ -180,7 +185,7 @@ h : xs.isEmpty = true
 -/
 #guard_msgs in
 example (h : xs.isEmpty) : P (List.zip xs ys) := by
-  fun_induction List.zipWith _ (xs.take 2) ys generalizing xs
+  fun_induction zipWith _ (xs.take 2) ys generalizing xs
 
 /--
 error: unsolved goals
@@ -205,4 +210,4 @@ h : xs.isEmpty = true
 -/
 #guard_msgs in
 example (h : xs.isEmpty) : P (List.zip xs ys) := by
-  induction xs.take 2, ys using List.zipWith.induct generalizing xs
+  induction xs.take 2, ys using zipWith.induct generalizing xs

tests/lean/run/funinduction_ident.lean

@@ -1,23 +1,36 @@
+-- We re-define these here to avoid stage0 complications
+def map (f : α → β) : List α → List β
+  | []    => []
+  | a::as => f a :: map f as
+
+def zipWith (f : α → β → γ) : (xs : List α) → (ys : List β) → List γ
+  | x::xs, y::ys => f x y :: zipWith f xs ys
+  | _,     _     => []
+
+def append : (xs ys : List α) → List α
+  | [],    bs => bs
+  | a::as, bs => a :: append as bs
+
 namespace ListEx
 
-theorem map_id (xs : List α) : List.map id xs = xs := by
-  fun_induction List.map <;> simp_all only [List.map, id]
+theorem map_id (xs : List α) : map id xs = xs := by
+  fun_induction map <;> simp_all only [map, id]
 
 -- This works because collect ignores `.dropped` arguments
 
 theorem map_map (f : α → β) (g : β → γ) xs :
-  List.map g (List.map f xs) = List.map (g ∘ f) xs := by
-  fun_induction List.map <;> simp_all only [List.map, Function.comp]
+  map g (map f xs) = map (g ∘ f) xs := by
+  fun_induction map <;> simp_all only [map, Function.comp]
 
 -- This should genuinely not work, but have a good error message
 
 /--
-error: found more than one suitable call of 'List.append' in the goal. Please include the desired arguments.
+error: found more than one suitable call of 'append' in the goal. Please include the desired arguments.
 -/
 #guard_msgs in
 theorem append_assoc :
-  List.append xs (List.append ys zs) = List.append (List.append xs ys) zs := by
-  fun_induction List.append <;> simp_all only [List.append]
+  append xs (append ys zs) = append (append xs ys) zs := by
+  fun_induction append <;> simp_all only [append]
 
 end ListEx
 

tests/lean/run/grind_constProp.lean

@@ -82,10 +82,10 @@ attribute [local grind] State.update State.find? State.get State.erase
   grind
 
 @[simp] theorem State.find?_update_self (σ : State) (x : Var) (v : Val) : (σ.update x v).find? x = some v := by
-  induction σ, x, v using State.update.induct <;> grind
+  induction σ using State.update.induct x <;> grind
 
 @[simp] theorem State.find?_update (σ : State) (v : Val) (h : x ≠ z) : (σ.update x v).find? z = σ.find? z := by
-  induction σ, x, v using State.update.induct <;> grind
+  induction σ using State.update.induct x <;> grind
 
 @[grind =] theorem State.find?_update_eq (σ : State) (v : Val)
     : (σ.update x v).find? z = if x = z then some v else σ.find? z := by
@@ -95,17 +95,17 @@ attribute [local grind] State.update State.find? State.get State.erase
   grind
 
 @[simp] theorem State.find?_erase_self (σ : State) (x : Var) : (σ.erase x).find? x = none := by
-  induction σ, x using State.erase.induct <;> grind
+  induction σ using State.erase.induct x <;> grind
 
 @[simp] theorem State.find?_erase (σ : State) (h : x ≠ z) : (σ.erase x).find? z = σ.find? z := by
-  induction σ, x using State.erase.induct <;> grind
+  induction σ using State.erase.induct x <;> grind
 
 @[simp, grind =] theorem State.find?_erase_eq (σ : State)
     : (σ.erase x).find? z = if x = z then none else σ.find? z := by
   grind only [= find?_erase_self, = find?_erase, cases Or]
 
 @[grind] theorem State.length_erase_le (σ : State) (x : Var) : (σ.erase x).length ≤ σ.length := by
-  induction σ, x using erase.induct <;> grind
+  induction σ using erase.induct x <;> grind
 
 def State.length_erase_lt (σ : State) (x : Var) : (σ.erase x).length < σ.length.succ := by
   grind
@@ -299,7 +299,7 @@ theorem State.cons_le_of_eq (h₁ : σ' ≼ σ) (h₂ : σ.find? x = some v) : (
   grind
 
 @[grind] theorem State.join_le_left (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₁ := by
-  induction σ₁, σ₂ using State.join.induct <;> grind
+  induction σ₁ using State.join.induct σ₂ <;> grind
 
 @[grind] theorem State.join_le_left_of (h : σ₁ ≼ σ₂) (σ₃ : State) : σ₁.join σ₃ ≼ σ₂ := by
   grind

tests/lean/run/issue2102.lean

@@ -0,0 +1,45 @@
+-- works
+def g' (T : Type) (ls : List T) : (Option (List T)) :=
+  match ls with
+  | _::tl =>
+      let res := Option.attach (g' T tl)
+      res.bind fun x => x.val
+  | [] => .none
+
+-- doesn't
+
+/--
+error: fail to show termination for
+  g''
+with errors
+failed to infer structural recursion:
+Not considering parameter T of g'':
+  its type is not an inductive
+Not considering parameter ls of g'':
+  its type is an inductive datatype
+    List T
+  and the datatype parameter
+    T
+  depends on the function parameter
+    T
+  which is not fixed.
+no parameters suitable for structural recursion
+
+failed to prove termination, possible solutions:
+  - Use `have`-expressions to prove the remaining goals
+  - Use `termination_by` to specify a different well-founded relation
+  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
+T✝ : Type
+head✝ : T✝
+tl : List T✝
+T : Type
+ls : List T
+⊢ sizeOf ls < 1 + sizeOf tl
+-/
+#guard_msgs in
+def g'' (T : Type) (ls : List T) : (Option (List T)) :=
+  match ls with
+  | _::tl =>
+      let res := Option.attach (g'' T tl)
+      res.bind fun ⟨x,h⟩ => x
+  | [] => .none

tests/lean/run/issue2108.lean

@@ -0,0 +1,40 @@
+inductive Foo : Nat → Type where
+| foo: (Nat → Foo n) → Foo n
+
+-- structural recursion failed, produced type incorrect term
+
+/--
+error: fail to show termination for
+  Foo.bar
+with errors
+failed to infer structural recursion:
+Not considering parameter #2 of Foo.bar:
+  its type is an inductive datatype
+    Foo x✝¹
+  and the datatype parameter
+    x✝¹
+  depends on the function parameter
+    x✝¹
+  which is not fixed.
+Cannot use parameter #1:
+  failed to eliminate recursive application
+    (f 0).bar
+
+
+Could not find a decreasing measure.
+The basic measures relate at each recursive call as follows:
+(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
+            n #1
+1) 36:14-23 =  ?
+
+#1: sizeOf x2
+
+Please use `termination_by` to specify a decreasing measure.
+-/
+#guard_msgs in
+def Foo.bar : {n: Nat} → Foo n → Foo n
+| _, foo f => (f 0).bar
+
+-- it works
+def Foo.bar' {n: Nat} : Foo n → Foo n
+| foo f => (f 0).bar'

tests/lean/run/issue2113.lean

@@ -0,0 +1,5 @@
+inductive Foo {f: Nat}: {d: Nat} → (h: d ≤ f) → Type where
+| foo : Foo (Nat.zero_le _) → (Bool → Foo h) → Foo h
+
+def Foo.bar (h: d ≤ f): Foo h → Foo h
+| foo _ f => (f true).bar h

tests/lean/run/issue4671.lean

@@ -4,17 +4,6 @@ inductive  A (n : Nat) : Type
   | a : A n
   | b : A n → A n
 
-/--
-error: cannot use specified measure for structural recursion:
-  its type is an inductive datatype
-    A n
-  and the datatype parameter
-    n
-  depends on the function parameter
-    n
-  which does not come before the varying parameters and before the indices of the recursion parameter.
--/
-#guard_msgs in
 def A.size (acc n : Nat) : A n → Nat
   | .a => acc
   | .b a' => 1 + A.size (acc + 1) n a'
@@ -27,17 +16,6 @@ inductive Xn (e : Sigma.{0} (· → Type)) (α : Type) : Nat → Type where
 | mk1_S {n} (x : Xn e α n) : Xn e α (n+1)
 | mk2 {n} (s : e.1) (p : e.2 s → Xn e α n) : Xn e α n
 
-/--
-error: cannot use specified measure for structural recursion:
-  its type is an inductive datatype
-    Xn e (Xn e α n) m
-  and the datatype parameter
-    Xn e α n
-  depends on the function parameter
-    n
-  which does not come before the varying parameters and before the indices of the recursion parameter.
--/
-#guard_msgs in
 def Xn.zip {e α m n} : Xn e (Xn e α n) m → Xn e α (n+m+1)
   | .mk1_S x => .mk1_S x.zip
   | .mk2 s p => .mk2 s fun a => (p a).zip

tests/lean/run/issue6281.lean

@@ -6,6 +6,8 @@ def f (n : Nat) (hn : n % 2 = 1) (m : Nat) (hm : (n + m) % 2 = 1) : Nat :=
     | 0 => 1
     | m' + 1 => f n' (by sorry) m' (by sorry)
 
+set_option pp.proofs true
+
 /--
 info: f.induct (motive : (n : Nat) → n % 2 = 1 → (m : Nat) → (n + m) % 2 = 1 → Prop)
   (case1 : ∀ (m : Nat) (hn : 1 % 2 = 1) (hm : (1 + m) % 2 = 1), motive 1 hn m hm)
@@ -14,7 +16,8 @@ info: f.induct (motive : (n : Nat) → n % 2 = 1 → (m : Nat) → (n + m) % 2 =
       (n' + 3 + 0) % 2 = 1 → motive n'.succ.succ.succ hn 0 hm)
   (case3 :
     ∀ (n' : Nat) (hn : (n' + 3) % 2 = 1) (m' : Nat) (hm : (n' + 3 + (m' + 1)) % 2 = 1),
-      (n' + 3 + m'.succ) % 2 = 1 → motive n' ⋯ m' ⋯ → motive n'.succ.succ.succ hn m'.succ hm)
+      (n' + 3 + m'.succ) % 2 = 1 →
+        motive n' (f.proof_1 n') m' (f.proof_2 n' m') → motive n'.succ.succ.succ hn m'.succ hm)
   (n : Nat) (hn : n % 2 = 1) (m : Nat) (hm : (n + m) % 2 = 1) : motive n hn m hm
 -/
 #guard_msgs in

tests/lean/run/omega.lean

@@ -520,54 +520,6 @@ example
     n = 65536 := by
   bv_omega
 
--- From https://github.com/leanprover/lean4/issues/5315
--- This used to fail with an unexpected bound variable error.
-
-def simple_foldl (f: β → α → β) (a: Array α) (i: Nat) (b: β): β :=
-  if h: i < a.size then
-    simple_foldl f a (i+1) (f b a[i])
-  else
-    b
-
-/--
-error: omega could not prove the goal:
-No usable constraints found. You may need to unfold definitions so `omega` can see linear arithmetic facts about `Nat` and `Int`, which may also involve multiplication, division, and modular remainder by constants.
--/
-#guard_msgs in
-theorem simple_fold_monotonic₁ (a: Array α) (f: β → α → β) (i: Nat) {P: α → β → Prop} {x: α}
-  (base: P x b)
-  (mono: ∀ x x' y, P x y → P x (f y x')): P x (simple_foldl f a i b) := by
-    unfold simple_foldl
-    split <;> try trivial
-    apply simple_fold_monotonic₁
-    . apply mono; exact base
-    . exact mono
-  termination_by a.size - i
-  decreasing_by
-    exfalso
-    rename_i a b
-    clear a b mono base
-    rename_i a; clear a
-    clear base
-    clear x
-    rename_i a; clear a
-    clear x
-    clear P
-    rename_i a; clear a
-    clear P
-    clear i
-    rename_i a; clear a
-    clear i
-    clear f
-    rename_i a; clear a
-    clear f
-    clear a
-    rename_i a; clear a
-    clear a
-    clear b
-    rename_i a
-    omega
-
 /-! ### Error messages -/
 
 /--

tests/lean/run/partial_fixpoint_induct.lean

@@ -72,29 +72,29 @@ partial_fixpoint
 end
 
 /--
-info: dependent2''a.fixpoint_induct (m : Nat) (motive_1 : (Nat → (b : Bool) → if b = true then Nat else Bool) → Prop)
-  (motive_2 : (Nat → Nat → (b : Bool) → if b = true then Nat else Bool) → Prop)
-  (motive_3 : (Fin (m + 1) → Nat → (b : Bool) → if b = true then Nat else Bool) → Prop)
-  (adm_1 : Lean.Order.admissible motive_1) (adm_2 : Lean.Order.admissible motive_2)
-  (adm_3 : Lean.Order.admissible motive_3)
+info: dependent2''a.fixpoint_induct (m : Nat) (b : Bool) (motive_1 : (Nat → if b = true then Nat else Bool) → Prop)
+  (motive_2 : (Nat → Nat → if b = true then Nat else Bool) → Prop)
+  (motive_3 : (Fin (m + 1) → Nat → if b = true then Nat else Bool) → Prop) (adm_1 : Lean.Order.admissible motive_1)
+  (adm_2 : Lean.Order.admissible motive_2) (adm_3 : Lean.Order.admissible motive_3)
   (h_1 :
-    ∀ (dependent2''a : Nat → (b : Bool) → if b = true then Nat else Bool)
-      (dependent2''b : Nat → Nat → (b : Bool) → if b = true then Nat else Bool),
+    ∀ (dependent2''a : Nat → if b = true then Nat else Bool)
+      (dependent2''b : Nat → Nat → if b = true then Nat else Bool),
       motive_1 dependent2''a →
         motive_2 dependent2''b →
-          motive_1 fun n b => if x : b = true then dependent2''a (n + 1) b else dependent2''b m (n + m) b)
+          motive_1 fun n => if x : b = true then dependent2''a (n + 1) else dependent2''b m (n + m))
   (h_2 :
-    ∀ (dependent2''b : Nat → Nat → (b : Bool) → if b = true then Nat else Bool)
-      (dependent2''c : Fin (m + 1) → Nat → (b : Bool) → if b = true then Nat else Bool),
+    ∀ (dependent2''b : Nat → Nat → if b = true then Nat else Bool)
+      (dependent2''c : Fin (m + 1) → Nat → if b = true then Nat else Bool),
       motive_2 dependent2''b →
         motive_3 dependent2''c →
-          motive_2 fun k n b => if b = true then dependent2''b k n b else dependent2''c (Fin.last m) (n + m) b)
+          motive_2 fun k n => if b = true then dependent2''b k n else dependent2''c (Fin.last m) (n + m))
   (h_3 :
-    ∀ (dependent2''a : Nat → (b : Bool) → if b = true then Nat else Bool)
-      (dependent2''c : Fin (m + 1) → Nat → (b : Bool) → if b = true then Nat else Bool),
+    ∀ (dependent2''a : Nat → if b = true then Nat else Bool)
+      (dependent2''c : Fin (m + 1) → Nat → if b = true then Nat else Bool),
       motive_1 dependent2''a →
-        motive_3 dependent2''c → motive_3 fun i n b => if b = true then dependent2''c i n b else dependent2''a (↑i) b) :
-  motive_1 (dependent2''a m) ∧ motive_2 (dependent2''b m) ∧ motive_3 (dependent2''c m)
+        motive_3 dependent2''c → motive_3 fun i n => if b = true then dependent2''c i n else dependent2''a ↑i) :
+  (motive_1 fun n => dependent2''a m n b) ∧
+    (motive_2 fun k n => dependent2''b m k n b) ∧ motive_3 fun i n => dependent2''c m i n b
 -/
 #guard_msgs in #check dependent2''a.fixpoint_induct
 
@@ -115,38 +115,36 @@ partial_fixpoint
 end
 
 /--
-info: dependent3''a.partial_correctness (m : Nat) (motive_1 : Nat → (b : Bool) → (if b = true then Nat else Bool) → Prop)
-  (motive_2 : Nat → Nat → (b : Bool) → (if b = true then Nat else Bool) → Prop)
-  (motive_3 : Fin (m + 1) → Nat → (b : Bool) → (if b = true then Nat else Bool) → Prop)
+info: dependent3''a.partial_correctness (m : Nat) (b : Bool) (motive_1 : Nat → (if b = true then Nat else Bool) → Prop)
+  (motive_2 : Nat → Nat → (if b = true then Nat else Bool) → Prop)
+  (motive_3 : Fin (m + 1) → Nat → (if b = true then Nat else Bool) → Prop)
   (h_1 :
-    ∀ (dependent3''a : Nat → (b : Bool) → Option (if b = true then Nat else Bool))
-      (dependent3''b : Nat → Nat → (b : Bool) → Option (if b = true then Nat else Bool)),
-      (∀ (n : Nat) (b : Bool) (r : if b = true then Nat else Bool), dependent3''a n b = some r → motive_1 n b r) →
-        (∀ (k n : Nat) (b : Bool) (r : if b = true then Nat else Bool),
-            dependent3''b k n b = some r → motive_2 k n b r) →
-          ∀ (n : Nat) (b : Bool) (r : if b = true then Nat else Bool),
-            (if x : b = true then dependent3''a (n + 1) b else dependent3''b m (n + m) b) = some r → motive_1 n b r)
+    ∀ (dependent3''a : Nat → Option (if b = true then Nat else Bool))
+      (dependent3''b : Nat → Nat → Option (if b = true then Nat else Bool)),
+      (∀ (n : Nat) (r : if b = true then Nat else Bool), dependent3''a n = some r → motive_1 n r) →
+        (∀ (k n : Nat) (r : if b = true then Nat else Bool), dependent3''b k n = some r → motive_2 k n r) →
+          ∀ (n : Nat) (r : if b = true then Nat else Bool),
+            (if x : b = true then dependent3''a (n + 1) else dependent3''b m (n + m)) = some r → motive_1 n r)
   (h_2 :
-    ∀ (dependent3''b : Nat → Nat → (b : Bool) → Option (if b = true then Nat else Bool))
-      (dependent3''c : Fin (m + 1) → Nat → (b : Bool) → Option (if b = true then Nat else Bool)),
-      (∀ (k n : Nat) (b : Bool) (r : if b = true then Nat else Bool), dependent3''b k n b = some r → motive_2 k n b r) →
-        (∀ (i : Fin (m + 1)) (n : Nat) (b : Bool) (r : if b = true then Nat else Bool),
-            dependent3''c i n b = some r → motive_3 i n b r) →
-          ∀ (k n : Nat) (b : Bool) (r : if b = true then Nat else Bool),
-            (if b = true then dependent3''b k n b else dependent3''c (Fin.last m) (n + m) b) = some r →
-              motive_2 k n b r)
+    ∀ (dependent3''b : Nat → Nat → Option (if b = true then Nat else Bool))
+      (dependent3''c : Fin (m + 1) → Nat → Option (if b = true then Nat else Bool)),
+      (∀ (k n : Nat) (r : if b = true then Nat else Bool), dependent3''b k n = some r → motive_2 k n r) →
+        (∀ (i : Fin (m + 1)) (n : Nat) (r : if b = true then Nat else Bool),
+            dependent3''c i n = some r → motive_3 i n r) →
+          ∀ (k n : Nat) (r : if b = true then Nat else Bool),
+            (if b = true then dependent3''b k n else dependent3''c (Fin.last m) (n + m)) = some r → motive_2 k n r)
   (h_3 :
-    ∀ (dependent3''a : Nat → (b : Bool) → Option (if b = true then Nat else Bool))
-      (dependent3''c : Fin (m + 1) → Nat → (b : Bool) → Option (if b = true then Nat else Bool)),
-      (∀ (n : Nat) (b : Bool) (r : if b = true then Nat else Bool), dependent3''a n b = some r → motive_1 n b r) →
-        (∀ (i : Fin (m + 1)) (n : Nat) (b : Bool) (r : if b = true then Nat else Bool),
-            dependent3''c i n b = some r → motive_3 i n b r) →
-          ∀ (i : Fin (m + 1)) (n : Nat) (b : Bool) (r : if b = true then Nat else Bool),
-            (if b = true then dependent3''c i n b else dependent3''a (↑i) b) = some r → motive_3 i n b r) :
-  (∀ (n : Nat) (b : Bool) (r : if b = true then Nat else Bool), dependent3''a m n b = some r → motive_1 n b r) ∧
-    (∀ (k n : Nat) (b : Bool) (r : if b = true then Nat else Bool), dependent3''b m k n b = some r → motive_2 k n b r) ∧
-      ∀ (i : Fin (m + 1)) (n : Nat) (b : Bool) (r : if b = true then Nat else Bool),
-        dependent3''c m i n b = some r → motive_3 i n b r
+    ∀ (dependent3''a : Nat → Option (if b = true then Nat else Bool))
+      (dependent3''c : Fin (m + 1) → Nat → Option (if b = true then Nat else Bool)),
+      (∀ (n : Nat) (r : if b = true then Nat else Bool), dependent3''a n = some r → motive_1 n r) →
+        (∀ (i : Fin (m + 1)) (n : Nat) (r : if b = true then Nat else Bool),
+            dependent3''c i n = some r → motive_3 i n r) →
+          ∀ (i : Fin (m + 1)) (n : Nat) (r : if b = true then Nat else Bool),
+            (if b = true then dependent3''c i n else dependent3''a ↑i) = some r → motive_3 i n r) :
+  (∀ (n : Nat) (r : if b = true then Nat else Bool), dependent3''a m n b = some r → motive_1 n r) ∧
+    (∀ (k n : Nat) (r : if b = true then Nat else Bool), dependent3''b m k n b = some r → motive_2 k n r) ∧
+      ∀ (i : Fin (m + 1)) (n : Nat) (r : if b = true then Nat else Bool),
+        dependent3''c m i n b = some r → motive_3 i n r
 -/
 #guard_msgs in #check dependent3''a.partial_correctness
 
@@ -162,25 +160,25 @@ def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := match xs wit
 partial_fixpoint
 
 /--
-info: List.findIndex.partial_correctness.{u_1} {α : Type u_1} (motive : List α → (α → Bool) → Nat → Prop)
+info: List.findIndex.partial_correctness.{u_1} {α : Type u_1} (p : α → Bool) (motive : List α → Nat → Prop)
   (h :
-    ∀ (findIndex : List α → (α → Bool) → Option Nat),
-      (∀ (xs : List α) (p : α → Bool) (r : Nat), findIndex xs p = some r → motive xs p r) →
-        ∀ (xs : List α) (p : α → Bool) (r : Nat),
+    ∀ (findIndex : List α → Option Nat),
+      (∀ (xs : List α) (r : Nat), findIndex xs = some r → motive xs r) →
+        ∀ (xs : List α) (r : Nat),
           (match xs with
               | [] => none
-              | x :: ys => if p x = true then some 0 else (fun x => x + 1) <$> findIndex ys p) =
+              | x :: ys => if p x = true then some 0 else (fun x => x + 1) <$> findIndex ys) =
               some r →
-            motive xs p r)
-  (xs : List α) (p : α → Bool) (r✝ : Nat) : xs.findIndex p = some r✝ → motive xs p r✝
+            motive xs r)
+  (xs : List α) (r✝ : Nat) : xs.findIndex p = some r✝ → motive xs r✝
 -/
 #guard_msgs in
 #check List.findIndex.partial_correctness
 
 theorem List.findIndex_implies_pred (xs : List α) (p : α → Bool) :
     xs.findIndex p = some i → xs[i]?.any p := by
-  apply List.findIndex.partial_correctness (motive := fun xs p i => xs[i]?.any p)
-  intro findIndex ih xs p r hsome
+  apply List.findIndex.partial_correctness (motive := fun xs i => xs[i]?.any p)
+  intro findIndex ih xs r hsome
   split at hsome
   next => contradiction
   next x ys =>
@@ -191,5 +189,5 @@ theorem List.findIndex_implies_pred (xs : List α) (p : α → Bool) :
     next =>
       simp only [Option.map_eq_map, Option.map_eq_some'] at hsome
       obtain ⟨r', hr, rfl⟩ := hsome
-      specialize ih _ _ _ hr
+      specialize ih _ _ hr
       simpa

tests/lean/run/structuralMutual.lean

@@ -414,17 +414,6 @@ inductive  B (n : Nat) : Type
   | a : A n → B n
 end
 
-/--
-error: cannot use specified measure for structural recursion:
-  its type is an inductive datatype
-    A n
-  and the datatype parameter
-    n
-  depends on the function parameter
-    n
-  which does not come before the varying parameters and before the indices of the recursion parameter.
--/
-#guard_msgs in
 set_option linter.constructorNameAsVariable false in
 mutual
 def A.size (n : Nat) (m : Nat) : A n → Nat
@@ -460,14 +449,11 @@ inductive T (n : Nat) : Nat → Type where
   | n : T n n → T n n
 
 /--
-error: cannot use specified measure for structural recursion:
-  its type is an inductive datatype
-    T n n
-  and the datatype parameter
+error: failed to infer structural recursion:
+Cannot use parameter #2:
+  its type is an inductive datatype and the datatype parameter
     n
-  depends on the function parameter
-    n
-  which does not come before the varying parameters and before the indices of the recursion parameter.
+  which cannot be fixed as it is an index or depends on an index, and indices cannot be fixed parameters when using structural recursion.
 -/
 #guard_msgs in
 def T.a {n : Nat} : T n n → Nat
@@ -525,18 +511,18 @@ Too many possible combinations of parameters of type Nattish (or please indicate
 Could not find a decreasing measure.
 The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
-Call from ManyCombinations.f to ManyCombinations.g at 557:15-29:
+Call from ManyCombinations.f to ManyCombinations.g at 543:15-29:
    #1 #2 #3 #4
 #5  ?  ?  ?  ?
-#6  ?  =  ?  ?
-#7  ?  ?  =  ?
-#8  ?  ?  ?  =
-Call from ManyCombinations.g to ManyCombinations.f at 560:15-29:
+#6  ?  ?  =  ?
+#7  ?  ?  ?  =
+#8  ?  =  ?  ?
+Call from ManyCombinations.g to ManyCombinations.f at 546:15-29:
    #5 #6 #7 #8
 #1  _  _  _  _
-#2  _  =  _  _
-#3  _  _  =  _
-#4  _  _  _  =
+#2  _  _  _  ?
+#3  _  ?  _  _
+#4  _  _  ?  _
 
 
 #1: sizeOf a
@@ -554,7 +540,7 @@ Please use `termination_by` to specify a decreasing measure.
 mutual
 def f (a b c d : Nattish) : Nat := match a with
   | .zero => 0
-  | .cons n => g (n 23) b c d
+  | .cons n => g (n 23) c d b
 def g (a b c d : Nattish) : Nat := match a with
   | .zero => 0
   | .cons n => f (n 42) b c d

tests/lean/run/structuralRec2.lean

@@ -0,0 +1,37 @@
+/-!
+More tests related to structural indices depending on fixed parameters
+-/
+
+inductive T (n : Nat) : Nat → Type where
+  | zero : T n 0
+  | succ {i} : T n i  → T n (i + n) → T n i
+
+
+/--
+error: cannot use specified measure for structural recursion:
+  its type is an inductive datatype
+    T (↑f) i
+  and the datatype parameter
+    ↑f
+  depends on the function parameter
+    i
+  which is not fixed.
+-/
+#guard_msgs in
+def foo (i : Nat) (f : Fin i) : T f i → Unit
+  | .zero => ()
+  | .succ t _ => foo i f t
+termination_by structural t => t
+
+def bar (a : Nat) (i : Nat) (f : Fin a) : T f i → Unit
+  | .zero => ()
+  | .succ t _ => bar a i f t
+termination_by structural t => t
+
+/--
+info: bar.induct (a : Nat) (f : Fin a) (motive : (i : Nat) → T (↑f) i → Prop) (case1 : motive 0 T.zero)
+  (case2 : ∀ (i : Nat) (t : T (↑f) i) (a_1 : T (↑f) (i + ↑f)), motive i t → motive i (t.succ a_1)) (i : Nat)
+  (a✝ : T (↑f) i) : motive i a✝
+-/
+#guard_msgs in
+#check bar.induct

tests/lean/wf2.lean.expected.out

@@ -2,6 +2,6 @@ wf2.lean:3:8-3:17: error: failed to prove termination, possible solutions:
   - Use `have`-expressions to prove the remaining goals
   - Use `termination_by` to specify a different well-founded relation
   - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
-x y : Nat
+y x : Nat
 h✝ : x < y
 ⊢ x - 1 < x