Type annotations help more and more

but I am a bit stuck/confused in `src/lake/Lake/DSL/DeclUtil.lean`

src/Lean/Elab/Binders.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 import Lean.Elab.Quotation.Precheck
 import Lean.Elab.Term
 import Lean.Elab.BindersUtil
+import Lean.Elab.PreDefinition.WF.TerminationHint
 
 namespace Lean.Elab.Term
 open Meta
@@ -570,7 +571,8 @@ def expandMatchAltsIntoMatchTactic (ref : Syntax) (matchAlts : Syntax) : MacroM
 -/
 def expandMatchAltsWhereDecls (matchAltsWhereDecls : Syntax) : MacroM Syntax :=
   let matchAlts     := matchAltsWhereDecls[0]
-  let whereDeclsOpt := matchAltsWhereDecls[1]
+  -- matchAltsWhereDecls[1] is the termination hints, collected elsewhere
+  let whereDeclsOpt := matchAltsWhereDecls[2]
   let rec loop (i : Nat) (discrs : Array Syntax) : MacroM Syntax :=
     match i with
     | 0   => do

src/Lean/Elab/Declaration.lean

@@ -187,15 +187,6 @@ def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Uni
   let v ← classInductiveSyntaxToView modifiers stx
   elabInductiveViews #[v]
 
-def getTerminationHints (stx : Syntax) : TerminationHints :=
-  let decl := stx[1]
-  let k := decl.getKind
-  if k == ``Parser.Command.def || k == ``Parser.Command.abbrev || k == ``Parser.Command.theorem || k == ``Parser.Command.instance then
-    let args := decl.getArgs
-    { terminationBy? := args[args.size - 2]!.getOptional?, decreasingBy? := args[args.size - 1]!.getOptional? }
-  else
-    {}
-
 @[builtin_command_elab declaration]
 def elabDeclaration : CommandElab := fun stx => do
   match (← liftMacroM <| expandDeclNamespace? stx) with
@@ -219,7 +210,7 @@ def elabDeclaration : CommandElab := fun stx => do
       let modifiers ← elabModifiers stx[0]
       elabStructure modifiers decl
     else if isDefLike decl then
-      elabMutualDef #[stx] (getTerminationHints stx)
+      elabMutualDef #[stx]
     else
       throwError "unexpected declaration"
 
@@ -332,21 +323,10 @@ def expandMutualPreamble : Macro := fun stx =>
 
 @[builtin_command_elab «mutual»]
 def elabMutual : CommandElab := fun stx => do
-  let hints := { terminationBy? := stx[3].getOptional?, decreasingBy? := stx[4].getOptional? }
   if isMutualInductive stx then
-    if let some bad := hints.terminationBy? then
-      throwErrorAt bad "invalid 'termination_by' in mutually inductive datatype declaration"
-    if let some bad := hints.decreasingBy? then
-      throwErrorAt bad "invalid 'decreasing_by' in mutually inductive datatype declaration"
     elabMutualInductive stx[1].getArgs
   else if isMutualDef stx then
-    for arg in stx[1].getArgs do
-      let argHints := getTerminationHints arg
-      if let some bad := argHints.terminationBy? then
-        throwErrorAt bad "invalid 'termination_by' in 'mutual' block, it must be used after the 'end' keyword"
-      if let some bad := argHints.decreasingBy? then
-        throwErrorAt bad "invalid 'decreasing_by' in 'mutual' block, it must be used after the 'end' keyword"
-    elabMutualDef stx[1].getArgs hints
+    elabMutualDef stx[1].getArgs
   else
     throwError "invalid mutual block: either all elements of the block must be inductive declarations, or they must all be definitions/theorems/abbrevs"
 

src/Lean/Elab/DefView.lean

@@ -127,7 +127,7 @@ def mkDefViewOfOpaque (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefV
       pure <| mkNode ``Parser.Command.declValSimple #[ mkAtomFrom stx ":=", val ]
   return {
     ref := stx, kind := DefKind.opaque, modifiers := modifiers,
-    declId := stx[1], binders := binders, type? := some type, value := val
+    declId := stx[1], binders := binders, type? := some type, value := val,
   }
 
 def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView :=

src/Lean/Elab/LetRec.lean

@@ -21,6 +21,7 @@ structure LetRecDeclView where
   type          : Expr
   mvar          : Expr -- auxiliary metavariable used to lift the 'let rec'
   valStx        : Syntax
+  termination   : WF.TerminationHints
 
 structure LetRecView where
   decls     : Array LetRecDeclView
@@ -59,7 +60,10 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
         pure decl[4]
       else
         liftMacroM <| expandMatchAltsIntoMatch decl decl[3]
-      pure { ref := declId, attrs, shortDeclName, declName, binderIds, type, mvar, valStx : LetRecDeclView }
+      -- TODO: Is this right?
+      let termination := WF.elabTerminationHints ⟨attrDeclStx[3]⟩
+      pure {
+        ref := declId, attrs, shortDeclName, declName, binderIds, type, mvar, valStx, termination : LetRecDeclView }
     else
       throwUnsupportedSyntax
   return { decls, body := letRec[3] }
@@ -102,6 +106,7 @@ private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array
     type           := view.type
     val            := values[i]!
     mvarId         := view.mvar.mvarId!
+    termination    := view.termination
     : LetRecToLift }
   modify fun s => { s with letRecsToLift := toLift.toList ++ s.letRecsToLift }
 

src/Lean/Elab/MutualDef.lean

@@ -13,6 +13,7 @@ import Lean.Elab.Match
 import Lean.Elab.DefView
 import Lean.Elab.Deriving.Basic
 import Lean.Elab.PreDefinition.Main
+import Lean.Elab.PreDefinition.WF.TerminationHint
 import Lean.Elab.DeclarationRange
 
 namespace Lean.Elab
@@ -228,7 +229,7 @@ def declVal          := declValSimple <|> declValEqns <|> Term.whereDecls
 -/
 private def declValToTerm (declVal : Syntax) : MacroM Syntax := withRef declVal do
   if declVal.isOfKind ``Parser.Command.declValSimple then
-    expandWhereDeclsOpt declVal[2] declVal[1]
+    expandWhereDeclsOpt declVal[3] declVal[1]
   else if declVal.isOfKind ``Parser.Command.declValEqns then
     expandMatchAltsWhereDecls declVal[0]
   else if declVal.isOfKind ``Parser.Command.whereStructInst then
@@ -238,6 +239,14 @@ private def declValToTerm (declVal : Syntax) : MacroM Syntax := withRef declVal
   else
     Macro.throwErrorAt declVal "unexpected declaration body"
 
+private def declValToTerminationHint (declVal : Syntax) : WF.TerminationHints :=
+  if declVal.isOfKind ``Parser.Command.declValSimple then
+    WF.elabTerminationHints ⟨declVal[2]⟩
+  else if declVal.isOfKind ``Parser.Command.declValEqns then
+    WF.elabTerminationHints ⟨declVal[0][1]⟩
+  else
+    .none
+
 private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array Expr) :=
   headers.mapM fun header => withDeclName header.declName <| withLevelNames header.levelNames do
     let valStx ← liftMacroM <| declValToTerm header.valueStx
@@ -625,7 +634,9 @@ def Replacement.apply (r : Replacement) (e : Expr) : Expr :=
       | _      => none
     | _ => none
 
-def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mainVals : Array Expr)
+def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr)
+    (mainHeaders : Array DefViewElabHeader) (mainVals : Array Expr)
+    (terminations : Array WF.TerminationHints)
     : TermElabM (Array PreDefinition) :=
   mainHeaders.size.foldM (init := preDefs) fun i preDefs => do
     let header := mainHeaders[i]!
@@ -637,7 +648,8 @@ def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr) (mainHea
       declName    := header.declName
       levelParams := [], -- we set it later
       modifiers   := header.modifiers
-      type, value
+      type, value,
+      termination := terminations[i]!
     }
 
 def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClosure) (kind : DefKind) (modifiers : Modifiers) : MetaM (Array PreDefinition) :=
@@ -655,7 +667,8 @@ def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClo
       declName    := c.toLift.declName
       levelParams := [] -- we set it later
       modifiers   := { modifiers with attrs := c.toLift.attrs }
-      kind, type, value
+      kind, type, value,
+      termination := c.toLift.termination
     }
 
 def getKindForLetRecs (mainHeaders : Array DefViewElabHeader) : DefKind :=
@@ -675,7 +688,9 @@ def getModifiersForLetRecs (mainHeaders : Array DefViewElabHeader) : Modifiers :
 - `mainVals`:      The elaborated value for the top-level definitions
 - `letRecsToLift`: The let-rec's definitions that need to be lifted
 -/
-def main (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mainFVars : Array Expr) (mainVals : Array Expr) (letRecsToLift : List LetRecToLift)
+def main (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mainFVars : Array Expr)
+    (mainVals : Array Expr) (letRecsToLift : List LetRecToLift)
+    (terminations : Array WF.TerminationHints)
     : TermElabM (Array PreDefinition) := do
   -- Store in recFVarIds the fvarId of every function being defined by the mutual block.
   let letRecsToLift := letRecsToLift.toArray
@@ -701,7 +716,7 @@ def main (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mai
     let letRecClosures := letRecClosures.map fun c => { c with toLift := { c.toLift with type := r.apply c.toLift.type, val := r.apply c.toLift.val } }
     let letRecKind     := getKindForLetRecs mainHeaders
     let letRecMods     := getModifiersForLetRecs mainHeaders
-    pushMain (← pushLetRecs #[] letRecClosures letRecKind letRecMods) sectionVars mainHeaders mainVals
+    pushMain (← pushLetRecs #[] letRecClosures letRecKind letRecMods) sectionVars mainHeaders mainVals terminations
 
 end MutualClosure
 
@@ -766,7 +781,7 @@ partial def checkForHiddenUnivLevels (allUserLevelNames : List Name) (preDefs :
     for preDef in preDefs do
       checkPreDef preDef
 
-def elabMutualDef (vars : Array Expr) (views : Array DefView) (hints : TerminationHints) : TermElabM Unit :=
+def elabMutualDef (vars : Array Expr) (views : Array DefView) : TermElabM Unit :=
   if isExample views then
     withoutModifyingEnv do
       -- save correct environment in info tree
@@ -780,6 +795,7 @@ where
     let headers ← elabHeaders views
     let headers ← levelMVarToParamHeaders views headers
     let allUserLevelNames := getAllUserLevelNames headers
+    let terminations := views.map (declValToTerminationHint ·.value)
     withFunLocalDecls headers fun funFVars => do
       for view in views, funFVar in funFVars do
         addLocalVarInfo view.declId funFVar
@@ -796,7 +812,7 @@ where
       let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
       checkLetRecsToLiftTypes funFVars letRecsToLift
       withUsed vars headers values letRecsToLift fun vars => do
-        let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
+        let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift terminations
         for preDef in preDefs do
           trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
         let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamPreDecls preDefs
@@ -805,7 +821,7 @@ where
         for preDef in preDefs do
           trace[Elab.definition] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}"
         checkForHiddenUnivLevels allUserLevelNames preDefs
-        addPreDefinitions preDefs hints
+        addPreDefinitions preDefs
         processDeriving headers
 
   processDeriving (headers : Array DefViewElabHeader) := do
@@ -820,13 +836,13 @@ where
 end Term
 namespace Command
 
-def elabMutualDef (ds : Array Syntax) (hints : TerminationHints) : CommandElabM Unit := do
+def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
   let views ← ds.mapM fun d => do
     let modifiers ← elabModifiers d[0]
     if ds.size > 1 && modifiers.isNonrec then
       throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block"
     mkDefView modifiers d[1]
-  runTermElabM fun vars => Term.elabMutualDef vars views hints
+  runTermElabM fun vars => Term.elabMutualDef vars views
 
 end Command
 end Lean.Elab

src/Lean/Elab/PreDefinition/Basic.lean

@@ -8,11 +8,13 @@ import Lean.Util.CollectLevelParams
 import Lean.Meta.AbstractNestedProofs
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.DefView
+import Lean.Elab.PreDefinition.WF.TerminationHint
 
 namespace Lean.Elab
 open Meta
 open Term
 
+
 /--
   A (potentially recursive) definition.
   The elaborator converts it into Kernel definitions using many different strategies.
@@ -25,6 +27,7 @@ structure PreDefinition where
   declName    : Name
   type        : Expr
   value       : Expr
+  termination : WF.TerminationHints
   deriving Inhabited
 
 def instantiateMVarsAtPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) :=

src/Lean/Elab/PreDefinition/Main.lean

@@ -13,10 +13,8 @@ namespace Lean.Elab
 open Meta
 open Term
 
-structure TerminationHints where
-  terminationBy? : Option Syntax := none
-  decreasingBy? : Option Syntax := none
-  deriving Inhabited
+/-- All termination hints for a given clique -/
+def TerminationHints := Array (TSyntax ``Parser.Termination.suffix)
 
 private def addAndCompilePartial (preDefs : Array PreDefinition) (useSorry := false) : TermElabM Unit := do
   for preDef in preDefs do
@@ -94,15 +92,12 @@ private def addAsAxioms (preDefs : Array PreDefinition) : TermElabM Unit := do
     applyAttributesOf #[preDef] AttributeApplicationTime.afterTypeChecking
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
 
-def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints) : TermElabM Unit := withLCtx {} {} do
+def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLCtx {} {} do
   for preDef in preDefs do
     trace[Elab.definition.body] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
   let preDefs ← preDefs.mapM ensureNoUnassignedMVarsAtPreDef
   let preDefs ← betaReduceLetRecApps preDefs
   let cliques := partitionPreDefs preDefs
-  let mut terminationBy ← liftMacroM <| WF.expandTerminationBy? hints.terminationBy? (cliques.map fun ds => ds.map (·.declName))
-  let mut decreasingBy  ← liftMacroM <| WF.expandDecreasingBy? hints.decreasingBy? (cliques.map fun ds => ds.map (·.declName))
-  let mut hasErrors := false
   for preDefs in cliques do
     trace[Elab.definition.scc] "{preDefs.map (·.declName)}"
     if preDefs.size == 1 && isNonRecursive preDefs[0]! then
@@ -116,35 +111,31 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints)
         addNonRec preDef
       else
         addAndCompileNonRec preDef
+      -- TODO: Complain about possible termination hints
     else if preDefs.any (·.modifiers.isUnsafe) then
       addAndCompileUnsafe preDefs
+      -- TODO: Complain about possible termination hints
     else if preDefs.any (·.modifiers.isPartial) then
       for preDef in preDefs do
         if preDef.modifiers.isPartial && !(← whnfD preDef.type).isForall then
           withRef preDef.ref <| throwError "invalid use of 'partial', '{preDef.declName}' is not a function{indentExpr preDef.type}"
       addAndCompilePartial preDefs
+      -- TODO: Complain about possible termination hints
     else
       try
-        let mut wf? := none
-        let mut decrTactic? := none
-        if let some wf := terminationBy.find? (preDefs.map (·.declName)) then
-          wf? := some wf
-          terminationBy := terminationBy.markAsUsed (preDefs.map (·.declName))
-        if let some { ref, value := decrTactic } := decreasingBy.find? (preDefs.map (·.declName)) then
-          decrTactic? := some (← withRef ref `(by $(⟨decrTactic⟩)))
-          decreasingBy := decreasingBy.markAsUsed (preDefs.map (·.declName))
-        if wf?.isSome || decrTactic?.isSome then
-          wfRecursion preDefs wf? decrTactic?
+        let hasHints := preDefs.any  fun preDef =>
+          preDef.termination.decreasing_by?.isSome || preDef.termination.termination_by?.isSome
+        if hasHints then
+          wfRecursion preDefs
         else
           withRef (preDefs[0]!.ref) <| mapError
             (orelseMergeErrors
               (structuralRecursion preDefs)
-              (wfRecursion preDefs none none))
+              (wfRecursion preDefs))
             (fun msg =>
               let preDefMsgs := preDefs.toList.map (MessageData.ofExpr $ mkConst ·.declName)
               m!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}")
       catch ex =>
-        hasErrors := true
         logException ex
         let s ← saveState
         try
@@ -159,9 +150,6 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints)
           else if preDefs.all fun preDef => preDef.kind == DefKind.theorem then
             addAsAxioms preDefs
         catch _ => s.restore
-  unless hasErrors do
-    liftMacroM <| terminationBy.ensureAllUsed
-    liftMacroM <| decreasingBy.ensureAllUsed
 
 builtin_initialize
   registerTraceClass `Elab.definition.body

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

@@ -13,6 +13,7 @@ import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
 import Lean.Elab.PreDefinition.Structural.BRecOn
+import Lean.Elab.PreDefinition.WF.PackMutual
 import Lean.Data.Array
 
 namespace Lean.Elab.WF
@@ -186,22 +187,47 @@ def assignSubsumed (mvars : Array MVarId) : MetaM (Array MVarId) :=
           return (false, true)
     return (true, true)
 
-def solveDecreasingGoals (decrTactic? : Option Syntax) (value : Expr) : MetaM Expr := do
+/--
+The subgoals are of the form `rel arg param`, where `param` is the `PackMutual`'ed parameter
+of the current function, and thus we can peek at that to know which function is making the call.
+The close coupling with how arguments are packed and termination goals look like is not great,
+but it works for now.
+-/
+def groupGoalsByFunction (numFuncs : Nat) (goals : Array MVarId) : MetaM (Array (Array MVarId)) := do
+  let mut r := mkArray numFuncs #[]
+  for goal in goals do
+    let (.mdata _ (.app _ param)) ← goal.getType
+        | throwError "MVar does not look like like a recursive call"
+    let (funidx, _) ← unpackMutualArg numFuncs param
+    r := r.modify funidx (·.push goal)
+  return r
+
+def solveDecreasingGoals (decrTactics : Array (Option Syntax)) (value : Expr) : MetaM Expr := do
   let goals ← getMVarsNoDelayed value
   let goals ← assignSubsumed goals
-  goals.forM fun goal => Lean.Elab.Term.TermElabM.run' <|
+  let goalss ← groupGoalsByFunction decrTactics.size goals
+  for goals in goalss, decrTactic? in decrTactics do
+    Lean.Elab.Term.TermElabM.run' do
     match decrTactic? with
     | none => do
-      let some ref := getRecAppSyntax? (← goal.getType)
-        | throwError "MVar does not look like like a recursive call"
+      for goal in goals do
+        let some ref := getRecAppSyntax? (← goal.getType)
+          | throwError "MVar does not look like like a recursive call"
         withRef ref <| applyDefaultDecrTactic goal
     | some decrTactic => do
-      -- make info from `runTactic` available
-      pushInfoTree (.hole goal)
-      Term.runTactic goal decrTactic
+      unless goals.isEmpty do -- unlikely to be empty
+        -- TODO: What is this pushInfo Tree
+        -- make info from `runTactic` available
+        -- pushInfoTree (.hole goal)
+        let remainingGoals ← Tactic.run goals[0]! do
+          Tactic.setGoals goals.toList
+          Tactic.evalTactic decrTactic
+        unless remainingGoals.isEmpty do
+          Term.reportUnsolvedGoals remainingGoals
   instantiateMVars value
 
-def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (wfRel : Expr) (decrTactic? : Option Syntax) : TermElabM Expr := do
+def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (wfRel : Expr)
+    (decrTactics : Array (Option Syntax)) : TermElabM Expr := do
   let type ← instantiateForall preDef.type prefixArgs
   let (wfFix, varName) ← forallBoundedTelescope type (some 1) fun x type => do
     let x := x[0]!
@@ -224,7 +250,7 @@ def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (wfRel : Expr) (dec
       let val := preDef.value.beta (prefixArgs.push x)
       let val ← processSumCasesOn x F val fun x F val => do
         processPSigmaCasesOn x F val (replaceRecApps preDef.declName prefixArgs.size)
-      let val ← solveDecreasingGoals decrTactic? val
+      let val ← solveDecreasingGoals decrTactics val
       mkLambdaFVars prefixArgs (mkApp wfFix (← mkLambdaFVars #[x, F] val))
 
 end Lean.Elab.WF

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

@@ -14,6 +14,7 @@ import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
 import Lean.Elab.PreDefinition.WF.TerminationHint
+import Lean.Elab.PreDefinition.WF.PackMutual
 import Lean.Data.Array
 
 
@@ -263,38 +264,6 @@ def filterSubsumed (rcs : Array RecCallWithContext ) : Array RecCallWithContext
           return (false, true)
     return (true, true)
 
-/-- Given the packed argument of a (possibly) mutual and (possibly) nary call,
-return the function index that is called and the arguments individually.
-
-We expect precisely the expressions produced by `packMutual`, with manifest
-`PSum.inr`, `PSum.inl` and `PSigma.mk` constructors, and thus take them apart
-rather than using projectinos. -/
-def unpackArg {m} [Monad m] [MonadError m] (arities : Array Nat) (e : Expr) :
-    m (Nat × Array Expr) := do
-  -- count PSum injections to find out which function is doing the call
-  let mut funidx := 0
-  let mut e := e
-  while funidx + 1 < arities.size do
-    if e.isAppOfArity ``PSum.inr 3 then
-      e := e.getArg! 2
-      funidx := funidx + 1
-    else if e.isAppOfArity ``PSum.inl 3 then
-      e := e.getArg! 2
-      break
-    else
-      throwError "Unexpected expression while unpacking mutual argument"
-
-  -- now unpack PSigmas
-  let arity := arities[funidx]!
-  let mut args := #[]
-  while args.size + 1 < arity do
-    if e.isAppOfArity ``PSigma.mk 4 then
-      args := args.push (e.getArg! 2)
-      e := e.getArg! 3
-    else
-      throwError "Unexpected expression while unpacking n-ary argument"
-  args := args.push e
-  return (funidx, args)
 
 /-- Traverse a unary PreDefinition, and returns a `WithRecCall` closure for each recursive
 call site.
@@ -382,8 +351,11 @@ def evalRecCall (decrTactic? : Option Syntax) (rcc : RecCallWithContext) (paramI
             | some decrTactic => Term.withoutErrToSorry do
               -- make info from `runTactic` available
               pushInfoTree (.hole mvarId)
-              Term.runTactic mvarId decrTactic
-              -- trace[Elab.definition.wf] "Found {rel} proof: {← instantiateMVars mvar}"
+              let decrTacticSeq := ⟨decrTactic⟩
+              -- runTactic uses `syntax[1]`, so looks like we have to wrap it again.
+              -- TODO: Fully understand what’s going on here
+              Term.runTactic mvarId (← `(tactic|($decrTacticSeq:tacticSeq)))
+              trace[Elab.definition.wf] "Found {rel} proof with {decrTactic}: {← instantiateMVars mvar}"
               pure ()
         trace[Elab.definition.wf] "inspectRecCall: success!"
         return rel
@@ -399,8 +371,9 @@ structure RecCallCache where mk'' ::
   cache : IO.Ref (Array (Array (Option GuessLexRel)))
 
 /-- Create a cache to memoize calls to `evalRecCall descTactic? rcc` -/
-def RecCallCache.mk (decrTactic? : Option Syntax) (rcc : RecCallWithContext) :
+def RecCallCache.mk (decrTactics : Array (Option Syntax)) (rcc : RecCallWithContext) :
     BaseIO RecCallCache := do
+  let decrTactic? := decrTactics[rcc.caller]!
   let cache ← IO.mkRef <| Array.mkArray rcc.params.size (Array.mkArray rcc.args.size Option.none)
   return { decrTactic?, rcc, cache }
 
@@ -570,8 +543,8 @@ def mkTupleSyntax : Array Term → MetaM Term
 Given an array of `MutualMeasures`, creates a `TerminationWF` that specifies the lexicographic
 combination of these measures.
 -/
-def buildTermWF (declNames : Array Name) (varNamess : Array (Array Name))
-    (measures : Array MutualMeasure) : MetaM TerminationWF := do
+def buildTermWF (varNamess : Array (Array Name)) (measures : Array MutualMeasure) :
+    MetaM TerminationWF := do
   let mut termByElements := #[]
   for h : funIdx in [:varNamess.size] do
     let vars := (varNamess[funIdx]'h.2).map mkIdent
@@ -582,13 +555,7 @@ def buildTermWF (declNames : Array Name) (varNamess : Array (Array Name))
           `($sizeOfIdent $v)
       | .func funIdx' => if funIdx' == funIdx then `(1) else `(0)
       )
-    let declName := declNames[funIdx]!
-
-    termByElements := termByElements.push
-      { ref := .missing
-        declName, vars, body,
-        implicit := true
-      }
+    termByElements := termByElements.push { ref := .missing, vars, body }
   return termByElements
 
 
@@ -700,8 +667,8 @@ Main entry point of this module:
 Try to find a lexicographic ordering of the arguments for which the recursive definition
 terminates. See the module doc string for a high-level overview.
 -/
-def guessLex (preDefs : Array PreDefinition)  (unaryPreDef : PreDefinition)
-    (fixedPrefixSize : Nat) (decrTactic? : Option Syntax) :
+def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
+    (fixedPrefixSize : Nat) :
     MetaM TerminationWF := do
   let varNamess ← preDefs.mapM (naryVarNames fixedPrefixSize ·)
   let arities := varNamess.map (·.size)
@@ -716,24 +683,21 @@ def guessLex (preDefs : Array PreDefinition)  (unaryPreDef : PreDefinition)
 
   -- If there is only one plausible measure, use that
   if let #[solution] := measures then
-    return ← buildTermWF (preDefs.map (·.declName)) varNamess #[solution]
+    return ← buildTermWF varNamess #[solution]
 
   -- Collect all recursive calls and extract their context
   let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities
   let recCalls := filterSubsumed recCalls
-  let rcs ← recCalls.mapM (RecCallCache.mk decrTactic? ·)
+  let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasing_by?)) ·)
   let callMatrix := rcs.map (inspectCall ·)
 
   match ← liftMetaM <| solve measures callMatrix with
   | .some solution => do
-    let wf ← buildTermWF (preDefs.map (·.declName)) varNamess solution
-
-    let wfStx ← withoutModifyingState do
-      preDefs.forM (addAsAxiom ·)
-      wf.unexpand
+    let wf ← buildTermWF varNamess solution
 
     if showInferredTerminationBy.get (← getOptions) then
-      logInfo m!"Inferred termination argument:{wfStx}"
+      for preDef in preDefs, term in wf do
+        logInfoAt preDef.ref m!"Inferred termination argument: {← term.unexpand}"
 
     return wf
   | .none =>

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

@@ -80,7 +80,7 @@ private def isOnlyOneUnaryDef (preDefs : Array PreDefinition) (fixedPrefixSize :
   else
     return false
 
-def wfRecursion (preDefs : Array PreDefinition) (wf? : Option TerminationWF) (decrTactic? : Option Syntax) : TermElabM Unit := do
+def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
   let preDefs ← preDefs.mapM fun preDef => return { preDef with value := (← preprocess preDef.value) }
   let (unaryPreDef, fixedPrefixSize) ← withoutModifyingEnv do
     for preDef in preDefs do
@@ -91,11 +91,19 @@ def wfRecursion (preDefs : Array PreDefinition) (wf? : Option TerminationWF) (de
     let unaryPreDefs ← packDomain fixedPrefixSize preDefsDIte
     return (← packMutual fixedPrefixSize preDefs unaryPreDefs, fixedPrefixSize)
 
-  let wf ←
-    if let .some wf := wf? then
-      pure wf
+  let wf ← do
+    let (preDefsWith, preDefsWithout) := preDefs.partition (·.termination.termination_by?.isSome)
+    if preDefsWith.isEmpty then
+      -- No termination_by anywhere, so guess one
+      guessLex preDefs unaryPreDef fixedPrefixSize
+    else if preDefsWithout.isEmpty then
+      pure <| preDefsWith.map (·.termination.termination_by?.get!)
     else
-      guessLex preDefs unaryPreDef fixedPrefixSize decrTactic?
+      -- Some have, some do not, so report errors
+      preDefsWithout.forM fun preDef => do
+        logErrorAt preDef.ref (m!"Missing `termination_by`; this function is mutually " ++
+          m!"recursive with {preDefsWith[0]!.declName}, which has a `termination_by` clause.")
+      return
 
   let preDefNonRec ← forallBoundedTelescope unaryPreDef.type fixedPrefixSize fun prefixArgs type => do
     let type ← whnfForall type
@@ -104,7 +112,7 @@ def wfRecursion (preDefs : Array PreDefinition) (wf? : Option TerminationWF) (de
       trace[Elab.definition.wf] "wfRel: {wfRel}"
       let (value, envNew) ← withoutModifyingEnv' do
         addAsAxiom unaryPreDef
-        let value ← mkFix unaryPreDef prefixArgs wfRel decrTactic?
+        let value ← mkFix unaryPreDef prefixArgs wfRel (preDefs.map (·.termination.decreasing_by?))
         eraseRecAppSyntaxExpr value
       /- `mkFix` invokes `decreasing_tactic` which may add auxiliary theorems to the environment. -/
       let value ← unfoldDeclsFrom envNew value

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

@@ -36,6 +36,47 @@ private def getCodomainsLevel (preDefsOriginal : Array PreDefinition) (preDefTyp
           throwError "invalid mutual definition, result types must be in the same universe level, resulting type for `{preDefsOriginal[0]!.declName}` is{indentExpr type₀} : {← inferType type₀}\nand for `{preDefsOriginal[i]!.declName}` is{indentExpr typeᵢ} : {← inferType typeᵢ}"
   return r
 
+def unpackMutualArg {m} [Monad m] [MonadError m] (numFuncs : Nat) (e : Expr) :
+    m (Nat × Expr) := do
+  let mut funidx := 0
+  let mut e := e
+  while funidx + 1 < numFuncs do
+    if e.isAppOfArity ``PSum.inr 3 then
+      e := e.getArg! 2
+      funidx := funidx + 1
+    else if e.isAppOfArity ``PSum.inl 3 then
+      e := e.getArg! 2
+      break
+    else
+      throwError "Unexpected expression while unpacking mutual argument"
+  return (funidx, e)
+
+def unpackPackedArg {m} [Monad m] [MonadError m] (arity : Nat) (e : Expr) :
+    m (Array Expr) := do
+  let mut e := e
+  let mut args := #[]
+  while args.size + 1 < arity do
+    if e.isAppOfArity ``PSigma.mk 4 then
+      args := args.push (e.getArg! 2)
+      e := e.getArg! 3
+    else
+      throwError "Unexpected expression while unpacking n-ary argument"
+  args := args.push e
+  return args
+
+/-- Given the packed argument of a (possibly) mutual and (possibly) nary call,
+return the function index that is called and the arguments individually.
+
+We expect precisely the expressions produced by `packMutual`, with manifest
+`PSum.inr`, `PSum.inl` and `PSigma.mk` constructors, and thus take them apart
+rather than using projectinos. -/
+def unpackArg {m} [Monad m] [MonadError m] (arities : Array Nat) (e : Expr) :
+    m (Nat × Array Expr) := do
+  let (funidx, e) ← unpackMutualArg arities.size e
+  let args ← unpackPackedArg arities[funidx]! e
+  return (funidx, args)
+
+
 /--
   Create the codomain for the new function that "combines" different `preDef` types
   See: `packMutual`

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

@@ -14,11 +14,13 @@ namespace Lean.Elab.WF
 open Meta
 open Term
 
+/-
 private def getRefFromElems (elems : Array TerminationByElement) : Syntax := Id.run do
   for elem in elems do
     if !elem.implicit then
       return elem.ref
   return elems[0]!.ref
+-/
 
 private partial def unpackMutual (preDefs : Array PreDefinition) (mvarId : MVarId) (fvarId : FVarId) : TermElabM (Array (FVarId × MVarId)) := do
   let rec go (i : Nat) (mvarId : MVarId) (fvarId : FVarId) (result : Array (FVarId × MVarId)) : TermElabM (Array (FVarId × MVarId)) := do
@@ -29,7 +31,7 @@ private partial def unpackMutual (preDefs : Array PreDefinition) (mvarId : MVarI
       return result.push (fvarId, mvarId)
   go 0 mvarId fvarId #[]
 
-private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mvarId : MVarId) (fvarId : FVarId) (element : TerminationByElement) : TermElabM MVarId := do
+private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mvarId : MVarId) (fvarId : FVarId) (element : TerminationBy) : TermElabM MVarId := do
   let varNames ← lambdaTelescope preDef.value fun xs _ => do
     let mut varNames ← xs.mapM fun x => x.fvarId!.getUserName
     if element.vars.size > varNames.size then
@@ -60,7 +62,9 @@ def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPre
   let expectedType := mkApp (mkConst ``WellFoundedRelation [u]) α
   trace[Elab.definition.wf] "elabWFRel start: {(← mkFreshTypeMVar).mvarId!}"
   withDeclName unaryPreDefName do
-  withRef (getRefFromElems wf) do
+  -- TODO: Which ref to use here?
+  -- withRef (getRefFromElems wf) do
+  id do
     let mainMVarId := (← mkFreshExprSyntheticOpaqueMVar expectedType).mvarId!
     let [fMVarId, wfRelMVarId, _] ← mainMVarId.apply (← mkConstWithFreshMVarLevels ``invImage) | throwError "failed to apply 'invImage'"
     let (d, fMVarId) ← fMVarId.intro1

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

@@ -3,58 +3,13 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Lean.Parser.Command
+import Lean.Parser.Term
 
 set_option autoImplicit false
 
 namespace Lean.Elab.WF
 
-/-! # Support for `decreasing_by` -/
-
-structure DecreasingByTactic where
-  ref   : Syntax
-  value : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq
-  deriving Inhabited
-
-inductive DecreasingBy where
-  | none
-  | one (val : DecreasingByTactic)
-  | many (map : NameMap DecreasingByTactic)
-  deriving Inhabited
-
-open Parser.Command in
-/--
-This function takes a user-specified `decreasing_by` clause (as `Sytnax`).
-If it is a `decreasingByMany` (a set of clauses guarded by the function name) then
-* checks that all mentioned names exist in the current declaration
-* check that at most one function from each clique is mentioned
-and sort the entries by function name.
--/
-def expandDecreasingBy? (decreasingBy? : Option Syntax) (cliques : Array (Array Name)) : MacroM DecreasingBy := do
-  let some decreasingBy := decreasingBy? | return DecreasingBy.none
-  let ref := decreasingBy
-  match decreasingBy with
-  | `(decreasingBy|decreasing_by $hint1:tacticSeq) =>
-    return DecreasingBy.one { ref, value := hint1 }
-  | `(decreasingBy|decreasing_by $hints:decreasingByMany) => do
-    let m ← hints.raw[0].getArgs.foldlM (init := {}) fun m arg => do
-      let arg : TSyntax `decreasingByElement := ⟨arg⟩ -- cannot use syntax pattern match with lookahead
-      let `(decreasingByElement| $declId:ident => $tac:tacticSeq) := arg | Macro.throwUnsupported
-      let declName? := cliques.findSome? fun clique => clique.findSome? fun declName =>
-        if declId.getId.isSuffixOf declName then some declName else none
-      match declName? with
-      | none => Macro.throwErrorAt declId s!"function '{declId.getId}' not found in current declaration"
-      | some declName => return m.insert declName { ref := arg, value := tac }
-    for clique in cliques do
-      let mut found? := Option.none
-      for declName in clique do
-        if let some { ref, .. } := m.find? declName then
-          if let some found := found? then
-            Macro.throwErrorAt ref s!"invalid termination hint element, '{declName}' and '{found}' are in the same clique"
-          found? := some declName
-    return DecreasingBy.many m
-  | _ => Macro.throwUnsupported
-
+/-
 def DecreasingBy.markAsUsed (t : DecreasingBy) (clique : Array Name) : DecreasingBy :=
   match t with
   | DecreasingBy.none   => DecreasingBy.none
@@ -80,48 +35,61 @@ def DecreasingBy.ensureAllUsed (t : DecreasingBy) : MacroM Unit := do
   | DecreasingBy.one v   => Macro.throwErrorAt v.ref "unused termination hint element"
   | DecreasingBy.many m  => m.forM fun _ v => Macro.throwErrorAt v.ref "unused termination hint element"
   | _ => pure ()
+-/
 
 /-! # Support for `termination_by` notation -/
 
 /-- A single `termination_by` clause -/
-structure TerminationByElement where
+structure TerminationBy where
   ref       : Syntax
-  declName  : Name
   vars      : TSyntaxArray [`ident, ``Lean.Parser.Term.hole]
   body      : Term
-  implicit  : Bool
   deriving Inhabited
 
-/-- `termination_by` clauses, grouped by clique -/
-structure TerminationByClique where
-  elements : Array TerminationByElement
-  used     : Bool := false
+open Parser.Termination in
+def TerminationBy.unexpand (wf : TerminationBy) : MetaM Syntax := do
+  -- TODO: Why can I not use $wf.vars below?
+  let vars : TSyntaxArray `ident := wf.vars.map (⟨·.raw⟩)
+  `(terminationBy|termination_by $vars* => $wf.body)
 
-/--
-A `termination_by` hint, as specified by the user
--/
-structure TerminationBy where
-  cliques : Array TerminationByClique
+/-- A complete set of `termination_by` hints, as applicable to a single clique.  -/
+abbrev TerminationWF := Array TerminationBy
+
+
+/-- The termination annotations for a single function -/
+structure TerminationHints where
+  ref : Syntax
+  termination_by? : Option TerminationBy
+  decreasing_by?  : Option (TSyntax ``Lean.Parser.Tactic.tacticSeq)
   deriving Inhabited
 
-/--
-A `termination_by` hint, as applicable to a single clique
--/
-abbrev TerminationWF := Array TerminationByElement
+
+def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none⟩
+
+open Parser.Termination
+
+def elabTerminationHints (stx : TSyntax ``suffix) : TerminationHints :=
+  -- TODO: Better understand if this is needed
+  if let .missing := stx.raw then { TerminationHints.none with ref := stx }
+  -- and why this is needed
+  else if stx.raw.matchesNull 0 then { TerminationHints.none with ref := stx }
+  else
+    match stx with
+  | `(suffix| $[$t?:terminationBy]? $[$d?:decreasingBy]? ) =>
+    { ref := stx
+      termination_by? := t?.map fun t => match t with
+        | `(terminationBy|termination_by $vars* => $body) => {ref := t, vars, body}
+        | _ => unreachable!
+      decreasing_by? := d?.map fun
+        | `(decreasingBy|decreasing_by $ts) => ts
+        | _ => unreachable!  }
+  | _ => panic! s!"Unexpected Termination.suffix syntax: {stx} of kind {stx.raw.getKind}"
+
+/-
 
 open Parser.Command in
 /--
-Expands the syntax for a `termination_by` clause, checking that
-* each function is mentioned once
-* each function mentioned actually occurs in the current declaration
-* if anything is specified, then all functions have a clause
-* the else-case (`_`) occurs only once, and only when needed
-
-NB:
-```
-def terminationByElement   := leading_parser ppLine >> (ident <|> hole) >> many (ident <|> hole) >> " => " >> termParser >> optional ";"
-def terminationBy          := leading_parser ppLine >> "termination_by " >> many1chIndent terminationByElement
-```
+Expands the syntax for a `termination_by` clause
 -/
 def expandTerminationBy? (hint? : Option Syntax) (cliques : Array (Array Name)) :
     MacroM TerminationBy := do
@@ -170,13 +138,9 @@ def expandTerminationBy? (hint? : Option Syntax) (cliques : Array (Array Name))
   if !usedElse && elseElemStx?.isSome then
     withRef elseElemStx?.get! <| Macro.throwError s!"invalid `termination_by` syntax, unnecessary else-case"
   return ⟨result⟩
+-/
 
-open Parser.Command in
-def TerminationWF.unexpand (elements : TerminationWF) : MetaM Syntax := do
-  let elementStxs ← elements.mapM fun element => do
-    let fn : Ident := mkIdent (← unresolveNameGlobal element.declName)
-    `(terminationByElement|$fn $element.vars* => $element.body)
-  `(terminationBy|termination_by $elementStxs*)
+/-
 
 def TerminationBy.markAsUsed (t : TerminationBy) (cliqueNames : Array Name) : TerminationBy :=
   .mk <| t.cliques.map fun clique =>
@@ -209,5 +173,6 @@ def TerminationBy.ensureAllUsed (t : TerminationBy) : MacroM Unit := do
         unless reportedAllImplicit do
           reportedAllImplicit := true
           Macro.throwErrorAt clique.elements[0]!.ref "unused termination hint element"
+-/
 
 end Lean.Elab.WF

src/Lean/Elab/Term.lean

@@ -10,6 +10,7 @@ import Lean.Linter.Deprecated
 import Lean.Elab.Config
 import Lean.Elab.Level
 import Lean.Elab.DeclModifiers
+import Lean.Elab.PreDefinition.WF.TerminationHint
 
 namespace Lean.Elab
 
@@ -95,6 +96,7 @@ structure LetRecToLift where
   type           : Expr
   val            : Expr
   mvarId         : MVarId
+  termination    : WF.TerminationHints
   deriving Inhabited
 
 /--

src/Lean/Parser/Command.lean

@@ -28,27 +28,6 @@ match against a quotation in a command kind's elaborator). -/
 @[builtin_term_parser low] def quot := leading_parser
   "`(" >> withoutPosition (incQuotDepth (many1Unbox commandParser)) >> ")"
 
-/--
-A decreasing_by clause can either be a single tactic (for all functions), or
-a list of tactics labeled with the function they apply to.
--/
-def decreasingByElement := leading_parser
-  ppLine >> ppIndent (ident >> " => " >> Tactic.tacticSeq >> patternIgnore (optional ";"))
-def decreasingByMany := leading_parser
-  atomic (lookahead (ident >> " => ")) >> many1Indent decreasingByElement
-def decreasingBy1  := leading_parser Tactic.tacticSeq
-
-def decreasingBy := leading_parser
-  ppDedent ppLine >> "decreasing_by " >> (decreasingByMany <|> decreasingBy1)
-
-def terminationByElement   := leading_parser
-  ppLine >> (ident <|> Term.hole) >> many (ppSpace >> (ident <|> Term.hole)) >>
-  " => " >> termParser >> patternIgnore (optional ";")
-def terminationBy          := leading_parser
-  ppDedent ppLine >> "termination_by" >> many1Indent terminationByElement
-
-def terminationSuffix :=
-  optional terminationBy >> optional decreasingBy
 
 @[builtin_command_parser]
 def moduleDoc := leading_parser ppDedent <|
@@ -96,7 +75,7 @@ def declSig          := leading_parser
 def optDeclSig       := leading_parser
   many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.optType
 def declValSimple    := leading_parser
-  " :=" >> ppHardLineUnlessUngrouped >> termParser >> optional Term.whereDecls
+  " :=" >> ppHardLineUnlessUngrouped >> termParser >> Termination.suffix >> optional Term.whereDecls
 def declValEqns      := leading_parser
   Term.matchAltsWhereDecls
 def whereStructField := leading_parser
@@ -116,20 +95,20 @@ def declVal          :=
   withAntiquot (mkAntiquot "declVal" `Lean.Parser.Command.declVal (isPseudoKind := true)) <|
     declValSimple <|> declValEqns <|> whereStructInst
 def «abbrev»         := leading_parser
-  "abbrev " >> declId >> ppIndent optDeclSig >> declVal >> terminationSuffix
+  "abbrev " >> declId >> ppIndent optDeclSig >> declVal
 def optDefDeriving   :=
   optional (ppDedent ppLine >> atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ")
 def «def»            := leading_parser
-  "def " >> declId >> ppIndent optDeclSig >> declVal >> optDefDeriving >> terminationSuffix
+  "def " >> declId >> ppIndent optDeclSig >> declVal >> optDefDeriving
 def «theorem»        := leading_parser
-  "theorem " >> declId >> ppIndent declSig >> declVal >> terminationSuffix
+  "theorem " >> declId >> ppIndent declSig >> declVal
 def «opaque»         := leading_parser
   "opaque " >> declId >> ppIndent declSig >> optional declValSimple
 /- As `declSig` starts with a space, "instance" does not need a trailing space
   if we put `ppSpace` in the optional fragments. -/
 def «instance»       := leading_parser
   Term.attrKind >> "instance" >> optNamedPrio >>
-  optional (ppSpace >> declId) >> ppIndent declSig >> declVal >> terminationSuffix
+  optional (ppSpace >> declId) >> ppIndent declSig >> declVal
 def «axiom»          := leading_parser
   "axiom " >> declId >> ppIndent declSig
 /- As `declSig` starts with a space, "example" does not need a trailing space. -/
@@ -269,7 +248,7 @@ def openDecl         :=
 
 @[builtin_command_parser] def «mutual» := leading_parser
   "mutual" >> many1 (ppLine >> notSymbol "end" >> commandParser) >>
-  ppDedent (ppLine >> "end") >> terminationSuffix
+  ppDedent (ppLine >> "end")
 def initializeKeyword := leading_parser
   "initialize " <|> "builtin_initialize "
 @[builtin_command_parser] def «initialize» := leading_parser

src/Lean/Parser/Term.lean

@@ -96,6 +96,44 @@ end Tactic
 def darrow : Parser := " => "
 def semicolonOrLinebreak := ";" <|> checkLinebreakBefore >> pushNone
 
+namespace Termination
+
+/-
+Termination suffix parsers, typically thought of as part of a command, but due to
+letrec we need them here already.
+-/
+
+/--
+Specify a termination argument for well-founded termination:
+```
+termination_by a _ b => a - b
+```
+indicates that termination of the currently defined recursive function follows
+because the difference between the first and third argument decreases.
+
+If omitted, a termination argument will be inferred.
+-/
+def terminationBy := leading_parser
+  ppDedent ppLine >> "termination_by" >> many (ppSpace >> (ident <|> "_")) >>
+  " => " >> termParser
+
+/--
+Manually prove that the termination argument (as specified with `termination_by` or inferred)
+decreases at each recursive call.
+
+By default, the tactic `decreasing_tactic` is used.
+-/
+def decreasingBy := leading_parser
+  ppDedent ppLine >> "decreasing_by " >> Tactic.tacticSeq
+
+/--
+Termination hints are `termination_by` and `decreasing_by`, in that order.
+-/
+def suffix := leading_parser
+  optional terminationBy >> optional decreasingBy
+
+end Termination
+
 namespace Term
 
 /-! # Built-in parsers -/
@@ -532,8 +570,9 @@ def attributes       := leading_parser
   "@[" >> withoutPosition (sepBy1 attrInstance ", ") >> "] "
 /-- `letRecDecl` matches the body of a let-rec declaration: a doc comment, attributes, and then
 a let declaration without the `let` keyword, such as `/-- foo -/ @[simp] bar := 1`. -/
+-- NB: Uses checkColGt, this is relative to the `withPosition` in `letrec` and `whereDecls`.
 def letRecDecl       := leading_parser
-  optional Command.docComment >> optional «attributes» >> letDecl
+  optional Command.docComment >> optional «attributes» >> letDecl >> Termination.suffix
 /-- `letRecDecls` matches `letRecDecl,+`, a comma-separated list of let-rec declarations (see `letRecDecl`). -/
 def letRecDecls      := leading_parser
   sepBy1 letRecDecl ", "
@@ -548,7 +587,7 @@ def whereDecls := leading_parser
 
 @[run_builtin_parser_attribute_hooks]
 def matchAltsWhereDecls := leading_parser
-  matchAlts >> optional whereDecls
+  matchAlts >> Termination.suffix >> optional whereDecls
 
 @[builtin_term_parser] def noindex := leading_parser
   "no_index " >> termParser maxPrec

src/lake/Lake/DSL/DeclUtil.lean

@@ -86,15 +86,15 @@ def mkConfigDecl (name? : Option Name)
 | `(structDeclSig| $id:ident) =>
   `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty :=
     {name := $(quote id.getId)})
-| `(structDeclSig| $id:ident where $fs;* $[$wds?]?) => do
+| `(structDeclSig| $id:ident where $fs;* $[$wds?:whereDecls]?) => do
   let fields ← fs.getElems.mapM expandDeclField
   let defn ← `({ name := $(quote id.getId), $fields,* })
-  `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?]?)
+  `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?:whereDecls]?)
 | `(structDeclSig| $id:ident $[: $ty?]? :=%$defTk $defn $[$wds?]?) => do
   let notice ← withRef defTk `(#eval IO.eprintln s!" warning: {__dir__}: `:=` syntax for configurations has been deprecated")
   `($notice $[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?]?)
-| `(structDeclSig| $id:ident { $[$fs $[,]?]* } $[$wds?]?) => do
+| `(structDeclSig| $id:ident { $[$fs $[,]?]* } $[$wds?:whereDecls]?) => do
   let fields ← fs.mapM expandDeclField
   let defn ← `({ name := $(quote id.getId), $fields,* })
-  `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?]?)
+  `(command|$[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?:whereDecls]?)
 | stx => Macro.throwErrorAt stx "ill-formed configuration syntax"

src/lake/Lake/DSL/Package.lean

@@ -65,9 +65,9 @@ optional(docComment) optional(Term.attributes)
 "post_update " (ppSpace simpleBinder)? (declValSimple <|> declValDo) : command
 
 macro_rules
-| `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? do $seq $[$wds?]?) =>
-  `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := do $seq $[$wds?]?)
-| `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := $defn $[$wds?]?) => do
+| `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? do $seq $[$wds?:whereDecls]?) =>
+  `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := do $seq $[$wds?:whereDecls]?)
+| `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := $defn $[$wds?:whereDecls]?) => do
   let pkg ← expandOptSimpleBinder pkg?
   let pkgName := mkIdentFrom pkg `_package.name
   let attr ← withRef kw `(Term.attrInstance| «post_update»)

src/lake/Lake/DSL/Script.lean

@@ -37,10 +37,10 @@ scoped syntax (name := scriptDecl)
 
 @[macro scriptDecl]
 def expandScriptDecl : Macro
-| `($[$doc?]? $[$attrs?]? script $id:ident $[$args?]? do $seq $[$wds?]?) => do
-  `($[$doc?]? $[$attrs?]? script $id:ident $[$args?]? := do $seq $[$wds?]?)
-| `($[$doc?]? $[$attrs?]? script $id:ident $[$args?]? := $defn $[$wds?]?) => do
+| `($[$doc?]? $[$attrs?]? script $id:ident $[$args?]? do $seq $[$wds?:whereDecls]?) => do
+  `($[$doc?]? $[$attrs?]? script $id:ident $[$args?]? := do $seq $[$wds?:whereDecls]?)
+| `($[$doc?]? $[$attrs?]? script $id:ident $[$args?]? := $defn $[$wds?:whereDecls]?) => do
   let args ← expandOptSimpleBinder args?
   let attrs := #[← `(Term.attrInstance| «script»)] ++ expandAttrs attrs?
-  `($[$doc?]? @[$attrs,*] def $id : ScriptFn := fun $args => $defn $[$wds?]?)
+  `($[$doc?]? @[$attrs,*] def $id : ScriptFn := fun $args => $defn $[$wds?:whereDecls]?)
 | stx => Macro.throwErrorAt stx "ill-formed script declaration"

src/lake/Lake/DSL/Targets.lean

@@ -34,7 +34,7 @@ scoped macro (name := moduleFacetDecl)
 doc?:optional(docComment) attrs?:optional(Term.attributes)
 kw:"module_facet " sig:buildDeclSig : command => do
   match sig with
-  | `(buildDeclSig| $id:ident $[$mod?]? : $ty := $defn $[$wds?]?) =>
+  | `(buildDeclSig| $id:ident $[$mod?]? : $ty := $defn $[$foo]? $[$bar]? $[$wds?]?) =>
     let attr ← withRef kw `(Term.attrInstance| module_facet)
     let attrs := #[attr] ++ expandAttrs attrs?
     let name := Name.quoteFrom id id.getId
@@ -62,18 +62,21 @@ scoped macro (name := packageFacetDecl)
 doc?:optional(docComment) attrs?:optional(Term.attributes)
 kw:"package_facet " sig:buildDeclSig : command => do
   match sig with
-  | `(buildDeclSig| $id:ident $[$pkg?]? : $ty := $defn $[$wds?]?) =>
+  | `(buildDeclSig| $id:ident $[$pkg?]? : $ty := $defn $[$foo]? $[$bar]?  $[$wds?]?) =>
     let attr ← withRef kw `(Term.attrInstance| package_facet)
     let attrs := #[attr] ++ expandAttrs attrs?
     let name := Name.quoteFrom id id.getId
     let facetId := mkIdentFrom id <| id.getId.modifyBase (.str · "_pkgFacet")
     let pkg ← expandOptSimpleBinder pkg?
+    -- These parsers do not even exist, why is the quotation below expecting them?
+    let foo : Option (TSyntax `Lean.Parser.Command.terminationBy) := none
+    let bar : Option (TSyntax `Lean.Parser.Command.decreasingBy) := none
     `(package_data $id : BuildJob $ty
       $[$doc?]? @[$attrs,*] abbrev $facetId : PackageFacetDecl := {
         name := $name
         config := Lake.mkFacetJobConfig
           fun $pkg => ($defn : IndexBuildM (BuildJob $ty))
-      } $[$wds?]?)
+      } $[$wds?]? $[$foo]? $[$bar]? )
   | stx => Macro.throwErrorAt stx "ill-formed package facet declaration"
 
 /--
@@ -90,7 +93,7 @@ scoped macro (name := libraryFacetDecl)
 doc?:optional(docComment) attrs?:optional(Term.attributes)
 kw:"library_facet " sig:buildDeclSig : command => do
   match sig with
-  | `(buildDeclSig| $id:ident $[$lib?]? : $ty := $defn $[$wds?]?) =>
+  | `(buildDeclSig| $id:ident $[$lib?]? : $ty := $defn $[$wds?:whereDecls]?) =>
     let attr ← withRef kw `(Term.attrInstance| library_facet)
     let attrs := #[attr] ++ expandAttrs attrs?
     let name := Name.quoteFrom id id.getId
@@ -124,7 +127,7 @@ scoped macro (name := targetDecl)
 doc?:optional(docComment) attrs?:optional(Term.attributes)
 kw:"target " sig:buildDeclSig : command => do
   match sig with
-  | `(buildDeclSig| $id:ident $[$pkg?]? : $ty := $defn $[$wds?]?) =>
+  | `(buildDeclSig| $id:ident $[$pkg?]? : $ty := $defn $[$wds?:whereDecls]?) =>
     let attr ← withRef kw `(Term.attrInstance| target)
     let attrs := #[attr] ++ expandAttrs attrs?
     let name := Name.quoteFrom id id.getId
@@ -208,13 +211,13 @@ scoped macro (name := externLibDecl)
 doc?:optional(docComment) attrs?:optional(Term.attributes)
 "extern_lib " spec:externLibDeclSpec : command => do
   match spec with
-  | `(externLibDeclSpec| $id:ident $[$pkg?]? := $defn $[$wds?]?) =>
+  | `(externLibDeclSpec| $id:ident $[$pkg?]? := $defn $[$wds?:whereDecls]?) =>
     let attr ← `(Term.attrInstance| extern_lib)
     let attrs := #[attr] ++ expandAttrs attrs?
     let pkgName := mkIdentFrom id `_package.name
     let targetId := mkIdentFrom id <| id.getId.modifyBase (· ++ `static)
     let name := Name.quoteFrom id id.getId
-    `(target $targetId $[$pkg?]? : FilePath := $defn $[$wds?]?
+    `(target $targetId $[$pkg?]? : FilePath := $defn $[$wds?:whereDecls]?
       $[$doc?:docComment]? @[$attrs,*] def $id : ExternLibDecl := {
         pkg := $pkgName
         name := $name

stage0/src/stdlib_flags.h

@@ -8,7 +8,7 @@ options get_default_options() {
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
     // with custom precheck hooks were affected
     opts = opts.update({"quotPrecheck"}, true);

tests/lean/1026.lean

@@ -3,7 +3,7 @@ def foo (n : Nat) : Nat :=
     let x := n - 1
     have := match () with | _ => trivial
     foo x
-termination_by _ n => n
+termination_by n => n
 decreasing_by sorry
 
 theorem ex : foo 0 = 0 := by

tests/lean/1050.lean

@@ -7,15 +7,15 @@ namespace Foo
   mutual
     def bar    : {as bs: Type u} → Foo.{u} as bs → bs :=
       bar_aux
+    termination_by => 0
+    decreasing_by sorry
 
     def bar_aux: {as bs: Type u} → Foo.{u} as bs → bs
       | as, bs, foo _ x => x.bar
+    termination_by => 0
+    decreasing_by sorry
 
   end
-  termination_by
-    bar     => 0
-    bar_aux => 0
-  decreasing_by sorry
 end Foo
 
 
@@ -23,15 +23,15 @@ namespace Foo
   mutual
     def bar1    : {as bs: Type u} → Foo.{u} as bs → bs
       | as, bs, x => bar_aux1 x
+    termination_by => 0
+    decreasing_by sorry
 
     def bar_aux1 : {as bs: Type u} → Foo.{u} as bs → bs
       | as, bs, foo _ x => x.bar1
+    termination_by => 0
+    decreasing_by sorry
 
   end
-  termination_by
-    bar1     => 0
-    bar_aux1 => 0
-  decreasing_by sorry
 end Foo
 
 
@@ -39,12 +39,11 @@ namespace Foo
   mutual
     def bar2    : Foo as bs → bs
       | x => bar_aux2 x
+  termination_by x => (sizeOf x, 1)
 
     def bar_aux2 : Foo as bs → bs
       | foo _ x => x.bar2
+  termination_by x => (sizeOf x, 0)
 
   end
-  termination_by
-    bar2     x => (sizeOf x, 1)
-    bar_aux2 x => (sizeOf x, 0)
 end Foo

tests/lean/1050.lean.expected.out

@@ -1,4 +1,4 @@
-1050.lean:7:2-18:21: error: invalid mutual definition, result types must be in the same universe level, resulting type for `Foo.bar` is
+1050.lean:7:2-18:5: error: invalid mutual definition, result types must be in the same universe level, resulting type for `Foo.bar` is
   Foo as bs → bs : Type (u + 1)
 and for `Foo.bar_aux` is
   bs : Type u

tests/lean/1363.lean

@@ -10,13 +10,13 @@ def f : Nat → Nat
 def g : Nat → Nat
   | 0 => 0
   | n + 1 => g n
-termination_by g x => x
+termination_by x => x
 
 @[macro_inline] -- Error
 def h : Nat → Nat → Nat
   | 0, _ => 0
   | n + 1, m => h n m
-termination_by h x y => x
+termination_by x y => x
 
 @[macro_inline] -- Error
 partial def skipMany (p : Parsec α) (it : String.Iterator) : Parsec PUnit := do

tests/lean/StxQuot.lean.expected.out

@@ -8,8 +8,8 @@ StxQuot.lean:8:12-8:13: error: unexpected token ')'; expected identifier or term
 "(«term_+_» (num \"1\") \"+\" (num \"1\"))"
 StxQuot.lean:19:15-19:16: error: unexpected token ']'; expected term
 "(Term.fun \"fun\" (Term.basicFun [`a._@.UnhygienicMain._hyg.1] [] \"=>\" `a._@.UnhygienicMain._hyg.1))"
-"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (num \"1\") [])\n  []\n  []\n  []))"
-"[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"1\") [])\n   []\n   []\n   []))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"2\") [])\n   []\n   []\n   []))]"
+"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n  []))"
+"[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n   []))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"2\") (Termination.suffix [] []) [])\n   []))]"
 "`Nat.one._@.UnhygienicMain._hyg.1"
 "`Nat.one._@.UnhygienicMain._hyg.1"
 "(Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1 `Nat.one._@.UnhygienicMain._hyg.1])"
@@ -18,8 +18,8 @@ StxQuot.lean:19:15-19:16: error: unexpected token ']'; expected term
 "(Term.proj `Nat.one._@.UnhygienicMain._hyg.1 \".\" `b._@.UnhygienicMain._hyg.1)"
 "(«term_+_» (num \"2\") \"+\" (num \"1\"))"
 "(«term_+_» («term_+_» (num \"1\") \"+\" (num \"2\")) \"+\" (num \"1\"))"
-"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (num \"1\") [])\n  []\n  []\n  []))"
-"[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"2\") [])\n   []\n   []\n   []))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"1\") [])\n   []\n   []\n   []))]"
+"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n  []))"
+"[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"2\") (Termination.suffix [] []) [])\n   []))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n   []))]"
 "0"
 0
 1

tests/lean/decreasing_by.lean

@@ -1,41 +0,0 @@
-mutual
-  inductive Even : Nat → Prop
-    | base : Even 0
-    | step : Odd n → Even (n+1)
-  inductive Odd : Nat → Prop
-    | step : Even n → Odd (n+1)
-end
-decreasing_by assumption
-
-mutual
- def f (n : Nat) :=
-   if n == 0 then 0 else f (n / 2) + 1
- decreasing_by assumption
-end
-
-def g' (n : Nat) :=
-  match n with
-  | 0 => 1
-  | n+1 => g' n * 3
-decreasing_by
-  h => assumption
-
-namespace Test
-mutual
-  def f : Nat → α → α → α
-    | 0, a, b => a
-    | n+1, a, b => g n a b |>.1
-
-  def g : Nat → α → α → (α × α)
-    | 0, a, b => (a, b)
-    | n+1, a, b => (h n a b, a)
-
-  def h : Nat → α → α → α
-    | 0, a, b => b
-    | n+1, a, b => f n a b
-end
-decreasing_by
-  f => assumption
-  g => assumption
-
-end Test

tests/lean/decreasing_by.lean.expected.out

@@ -1,4 +0,0 @@
-decreasing_by.lean:8:0-8:24: error: invalid 'decreasing_by' in mutually inductive datatype declaration
-decreasing_by.lean:13:1-13:25: error: invalid 'decreasing_by' in 'mutual' block, it must be used after the 'end' keyword
-decreasing_by.lean:21:2-21:3: error: function 'h' not found in current declaration
-decreasing_by.lean:39:2-39:17: error: invalid termination hint element, 'Test.g' and 'Test.f' are in the same clique

tests/lean/guessLex.lean.expected.out

@@ -1,50 +1,39 @@
-Inferred termination argument:
-termination_by
-  ackermann n m => (sizeOf n, sizeOf m)
-Inferred termination argument:
-termination_by
-  ackermann2 n m => (sizeOf m, sizeOf n)
-Inferred termination argument:
-termination_by
-  ackermannList n m => (sizeOf n, sizeOf m)
-Inferred termination argument:
-termination_by
-  foo2 x1 x2 => (sizeOf x2, sizeOf x1)
-Inferred termination argument:
-termination_by
-  even x1 => sizeOf x1
-  odd x1 => sizeOf x1
-Inferred termination argument:
-termination_by
-  evenWithFixed x1 => sizeOf x1
-  oddWithFixed x1 => sizeOf x1
-Inferred termination argument:
-termination_by
-  ping.pong x1 => (sizeOf x1, 0)
-  ping n => (sizeOf n, 1)
-Inferred termination argument:
-termination_by
-  hasForbiddenArg n _h m => (sizeOf m, sizeOf n)
-Inferred termination argument:
-termination_by
-  blowup x1 x2 x3 x4 x5 x6 x7 x8 =>
+Inferred termination argument: 
+termination_by n m => (sizeOf n, sizeOf m)
+Inferred termination argument: 
+termination_by n m => (sizeOf m, sizeOf n)
+Inferred termination argument: 
+termination_by n m => (sizeOf n, sizeOf m)
+Inferred termination argument: 
+termination_by x1 x2 => (sizeOf x2, sizeOf x1)
+Inferred termination argument: 
+termination_by x1 => sizeOf x1
+Inferred termination argument: 
+termination_by x1 => sizeOf x1
+Inferred termination argument: 
+termination_by x1 => sizeOf x1
+Inferred termination argument: 
+termination_by x1 => sizeOf x1
+Inferred termination argument: 
+termination_by x1 => (sizeOf x1, 0)
+Inferred termination argument: 
+termination_by n => (sizeOf n, 1)
+Inferred termination argument: 
+termination_by n _h m => (sizeOf m, sizeOf n)
+Inferred termination argument: 
+termination_by x1 x2 x3 x4 x5 x6 x7 x8 =>
   (sizeOf x8, sizeOf x7, sizeOf x6, sizeOf x5, sizeOf x4, sizeOf x3, sizeOf x2, sizeOf x1)
-Inferred termination argument:
-termination_by
-  dependent x1 x2 => (sizeOf x1, sizeOf x2)
-Inferred termination argument:
-termination_by
-  eval a => (sizeOf a, 1)
-  eval_add a => (sizeOf a, 0)
-Inferred termination argument:
-termination_by
-  shadow1 x2 x2' => sizeOf x2'
-Inferred termination argument:
-termination_by
-  shadow2 some_n' x2 => sizeOf x2
-Inferred termination argument:
-termination_by
-  shadow3 sizeOf' x2 => sizeOf x2
-Inferred termination argument:
-termination_by
-  qualifiedSizeOf m x2 => SizeOf.sizeOf x2
+Inferred termination argument: 
+termination_by x1 x2 => (sizeOf x1, sizeOf x2)
+Inferred termination argument: 
+termination_by a => (sizeOf a, 1)
+Inferred termination argument: 
+termination_by a => (sizeOf a, 0)
+Inferred termination argument: 
+termination_by x2 x2' => sizeOf x2'
+Inferred termination argument: 
+termination_by some_n' x2 => sizeOf x2
+Inferred termination argument: 
+termination_by sizeOf' x2 => sizeOf x2
+Inferred termination argument: 
+termination_by m x2 => SizeOf.sizeOf x2

tests/lean/guessLexFailures.lean

@@ -99,7 +99,7 @@ namespace TrickyCode
 def FinPlus1 n := Fin (n + 1)
 def badCasesOn (n m : Nat) : Fin (n + 1) :=
    Nat.casesOn (motive := FinPlus1) n (⟨0,Nat.zero_lt_succ _⟩) (fun n => Fin.succ (badCasesOn n (.succ m)))
--- termination_by badCasesOn n m => n
+-- termination_by n m => n
 decreasing_by decreasing_tactic
 
 
@@ -109,7 +109,7 @@ decreasing_by decreasing_tactic
 -- https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Going.20under.20exactly.20one.20lambda/near/404278529
 def badCasesOn2 (n m : Nat) : Fin (n + 1) :=
    Nat.casesOn (motive := FinPlus1) n (⟨0,Nat.zero_lt_succ _⟩) (fun n => Fin.succ (badCasesOn2 n (.succ m)))
-termination_by badCasesOn2 n m => n
+termination_by n m => n
 decreasing_by decreasing_tactic
 
 -- The GuessLex code at does not like `casesOn` alternative with insufficient lambdas
@@ -119,7 +119,7 @@ def Fin_succ_comp (f : (n : Nat) → Fin (n + 1)) : (n : Nat) → Fin (n + 2) :=
 def badCasesOn3 (n m : Nat) : Fin (n + 1) :=
    Nat.casesOn (motive := fun n => Fin (n + 1)) n (⟨0,Nat.zero_lt_succ _⟩)
       (Fin_succ_comp (fun n => badCasesOn3 n (.succ m)))
--- termination_by badCasesOn3 n m => n
+-- termination_by n m => n
 decreasing_by decreasing_tactic
 
 
@@ -127,7 +127,7 @@ decreasing_by decreasing_tactic
 def badCasesOn4 (n m : Nat) : Fin (n + 1) :=
    Nat.casesOn (motive := fun n => Fin (n + 1)) n (⟨0,Nat.zero_lt_succ _⟩)
       (Fin_succ_comp (fun n => badCasesOn4 n (.succ m)))
-termination_by badCasesOn4 n m => n
+termination_by n m => n
 decreasing_by decreasing_tactic
 
 end TrickyCode

tests/lean/guessLexTricky.lean

@@ -39,15 +39,32 @@ macro_rules | `(tactic|search_lex $ts:tacticSeq) => `(tactic| (
 mutual
 def prod (x y z : Nat) : Nat :=
   if y % 2 = 0 then eprod x y z else oprod x y z
+decreasing_by
+  -- TODO: Why does it not work to wrap it all in `all_goals`?
+  all_goals simp_wf
+  · search_lex solve
+      | decreasing_trivial
+      | apply Nat.bitwise_rec_lemma; assumption
+  · search_lex solve
+      | decreasing_trivial
+      | apply Nat.bitwise_rec_lemma; assumption
+
 def oprod (x y z : Nat) := eprod x (y - 1) (z + x)
-def eprod (x y z : Nat) := if y = 0 then z else prod (2 * x) (y / 2) z
-end
--- termination_by
---   prod x y z => (y, 2)
---   oprod x y z => (y, 1)
---   eprod x y z => (y, 0)
 decreasing_by
   simp_wf
   search_lex solve
     | decreasing_trivial
     | apply Nat.bitwise_rec_lemma; assumption
+
+def eprod (x y z : Nat) := if y = 0 then z else prod (2 * x) (y / 2) z
+decreasing_by
+  simp_wf
+  search_lex solve
+    | decreasing_trivial
+    | apply Nat.bitwise_rec_lemma; assumption
+
+end
+-- termination_by
+--   prod x y z => (y, 2)
+--   oprod x y z => (y, 1)
+--   eprod x y z => (y, 0)

tests/lean/guessLexTricky.lean.expected.out

@@ -1,5 +1,6 @@
-Inferred termination argument:
-termination_by
-  prod x y z => (sizeOf y, 1, 0)
-  oprod x y z => (sizeOf y, 0, 1)
-  eprod x y z => (sizeOf y, 0, 0)
+Inferred termination argument: 
+termination_by x y z => (sizeOf y, 1, 0)
+Inferred termination argument: 
+termination_by x y z => (sizeOf y, 0, 1)
+Inferred termination argument: 
+termination_by x y z => (sizeOf y, 0, 0)

tests/lean/guessLexTricky2.lean.expected.out

@@ -1,4 +1,4 @@
-Inferred termination argument:
-termination_by
-  pedal x1 x2 x3 => (sizeOf x1, sizeOf x2, 0)
-  coast x1 x2 x3 => (sizeOf x1, sizeOf x2, 1)
+Inferred termination argument: 
+termination_by x1 x2 x3 => (sizeOf x1, sizeOf x2, 0)
+Inferred termination argument: 
+termination_by x1 x2 x3 => (sizeOf x1, sizeOf x2, 1)

tests/lean/heapSort.lean

@@ -168,9 +168,9 @@ def Array.toBinaryHeap (lt : α → α → Bool) (a : Array α) : BinaryHeap α
       have : a.popMax.size < a.size := by
         simp; exact Nat.sub_lt (BinaryHeap.size_pos_of_max e) Nat.zero_lt_one
       loop a.popMax (out.push x)
+    termination_by _ => a.size
+    decreasing_by assumption
   loop (a.toBinaryHeap gt) #[]
-termination_by _ => a.size
-decreasing_by assumption
 
 attribute [simp] Array.heapSort.loop
 #check Array.heapSort.loop._eq_1

tests/lean/interactive/hover.lean

@@ -188,7 +188,7 @@ example : Nat → Nat → Nat := by
       --^ textDocument/hover
 
 def g (n : Nat) : Nat := g 0
-termination_by g n => n
+termination_by n => n
 decreasing_by have n' := n; admit
                        --^ textDocument/hover
 

tests/lean/letRecMissingAnnotation.lean

@@ -4,5 +4,5 @@ def sum (as : Array Nat) : Nat :=
       go (i+2) (s + as.get ⟨i, h⟩) -- Error
     else
       s
+    termination_by i _ => as.size - i
   go 0 0
-termination_by go i _ => as.size - i

tests/lean/mutwf1.lean

@@ -4,24 +4,24 @@ mutual
     | n, true  => 2 * f n false
     | 0, false => 1
     | n, false => n + g n
+  termination_by n b => (n, if b then 2 else 1)
+  decreasing_by
+  all_goals simp_wf
+  · apply Prod.Lex.right; decide
+  · apply Prod.Lex.right; decide
 
   def g (n : Nat) : Nat :=
     if h : n ≠ 0 then
       f (n-1) true
     else
       n
-end
-termination_by
-  f n b => (n, if b then 2 else 1)
-  g n => (n, 0)
-decreasing_by
-  simp_wf
-  first
-  | apply Prod.Lex.left
-    apply Nat.pred_lt
-  | apply Prod.Lex.right
-    decide
+  termination_by n => (n, 0)
+  decreasing_by
+  all_goals simp_wf
+  apply Prod.Lex.left
+  apply Nat.pred_lt
   done -- should fail
+end
 end Ex1
 
 
@@ -31,14 +31,13 @@ mutual
     | n, true  => 2 * f n false
     | 0, false => 1
     | n, false => n + g (n+1) -- Error
+  termination_by n b => (n, if b then 2 else 1)
 
   def g (n : Nat) : Nat :=
     if h : n ≠ 0 then
       f (n-1) true
     else
       n
+  termination_by n => (n, 0)
 end
-termination_by
-  f n b => (n, if b then 2 else 1)
-  g n   => (n, 0)
 end Ex2

tests/lean/mutwf1.lean.expected.out

@@ -1,4 +1,4 @@
-mutwf1.lean:24:2-24:6: error: unsolved goals
+mutwf1.lean:23:2-23:6: error: unsolved goals
 case h.a
 n : Nat
 h : n ≠ 0

tests/lean/run/1171.lean

@@ -6,7 +6,7 @@ def Nat.hasDecEq: (a: Nat) → (b: Nat) → Decidable (Eq a b)
   match h:hasDecEq n m with -- it works without `h:`
   | isTrue heq => isTrue  (heq ▸ rfl)
   | isFalse hne => isFalse (Nat.noConfusion · (λ heq  => absurd heq hne))
-termination_by _ a b => (a, b)
+termination_by a b => (a, b)
 
 set_option pp.proofs true
 #print Nat.hasDecEq

tests/lean/run/1848.lean

@@ -1,11 +1,11 @@
 abbrev f : Nat → Nat
   | 0 => 0
   | n + 1 => f n
-termination_by _ n => n
+termination_by n => n
 
 mutual
 abbrev f1 : Nat → Nat
   | 0 => 0
   | n + 1 => f1 n
+termination_by n => n
 end
-termination_by _ n => n

tests/lean/run/2810.lean

@@ -19,7 +19,7 @@ def f3 (n : Nat) : Nat :=
   match n with
   | 0 => 0
   | n + 1 => (f3) n
-termination_by f3 n => n
+termination_by n => n
 
 -- Same with rewrite
 

tests/lean/run/860.lean

@@ -13,17 +13,19 @@ private theorem pack_loop_terminates : (n : Nat) → n / 2 < n.succ
     · apply Nat.zero_lt_succ
 
 def pack (n: Nat) : List Nat :=
-  let rec loop (n : Nat) (acc : Nat) (accs: List Nat) : List Nat :=
-    let next (n: Nat) := n / 2;
-    match n with
-    | Nat.zero => List.cons acc accs
-    | n+1 => match evenq n with
-      | true => loop (next n) 0 (List.cons acc accs)
-      | false => loop (next n) (acc+1) accs
+  let rec
+    loop (n : Nat) (acc : Nat) (accs: List Nat) : List Nat :=
+      let next (n: Nat) := n / 2;
+      match n with
+      | Nat.zero => List.cons acc accs
+      | n+1 => match evenq n with
+        | true => loop (next n) 0 (List.cons acc accs)
+        | false => loop (next n) (acc+1) accs
+    termination_by n _ _ => n
+    decreasing_by all_goals
+      simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel]
+      apply pack_loop_terminates
+
   loop n 0 []
-termination_by _ n _ _ => n
-decreasing_by
-  simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel]
-  apply pack_loop_terminates
 
 #eval pack 27

tests/lean/run/879.lean

@@ -5,13 +5,9 @@ termination_by _ => b
 
 def foo2 (b c : Nat) := if h : b = 0 then a + c else foo2 (b - 1) c
 termination_by
-  foo2 x y z => y
-
-def foo3 (b c : Nat) := if h : b = 0 then a + c else foo3 (b - 1) c
-termination_by
-  _ x y z => y
+  x y z => y
 
 def foo4 (b c : Nat) := if h : b = 0 then a + c else foo4 (b - 1) c
 termination_by
   -- We can rename from right to left
-  foo4 y _ => y
+  y _ => y

tests/lean/run/955.lean

@@ -3,11 +3,15 @@ mutual
   def isEven : Nat → Bool
     | 0 => true
     | n+1 => isOdd n
+  termination_by n =>
+    match n with
+    | _ => n
+
   def isOdd : Nat → Bool
     | 0 => false
     | n+1 => isEven n
+  termination_by n =>
+    match n with
+    | _ => n
 end
-termination_by _ n =>
-  match n with
-  | _ => n
 end Ex2

tests/lean/run/ack.lean

@@ -2,4 +2,4 @@ def ack : Nat → Nat → Nat
   | 0,   y   => y+1
   | x+1, 0   => ack x 1
   | x+1, y+1 => ack x (ack (x+1) y)
-termination_by _ a b => (a, b)
+termination_by a b => (a, b)

tests/lean/run/addDecorationsWithoutPartial.lean

@@ -77,4 +77,4 @@ def addDecorations (e : Expr) : Expr :=
       let rest := Expr.forallE name newType newBody data
       some <| mkApp2 (mkConst `SlimCheck.NamedBinder) (mkStrLit n) rest
     | _ => none
-decreasing_by exact Nat.le_trans (by simp_arith) h
+decreasing_by all_goals exact Nat.le_trans (by simp_arith) h

tests/lean/run/binrec.lean

@@ -44,8 +44,8 @@ def Nat.binrec
     bit_div_even h₂ ▸ ind false (n / 2) (fun _ => binrec motive base ind (n / 2))
   else
     bit_div_odd h₂ ▸ ind true  (n / 2) (fun _ => binrec motive base ind (n / 2))
-termination_by _ n => n
-decreasing_by exact Nat.div2_lt h₁
+termination_by n => n
+decreasing_by all_goals exact Nat.div2_lt h₁
 
 theorem Nat.binind
     (motive : Nat → Prop)

tests/lean/run/constProp.lean

@@ -397,7 +397,7 @@ def State.length_erase_lt (σ : State) (x : Var) : (σ.erase x).length < σ.leng
     match σ₂.find? x with
     | some w => if v = w then (x, v) :: join σ₁' σ₂ else join σ₁' σ₂
     | none => join σ₁' σ₂
-termination_by _ σ₁ _ => σ₁.length
+termination_by σ₁ _ => σ₁.length
 
 local notation "⊥" => []
 
@@ -468,7 +468,7 @@ theorem State.join_le_left (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₁ :=
       next => apply cons_le_cons; apply le_trans ih (erase_le _)
       next => apply le_trans ih (erase_le_cons (le_refl _))
     next h => apply le_trans ih (erase_le_cons (le_refl _))
-termination_by _ σ₁ _ => σ₁.length
+termination_by σ₁ _ => σ₁.length
 
 theorem State.join_le_left_of (h : σ₁ ≼ σ₂) (σ₃ : State) : σ₁.join σ₃ ≼ σ₂ :=
   le_trans (join_le_left σ₁ σ₃) h
@@ -485,7 +485,7 @@ theorem State.join_le_right (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₂ :
       split <;> simp [*]
       next => apply cons_le_of_eq ih h
     next h => assumption
-termination_by _ σ₁ _ => σ₁.length
+termination_by σ₁ _ => σ₁.length
 
 theorem State.join_le_right_of (h : σ₁ ≼ σ₂) (σ₃ : State) : σ₃.join σ₁ ≼ σ₂ :=
   le_trans (join_le_right σ₃ σ₁) h

tests/lean/run/decreasingTacticUpdatedEnvIssue.lean

@@ -21,4 +21,4 @@ def f (x : Nat) : Nat :=
     1
   else
     f (g x (x > 0)) + 2
-termination_by f x => x
+termination_by x => x

tests/lean/run/defaultEliminator.lean

@@ -9,8 +9,8 @@
     | x+1, 0   => succ_zero x (go x 0)
     | 0,   y+1 => zero_succ y (go 0 y)
     | x+1, y+1 => succ_succ x y (go x y)
+    termination_by x y => (x, y)
   go x y
-termination_by go x y => (x, y)
 
 def f (x y : Nat) :=
   match x, y with
@@ -18,7 +18,7 @@ def f (x y : Nat) :=
   | x+1, 0   => f x 0
   | 0,   y+1 => f 0 y
   | x+1, y+1 => f x y
-termination_by f x y => (x, y)
+termination_by x y => (x, y)
 
 example (x y : Nat) : f x y > 0 := by
   induction x, y with

tests/lean/run/eqnsAtSimp.lean

@@ -2,13 +2,17 @@ mutual
   def isEven : Nat → Bool
     | 0 => true
     | n+1 => isOdd n
+  decreasing_by
+    simp [measure, invImage, InvImage, Nat.lt_wfRel]
+    apply Nat.lt_succ_self
+
   def isOdd : Nat → Bool
     | 0 => false
     | n+1 => isEven n
+  decreasing_by
+    simp [measure, invImage, InvImage, Nat.lt_wfRel]
+    apply Nat.lt_succ_self
 end
-decreasing_by
-  simp [measure, invImage, InvImage, Nat.lt_wfRel]
-  apply Nat.lt_succ_self
 
 theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
   induction x with

tests/lean/run/eqnsAtSimp2.lean

@@ -2,11 +2,13 @@ mutual
   @[simp] def isEven : Nat → Bool
     | 0 => true
     | n+1 => isOdd n
+  decreasing_by apply Nat.lt_succ_self
+
   @[simp] def isOdd : Nat → Bool
     | 0 => false
     | n+1 => isEven n
+  decreasing_by apply Nat.lt_succ_self
 end
-decreasing_by apply Nat.lt_succ_self
 
 theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
   induction x with

tests/lean/run/issue2628.lean

@@ -8,12 +8,13 @@ mutual
 def foo : Nat → Nat
   | .zero => 0
   | .succ n => (id bar) n
+decreasing_by sorry
+
 def bar : Nat → Nat
   | .zero => 0
   | .succ n => foo n
-end
-termination_by foo n => n; bar n => n
 decreasing_by sorry
+end
 
 end Ex1
 
@@ -28,12 +29,15 @@ def foo : Nat → Nat → Nat
   | .zero, _m => 0
   | .succ n, .zero => (id' (bar n)) .zero
   | .succ n, m => (id' bar) n m
+termination_by n m => (n,m)
+decreasing_by all_goals sorry
+
 def bar : Nat → Nat → Nat
   | .zero, _m => 0
   | .succ n, m => foo n m
+termination_by n m => (n,m)
+decreasing_by all_goals sorry
 end
-termination_by foo n m => (n,m); bar n m => (n,m)
-decreasing_by sorry
 
 end Ex2
 
@@ -44,12 +48,12 @@ mutual
 def foo : Nat → Nat → Nat
   | .zero => fun _ => 0
   | .succ n => fun m => (id bar) n m
+decreasing_by all_goals sorry
 def bar : Nat → Nat → Nat
   | .zero => fun _ => 0
   | .succ n => fun m => foo n m
+decreasing_by all_goals sorry
 end
-termination_by foo n => n; bar n => n
-decreasing_by sorry
 
 end Ex3
 
@@ -62,12 +66,14 @@ def foo : Nat → Nat → Nat → Nat
   | .zero, _m => fun _ => 0
   | .succ n, .zero => fun k => (id' (bar n)) .zero k
   | .succ n, m => fun k => (id' bar) n m k
+termination_by n m => (n,m)
+decreasing_by all_goals sorry
 def bar : Nat → Nat → Nat → Nat
   | .zero, _m => fun _ => 0
   | .succ n, m => fun k => foo n m k
+termination_by n m => (n,m)
+decreasing_by all_goals sorry
 end
-termination_by foo n m => (n,m); bar n m => (n,m)
-decreasing_by sorry
 
 end Ex4
 
@@ -80,12 +86,12 @@ mutual
 def foo : FunType
   | .zero => 0
   | .succ n => (id bar) n
+decreasing_by all_goals sorry
 def bar : Nat → Nat
   | .zero => 0
   | .succ n => foo n
+decreasing_by all_goals sorry
 end
-termination_by foo n => n; bar n => n
-decreasing_by sorry
 
 end Ex5
 
@@ -98,11 +104,13 @@ def foo : Nat → Nat → Nat → Nat
   | .zero, _m => fun _ => 0
   | .succ n, .zero => fun k => (id' (bar n)) .zero k
   | .succ n, m => fun k => (id' bar) n m k
+termination_by n m => (n,m)
+decreasing_by all_goals sorry
 def bar : Nat → Fun3Type
   | .zero, _m => fun _ => 0
   | .succ n, m => fun k => foo n m k
+termination_by n m => (n,m)
+decreasing_by all_goals sorry
 end
-termination_by foo n m => (n,m); bar n m => (n,m)
-decreasing_by sorry
 
 end Ex6

tests/lean/run/issue2883.lean

@@ -15,11 +15,10 @@ end
 mutual
   def foo : B → Prop
   | .fromA a => bar a 0
+  termination_by x => sizeOf x
 
   def bar : A → Nat → Prop
   | .baseA   => (fun _ => True)
   | .fromB b => (fun (c : Nat) => ∃ (t : Nat), foo b)
+  termination_by x => sizeOf x
 end
-termination_by
-  foo x => sizeOf x
-  bar x => sizeOf x

tests/lean/run/issue2925.lean

@@ -5,11 +5,13 @@ mutual
 def foo : FunType
   | .zero => 0
   | .succ n => bar n
+termination_by n => n
 def bar : Nat → Nat
   | .zero => 0
   | .succ n => baz n 0
+termination_by n => n
 def baz : Fun2Type
   | .zero, m => 0
   | .succ n, m => foo n
+termination_by n _ => n
 end
-termination_by foo n => n; bar n => n; baz n _ => n

tests/lean/run/letrecWFIssue.lean

@@ -16,7 +16,10 @@ def Tree.size : Tree α → Nat
       apply Nat.lt_succ_self
     sizeList l
   | Tree.leaf _ => 1
-where sizeList : TreeList α → Nat
+-- use automatically synthesized size function, which is not quite the number of leaves
+termination_by t => sizeOf t
+where
+  sizeList : TreeList α → Nat
   | TreeList.nil => 0
   | TreeList.cons t l =>
     have : sizeOf t < 1 + sizeOf t + sizeOf l := by
@@ -28,7 +31,4 @@ where sizeList : TreeList α → Nat
       apply Nat.lt_succ_of_le
       apply Nat.le_add_left
     t.size + sizeList l
--- use automatically synthesized size function, which is not quite the number of leaves
-termination_by
-  size t => sizeOf t
-  sizeList l => sizeOf l
+  termination_by l => sizeOf l

tests/lean/run/mut_ind_wf.lean

@@ -19,6 +19,8 @@ def Tree.size : Tree α → Nat
       apply Nat.lt_succ_self
     sizeList l
   | Tree.leaf _ => 1
+-- use automatically synthesized size function, which is not quite the number of leaves
+termination_by t => sizeOf t
 
 def Tree.sizeList : TreeList α → Nat
   | TreeList.nil => 0
@@ -32,11 +34,8 @@ def Tree.sizeList : TreeList α → Nat
       apply Nat.lt_succ_of_le
       apply Nat.le_add_left
     t.size + sizeList l
+termination_by l => sizeOf l
 end
--- use automatically synthesized size function, which is not quite the number of leaves
-termination_by
-  size t => sizeOf t
-  sizeList l => sizeOf l
 
 end Mutual
 
@@ -54,6 +53,7 @@ def Tree.size : Tree α → Nat
       apply Nat.lt_succ_self
     sizeList l
   | Tree.leaf _ => 1
+termination_by t => sizeOf t
 
 def Tree.sizeList : List (Tree α) → Nat
   | [] => 0
@@ -67,9 +67,7 @@ def Tree.sizeList : List (Tree α) → Nat
       apply Nat.lt_succ_of_le
       apply Nat.le_add_left
     t.size + sizeList l
+termination_by l => sizeOf l
 end
-termination_by
-  size t => sizeOf t
-  sizeList l => sizeOf l
 
 end Nested

tests/lean/run/mutwf1.lean

@@ -3,19 +3,18 @@ mutual
   def f : Nat → α → α → α
     | 0, a, b => a
     | n, a, b => g a n b |>.1
+  termination_by n _ _ => (n, 2)
 
   def g : α → Nat → α → (α × α)
     | a, 0, b => (a, b)
     | a, n, b => (h a b n, a)
+  termination_by _ n _ => (n, 1)
 
   def h : α → α → Nat → α
     | a, b, 0 => b
     | a, b, n+1 => f n a b
+  termination_by _ _ n => (n, 0)
 end
-termination_by
-  f n _ _ => (n, 2)
-  g _ n _ => (n, 1)
-  h _ _ n => (n, 0)
 
 #print f
 #print g

tests/lean/run/mutwf2.lean

@@ -3,11 +3,12 @@ mutual
   def isEven : Nat → Bool
     | 0 => true
     | n+1 => isOdd n
+  termination_by n => n
   def isOdd : Nat → Bool
     | 0 => false
     | n+1 => isEven n
+  termination_by n => n
 end
-termination_by _ n => n
 
 #print isEven
 #print isOdd

tests/lean/run/mutwf3.lean

@@ -3,26 +3,30 @@ mutual
   def f : Nat → α → α → α
     | 0, a, b => a
     | n, a, b => g a n b |>.1
+  termination_by n _ _ => (n, 2)
+  decreasing_by
+    simp_wf
+    apply Prod.Lex.right
+    decide
 
   def g : α → Nat → α → (α × α)
     | a, 0, b => (a, b)
     | a, n, b => (h a b n, a)
+  termination_by _ n _ => (n, 1)
+  decreasing_by
+    simp_wf
+    apply Prod.Lex.right
+    decide
 
   def h : α → α → Nat → α
     | _a, b, 0 => b
     | a, b, n+1 => f n a b
-end
-termination_by
-  f n _ _ => (n, 2)
-  g _ n _ => (n, 1)
-  h _ _ n => (n, 0)
-decreasing_by
-  simp_wf
-  first
-  | apply Prod.Lex.left
+  termination_by _ _ n => (n, 0)
+  decreasing_by
+    simp_wf
+    apply Prod.Lex.left
     apply Nat.lt_succ_self
-  | apply Prod.Lex.right
-    decide
+end
 
 #eval f 5 'a' 'b'
 #print f
@@ -36,19 +40,18 @@ mutual
   def f : Nat → α → α → α
     | 0, a, b => a
     | n, a, b => g a n b |>.1
+  termination_by n _ _ => (n, 2)
 
   def g : α → Nat → α → (α × α)
     | a, 0, b => (a, b)
     | a, n, b => (h a b n, a)
+  termination_by _ n _ => (n, 1)
 
   def h : α → α → Nat → α
     | a, b, 0 => b
     | a, b, n+1 => f n a b
+  termination_by _ _ n => (n, 0)
 end
-termination_by
-  f n _ _ => (n, 2)
-  g _ n _ => (n, 1)
-  h _ _ n => (n, 0)
 
 #print f._unary._mutual
 

tests/lean/run/mutwf4.lean

@@ -1,19 +1,17 @@
-set_option trace.Elab.definition.wf true in
 mutual
   def f : Nat → Bool → Nat
     | n, true  => 2 * f n false
     | 0, false => 1
     | n, false => n + g n
+  termination_by n b => (n, if b then 2 else 1)
 
   def g (n : Nat) : Nat :=
     if h : n ≠ 0 then
       f (n-1) true
     else
       n
+  termination_by n => (n, 0)
 end
-termination_by
-  f n b => (n, if b then 2 else 1)
-  g n   => (n, 0)
 
 #print f
 #print g

tests/lean/run/nestedIssueMatch.lean

@@ -5,7 +5,7 @@ def g (t : Nat) : Nat := match t with
       | 0 => 0
       | m + 1 => g n
   | 0 => 0
-decreasing_by sorry
+decreasing_by all_goals sorry
 
 attribute [simp] g
 

tests/lean/run/nestedWF.lean

@@ -4,6 +4,9 @@ mutual
 def h (c : Nat) (x : Nat) := match g c x c c with
   | 0 => 1
   | r => r + 2
+termination_by c x => 0
+decreasing_by all_goals sorry
+
 def g (c : Nat) (t : Nat) (a b : Nat) : Nat := match t with
   | (n+1) => match g c n a b with
     | 0 => 0
@@ -11,15 +14,15 @@ def g (c : Nat) (t : Nat) (a b : Nat) : Nat := match t with
       | 0 => 0
       | m + 1 => g c m a b
   | 0 => f c 0
+termination_by c t a b => 0
+decreasing_by all_goals sorry
+
 def f (c : Nat) (x : Nat) := match h c x with
   | 0 => 1
   | r => f c r
+termination_by c x => 0
+decreasing_by all_goals sorry
 end
-termination_by
-  g x a b => 0
-  f c x => 0
-  h c x => 0
-decreasing_by sorry
 
 attribute [simp] g
 attribute [simp] h
@@ -43,7 +46,7 @@ def g (t : Nat) : Nat := match t with
       | 0 => 0
       | m + 1 => g n
   | 0 => 0
-decreasing_by sorry
+decreasing_by all_goals sorry
 
 theorem ex1 : g 0 = 0 := by
   rw [g]

tests/lean/run/overAndPartialAppsAtWF.lean

@@ -17,7 +17,6 @@ termination_by _ => a.size - i
     fun z => f (x - 1) (y + 1) z + 1
   else
     (· + y)
-termination_by
-  f x y => x
+termination_by x y => x
 
 #check f._eq_1

tests/lean/run/psumAtWF.lean

@@ -4,13 +4,12 @@ def fn (f : α → α) (a : α) (n : Nat) : α :=
   match n with
   | 0 => a
   | n+1 => gn f (f (f a)) (f a) n
+termination_by n => n
 
 def gn (f : α → α) (a b : α) (n : Nat) : α :=
   match n with
   | 0 => b
   | n+1 => fn f (f b) n
+termination_by n => n
 
 end
-termination_by
-  fn n => n
-  gn n => n

tests/lean/run/renameFixedPrefix.lean

@@ -3,4 +3,4 @@ def f (as : Array Nat) (hsz : as.size > 0) (i : Nat) : Nat :=
     as.get ⟨i, h⟩ + f as hsz (i + 1)
   else
     0
-termination_by f a h i => a.size - i
+termination_by a h i => a.size - i

tests/lean/run/robinson.lean

@@ -41,11 +41,10 @@ def robinson (u v : Term) : { f : Option Subst // P f u v } := match u, v with
   | .Var i, .Var j =>
     if i = j then ⟨ some id, sorry ⟩
     else ⟨ some λ n => if n = i then j else n, sorry ⟩
-termination_by _ u v => (u, v)
+termination_by  u v => (u, v)
 decreasing_by
-  first
-    | apply decr_left _ _ _ _
-    | apply decr_right _ _ _ _ _
+  · apply decr_left _ _ _ _
+  · apply decr_right _ _ _ _ _
 
 attribute [simp] robinson
 

tests/lean/run/splitIssue.lean

@@ -14,8 +14,9 @@ def len : List α → Nat
   | l =>
     match splitList l with
     | ListSplit.split fst snd => len fst + len snd
-termination_by _ l => l.length
+termination_by l => l.length
 decreasing_by
+  all_goals
   simp [measure, id, invImage, InvImage, Nat.lt_wfRel, WellFoundedRelation.rel, sizeOf] <;>
   first
     | apply Nat.lt_add_right

tests/lean/run/splitList.lean

@@ -32,7 +32,7 @@ def len : List α → Nat
       have dec₁ : fst.length < as.length + 2 := by subst l; simp_arith [eq_of_heq h₂] at this |- ; simp [this]
       have dec₂ : snd.length < as.length + 2 := by subst l; simp_arith [eq_of_heq h₂] at this |- ; simp [this]
       len fst + len snd
-termination_by _ xs => xs.length
+termination_by xs => xs.length
 
 theorem len_nil : len ([] : List α) = 0 := by
  simp [len]
@@ -78,10 +78,11 @@ def len : List α → Nat
       len fst + len snd
 termination_by _ xs => xs.length
 decreasing_by
-  simp_wf
-  have := splitList_length (fst ++ snd) (by simp_arith [h₁]) h₁
-  subst h₂
-  simp_arith [eq_of_heq h₃] at this |- ; simp [this]
+  all_goals
+    simp_wf
+    have := splitList_length (fst ++ snd) (by simp_arith [h₁]) h₁
+    subst h₂
+    simp_arith [eq_of_heq h₃] at this |- ; simp [this]
 
 theorem len_nil : len ([] : List α) = 0 := by
   simp [len]

tests/lean/run/wfEqns1.lean

@@ -9,13 +9,17 @@ mutual
   def isEven : Nat → Bool
     | 0 => true
     | n+1 => isOdd n
+  decreasing_by
+    simp [measure, invImage, InvImage, Nat.lt_wfRel]
+    apply Nat.lt_succ_self
+
   def isOdd : Nat → Bool
     | 0 => false
     | n+1 => isEven n
+  decreasing_by
+    simp [measure, invImage, InvImage, Nat.lt_wfRel]
+    apply Nat.lt_succ_self
 end
-decreasing_by
-  simp [measure, invImage, InvImage, Nat.lt_wfRel]
-  apply Nat.lt_succ_self
 
 #print isEven
 

tests/lean/run/wfEqns2.lean

@@ -11,21 +11,24 @@ def g (i j : Nat) : Nat :=
   match j with
   | Nat.zero => 1
   | Nat.succ j => h i j
+termination_by i j => (i + j, 0)
+decreasing_by
+  simp_wf
+  · apply Prod.Lex.left
+    apply Nat.lt_succ_self
+
 def h (i j : Nat) : Nat :=
   match j with
   | 0 => g i 0
   | Nat.succ j => g i j
-end
-termination_by
-  g i j => (i + j, 0)
-  h i j => (i + j, 1)
+termination_by i j => (i + j, 1)
 decreasing_by
-  simp_wf
-  first
-  | apply Prod.Lex.left
-    apply Nat.lt_succ_self
-  | apply Prod.Lex.right
+  all_goals simp_wf
+  · apply Prod.Lex.right
     decide
+  · apply Prod.Lex.left
+    apply Nat.lt_succ_self
+end
 
 #eval tst ``g
 #check g._eq_1

tests/lean/run/wfEqns4.lean

@@ -9,26 +9,30 @@ mutual
   def f : Nat → α → α → α
     | 0, a, b => a
     | n, a, b => g a n b |>.1
+  termination_by n _ _ => (n, 2)
+  decreasing_by
+    simp_wf
+    apply Prod.Lex.right
+    decide
 
   def g : α → Nat → α → (α × α)
     | a, 0, b => (a, b)
     | a, n, b => (h a b n, a)
+  termination_by _ n _ => (n, 1)
+  decreasing_by
+    simp_wf
+    apply Prod.Lex.right
+    decide
 
   def h : α → α → Nat → α
     | a, b, 0 => b
     | a, b, n+1 => f n a b
-end
-termination_by
-  f n _ _ => (n, 2)
-  g _ n _ => (n, 1)
-  h _ _ n => (n, 0)
-decreasing_by
-  simp_wf
-  first
-  | apply Prod.Lex.left
+  termination_by _ _ n => (n, 0)
+  decreasing_by
+    simp_wf
+    apply Prod.Lex.left
     apply Nat.lt_succ_self
-  | apply Prod.Lex.right
-    decide
+end
 
 #eval f 5 'a' 'b'
 

tests/lean/run/wfLean3Issue.lean

@@ -3,4 +3,4 @@ def foo : Nat → Nat → Nat
   | s+1, 0   => foo s 0 + 1
   | 0,   b+1 => foo 0 b + 1
   | s+1, b+1 => foo (s+1) b + foo s (b+1)
-termination_by foo b s => (b, s)
+termination_by b s => (b, s)

tests/lean/run/wfOverapplicationIssue.lean

@@ -8,5 +8,5 @@ theorem Array.sizeOf_lt_of_mem' [DecidableEq α] [SizeOf α] {as : Array α} (h
       next he => subst a; apply sizeOf_get_lt
       next => have ih := aux (j+1) h; assumption
     · contradiction
+    termination_by j => as.size - j
   apply aux 0 h
-termination_by aux j => as.size - j

tests/lean/run/wfSum.lean

@@ -6,4 +6,4 @@ where
       go (i+1) (s + as.get ⟨i, h⟩)
     else
       s
-termination_by _ i s => as.size - i
+  termination_by i s => as.size - i

tests/lean/termination_by.lean

@@ -1,105 +1,34 @@
-mutual
-  inductive Even : Nat → Prop
-    | base : Even 0
-    | step : Odd n → Even (n+1)
-  inductive Odd : Nat → Prop
-    | step : Even n → Odd (n+1)
-end
-termination_by _ n => n -- Error
-
-mutual
- def f (n : Nat) :=
-   if n == 0 then 0 else f (n / 2) + 1
- termination_by _ => n -- Error
-end
-
-mutual
- def f (n : Nat) :=
-   if n == 0 then 0 else f (n / 2) + 1
-end
-termination_by n => n -- Error
-
-
-def g' (n : Nat) :=
-  match n with
-  | 0 => 1
-  | n+1 => g' n * 3
-termination_by
-  h' n => n -- Error
-
-def g' (n : Nat) :=
-  match n with
-  | 0 => 1
-  | n+1 => g' n * 3
-termination_by
-  g' n => n
-  _ n => n -- Error
+/-!
+This module tests various mis-uses of termination_by,
+in particular that all or none of a recursive group have it.
+-/
 
 mutual
   def isEven : Nat → Bool
     | 0 => true
     | n+1 => isOdd n
-  def isOdd : Nat → Bool
+  termination_by x => x
+
+  def isOdd : Nat → Bool -- Error
     | 0 => false
     | n+1 => isEven n
 end
-termination_by
-   isEven x => x -- Error
-
-mutual
-  def isEven : Nat → Bool
-    | 0 => true
-    | n+1 => isOdd n
-  def isOdd : Nat → Bool
-    | 0 => false
-    | n+1 => isEven n
-end
-termination_by
-   isEven x => x
-   isOd x => x -- Error
-
-mutual
-  def isEven : Nat → Bool
-    | 0 => true
-    | n+1 => isOdd n
-  def isOdd : Nat → Bool
-    | 0 => false
-    | n+1 => isEven n
-end
-termination_by
-   isEven x => x
-   isEven y => y -- Error
-
-mutual
-  def isEven : Nat → Bool
-    | 0 => true
-    | n+1 => isOdd n
-  def isOdd : Nat → Bool
-    | 0 => false
-    | n+1 => isEven n
-end
-termination_by
-   isEven x => x
-   _ x => x
-   _ x => x + 1 -- Error
-
 
 namespace Test
 mutual
   def f : Nat → α → α → α
     | 0, a, b => a
     | n+1, a, b => g n a b |>.1
+  termination_by n => n
 
   def g : Nat → α → α → (α × α)
     | 0, a, b => (a, b)
     | n+1, a, b => (h n a b, a)
+  termination_by n => n
 
-  def h : Nat → α → α → α
+  def h : Nat → α → α → α -- Error
     | 0, a, b => b
     | n+1, a, b => f n a b
 end
-termination_by
-  f n => n -- Error
-  g n => n
 
 end Test

tests/lean/termination_by.lean.expected.out

@@ -1,10 +1,2 @@
-termination_by.lean:8:0-8:23: error: invalid 'termination_by' in mutually inductive datatype declaration
-termination_by.lean:13:1-13:22: error: invalid 'termination_by' in 'mutual' block, it must be used after the 'end' keyword
-termination_by.lean:20:15-20:21: error: function 'n' not found in current declaration
-termination_by.lean:28:2-28:11: error: function 'h'' not found in current declaration
-termination_by.lean:36:2-36:10: error: invalid `termination_by` syntax, unnecessary else-case
-termination_by.lean:47:3-47:16: error: invalid `termination_by` syntax, missing case for function 'isOdd'
-termination_by.lean:59:3-59:14: error: function 'isOd' not found in current declaration
-termination_by.lean:71:3-71:16: error: invalid `termination_by` syntax, `isEven` case has already been provided
-termination_by.lean:84:3-84:15: error: invalid `termination_by` syntax, the else-case (i.e., `_ ... => ...`) has already been specified
-termination_by.lean:102:2-102:10: error: invalid `termination_by` syntax, missing case for function 'Test.h'
+termination_by.lean:12:6-12:11: error: Missing `termination_by`; this function is mutually recursive with isEven, which has a `termination_by` clause.
+termination_by.lean:29:6-29:7: error: Missing `termination_by`; this function is mutually recursive with Test.f, which has a `termination_by` clause.

tests/lean/termination_by_where.lean

@@ -0,0 +1,16 @@
+/-!
+This module systematically tests the relative placement of `decreasing_by` and `where`.
+-/
+
+-- For concise recursive definition that need well-founded recursion
+-- and `decreasing_by` tactics that would fail if run on the wrong function
+opaque dec1 : Nat → Nat
+axiom dec1_lt (n : Nat) : dec1 n < n
+opaque dec2 : Nat → Nat
+axiom dec2_lt (n : Nat) : dec2 n < n
+
+def foo (n : Nat) := foo (dec1 n) + bar n
+decreasing_by apply dec1_lt
+where
+bar (m : Nat) : Nat := bar (dec2 m)
+decreasing_by apply dec2_lt

tests/lean/treeMap.lean

@@ -6,4 +6,4 @@ open TreeNode in def treeToList (t : TreeNode) : List String :=
  match t with
  | mkLeaf name => [name]
  | mkNode name children => name :: List.join (children.map treeToList)
-termination_by _ t => t
+termination_by t => t

tests/lean/unfold1.lean

@@ -2,11 +2,12 @@ mutual
   def isEven : Nat → Bool
     | 0 => true
     | n+1 => isOdd n
+  decreasing_by apply Nat.lt_succ_self
   def isOdd : Nat → Bool
     | 0 => false
     | n+1 => isEven n
+  decreasing_by apply Nat.lt_succ_self
 end
-decreasing_by apply Nat.lt_succ_self
 
 theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
   induction x with

tests/lean/wf2.lean

@@ -3,4 +3,4 @@ def g (x : Nat) (y : Nat) : Nat :=
     2 * g (x-1) y -- Error here
   else
     0
-termination_by g x y => x
+termination_by x y => x