refactor: TerminationArgument → TerminationMeasure

this PR aligns the terminology of the code with the one use in the
reference manual, as developed with and refined by @david-christiansen.

doc/declarations.md

@@ -590,9 +590,9 @@ This table should be read as follows:
  * No other proofs were attempted, either because the parameter has a type without a non-trivial ``WellFounded`` instance (parameter 3), or because it is already clear that no decreasing measure can be found.
 
 
-Lean will print the termination argument it found if ``set_option showInferredTerminationBy true`` is set.
+Lean will print the termination measure it found if ``set_option showInferredTerminationBy true`` is set.
 
-If Lean does not find the termination argument, or if you want to be explicit, you can append a `termination_by` clause to the function definition, after the function's body, but before the `where` clause if present. It is of the form
+If Lean does not find the termination measure, or if you want to be explicit, you can append a `termination_by` clause to the function definition, after the function's body, but before the `where` clause if present. It is of the form
 ```
 termination_by e
 ```
@@ -672,7 +672,7 @@ def num_consts_lst : List Term → Nat
 end
 ```
 
-In a set of mutually recursive function, either all or no functions must have an explicit termination argument (``termination_by``). A change of the default termination tactic (``decreasing_by``) only affects the proofs about the recursive calls of that function, not the other functions in the group.
+In a set of mutually recursive function, either all or no functions must have an explicit termination measure (``termination_by``). A change of the default termination tactic (``decreasing_by``) only affects the proofs about the recursive calls of that function, not the other functions in the group.
 
 ```
 mutual

src/Lean/Elab/PreDefinition/Main.lean

@@ -219,14 +219,14 @@ def checkTerminationByHints (preDefs : Array PreDefinition) : CoreM Unit := do
         m!"`nontermination_partialFixpointursive`, so this one cannot be either.")
 
 /--
-Elaborates the `TerminationHint` in the clique to `TerminationArguments`
+Elaborates the `TerminationHint` in the clique to `TerminationMeasures`
 -/
-def elabTerminationByHints (preDefs : Array PreDefinition) : TermElabM (Array (Option TerminationArgument)) := do
+def elabTerminationByHints (preDefs : Array PreDefinition) : TermElabM (Array (Option TerminationMeasure)) := do
   preDefs.mapM fun preDef => do
     let arity ← lambdaTelescope preDef.value fun xs _ => pure xs.size
     let hints := preDef.termination
     hints.terminationBy?.mapM
-      (TerminationArgument.elab preDef.declName preDef.type arity hints.extraParams ·)
+      (TerminationMeasure.elab preDef.declName preDef.type arity hints.extraParams ·)
 
 def shouldUseStructural (preDefs : Array PreDefinition) : Bool :=
   preDefs.any fun preDef =>
@@ -279,18 +279,18 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
           try
             checkCodomainsLevel preDefs
             checkTerminationByHints preDefs
-            let termArg?s ← elabTerminationByHints preDefs
+            let termMeasures?s ← elabTerminationByHints preDefs
             if shouldUseStructural preDefs then
-              structuralRecursion preDefs termArg?s
+              structuralRecursion preDefs termMeasures?s
             else if shouldUsepartialFixpoint preDefs then
               partialFixpoint preDefs
             else if shouldUseWF preDefs then
-              wfRecursion preDefs termArg?s
+              wfRecursion preDefs termMeasures?s
             else
               withRef (preDefs[0]!.ref) <| mapError
                 (orelseMergeErrors
-                  (structuralRecursion preDefs termArg?s)
-                  (wfRecursion preDefs termArg?s))
+                  (structuralRecursion preDefs termMeasures?s)
+                  (wfRecursion preDefs termMeasures?s))
                 (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}")

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

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Joachim Breitner
 -/
 prelude
-import Lean.Elab.PreDefinition.TerminationArgument
+import Lean.Elab.PreDefinition.TerminationMeasure
 import Lean.Elab.PreDefinition.Structural.Basic
 import Lean.Elab.PreDefinition.Structural.RecArgInfo
 
@@ -56,7 +56,7 @@ private def hasBadParamDep? (ys : Array Expr) (indParams : Array Expr) : MetaM (
 
 /--
 Assemble the `RecArgInfo` for the `i`th parameter in the parameter list `xs`. This performs
-various sanity checks on the argument (is it even an inductive type etc).
+various sanity checks on the parameter (is it even of inductive type etc).
 -/
 def getRecArgInfo (fnName : Name) (numFixed : Nat) (xs : Array Expr) (i : Nat) : MetaM RecArgInfo := do
   if h : i < xs.size then
@@ -112,17 +112,17 @@ considered.
 
 The `xs` are the fixed parameters, `value` the body with the fixed prefix instantiated.
 
-Takes the optional user annotations into account (`termArg?`). If this is given and the argument
+Takes the optional user annotation into account (`termMeasure?`). If this is given and the measure
 is unsuitable, throw an error.
 -/
 def getRecArgInfos (fnName : Name) (xs : Array Expr) (value : Expr)
-    (termArg? : Option TerminationArgument) : MetaM (Array RecArgInfo × MessageData) := do
+    (termMeasure? : Option TerminationMeasure) : MetaM (Array RecArgInfo × MessageData) := do
   lambdaTelescope value fun ys _ => do
-    if let .some termArg := termArg? then
-      -- User explicitly asked to use a certain argument, so throw errors eagerly
-      let recArgInfo ← withRef termArg.ref do
-        mapError (f := (m!"cannot use specified parameter for structural recursion:{indentD ·}")) do
-          getRecArgInfo fnName xs.size (xs ++ ys) (← termArg.structuralArg)
+    if let .some termMeasure := termMeasure? then
+      -- User explicitly asked to use a certain measure, so throw errors eagerly
+      let recArgInfo ← withRef termMeasure.ref do
+        mapError (f := (m!"cannot use specified measure for structural recursion:{indentD ·}")) do
+          getRecArgInfo fnName xs.size (xs ++ ys) (← termMeasure.structuralArg)
       return (#[recArgInfo], m!"")
     else
       let mut recArgInfos := #[]
@@ -233,12 +233,12 @@ def allCombinations (xss : Array (Array α)) : Option (Array (Array α)) :=
 
 
 def tryAllArgs (fnNames : Array Name) (xs : Array Expr) (values : Array Expr)
-   (termArg?s : Array (Option TerminationArgument)) (k : Array RecArgInfo → M α) : M α := do
+   (termMeasure?s : Array (Option TerminationMeasure)) (k : Array RecArgInfo → M α) : M α := do
   let mut report := m!""
   -- Gather information on all possible recursive arguments
   let mut recArgInfoss := #[]
-  for fnName in fnNames, value in values, termArg? in termArg?s do
-    let (recArgInfos, thisReport) ← getRecArgInfos fnName xs value termArg?
+  for fnName in fnNames, value in values, termMeasure? in termMeasure?s do
+    let (recArgInfos, thisReport) ← getRecArgInfos fnName xs value termMeasure?
     report := report ++ thisReport
     recArgInfoss := recArgInfoss.push recArgInfos
   -- Put non-indices first

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

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Joachim Breitner
 -/
 prelude
-import Lean.Elab.PreDefinition.TerminationArgument
+import Lean.Elab.PreDefinition.TerminationMeasure
 import Lean.Elab.PreDefinition.Structural.Basic
 import Lean.Elab.PreDefinition.Structural.FindRecArg
 import Lean.Elab.PreDefinition.Structural.Preprocess
@@ -127,7 +127,7 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (xs : Array Expr
   let valuesNew ← valuesNew.mapM (mkLambdaFVars xs ·)
   return (Array.zip preDefs valuesNew).map fun ⟨preDef, valueNew⟩ => { preDef with value := valueNew }
 
-private def inferRecArgPos (preDefs : Array PreDefinition) (termArg?s : Array (Option TerminationArgument)) :
+private def inferRecArgPos (preDefs : Array PreDefinition) (termMeasure?s : Array (Option TerminationMeasure)) :
     M (Array Nat × (Array PreDefinition) × Nat) := do
   withoutModifyingEnv do
     preDefs.forM (addAsAxiom ·)
@@ -142,7 +142,7 @@ private def inferRecArgPos (preDefs : Array PreDefinition) (termArg?s : Array (O
       assert! xs.size = maxNumFixed
       let values ← preDefs.mapM (instantiateLambda ·.value xs)
 
-      tryAllArgs fnNames xs values termArg?s fun recArgInfos => do
+      tryAllArgs fnNames xs values termMeasure?s fun recArgInfos => do
         let recArgPoss := recArgInfos.map (·.recArgPos)
         trace[Elab.definition.structural] "Trying argument set {recArgPoss}"
         let numFixed := recArgInfos.foldl (·.min ·.numFixed) maxNumFixed
@@ -156,20 +156,20 @@ private def inferRecArgPos (preDefs : Array PreDefinition) (termArg?s : Array (O
           let preDefs' ← elimMutualRecursion preDefs xs recArgInfos
           return (recArgPoss, preDefs', numFixed)
 
-def reportTermArg (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit := do
+def reporttermMeasure (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit := do
   if let some ref := preDef.termination.terminationBy?? then
     let fn ← lambdaTelescope preDef.value fun xs _ => mkLambdaFVars xs xs[recArgPos]!
-    let termArg : TerminationArgument:= {ref := .missing, structural := true, fn}
+    let termMeasure : TerminationMeasure:= {ref := .missing, structural := true, fn}
     let arity ← lambdaTelescope preDef.value fun xs _ => pure xs.size
-    let stx ← termArg.delab arity (extraParams := preDef.termination.extraParams)
+    let stx ← termMeasure.delab arity (extraParams := preDef.termination.extraParams)
     Tactic.TryThis.addSuggestion ref stx
 
 
-def structuralRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option TerminationArgument)) : TermElabM Unit := do
+def structuralRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option TerminationMeasure)) : TermElabM Unit := do
   let names := preDefs.map (·.declName)
-  let ((recArgPoss, preDefsNonRec, numFixed), state) ← run <| inferRecArgPos preDefs termArg?s
+  let ((recArgPoss, preDefsNonRec, numFixed), state) ← run <| inferRecArgPos preDefs termMeasure?s
   for recArgPos in recArgPoss, preDef in preDefs do
-    reportTermArg preDef recArgPos
+    reporttermMeasure preDef recArgPos
   state.addMatchers.forM liftM
   preDefsNonRec.forM fun preDefNonRec => do
     let preDefNonRec ← eraseRecAppSyntax preDefNonRec

src/Lean/Elab/PreDefinition/TerminationHint.lean

@@ -54,7 +54,7 @@ structure TerminationHints where
   Here we record the number of parameters past the `:`. It is set by
   `TerminationHints.rememberExtraParams` and used as follows:
 
-  * When we guess the termination argument in `GuessLex` and want to print it in surface-syntax
+  * When we guess the termination measure in `GuessLex` and want to print it in surface-syntax
     compatible form.
   * If there are fewer variables in the `termination_by` annotation than there are extra
     parameters, we know which parameters they should apply to (`TerminationBy.checkVars`).

src/Lean/Elab/PreDefinition/TerminationArgument.lean → src/Lean/Elab/PreDefinition/TerminationMeasure.lean

@@ -14,8 +14,8 @@ import Lean.PrettyPrinter.Delaborator.Basic
 
 /-!
 This module contains
-* the data type `TerminationArgument`, the elaborated form of a `TerminationBy` clause,
-* the `TerminationArguments` type for a clique, and
+* the data type `TerminationMeasure`, the elaborated form of a `TerminationBy` clause,
+* the `TerminationMeasures` type for a clique, and
 * elaboration and deelaboration functions.
 -/
 
@@ -29,28 +29,28 @@ open Lean Meta Elab Term
 Elaborated form for a `termination_by` clause.
 
 The `fn` has the same (value) arity as the recursive functions (stored in
-`arity`), and maps its arguments (including fixed prefix, in unpacked form) to
-the termination argument.
+`arity`), and maps its measures (including fixed prefix, in unpacked form) to
+the termination measure.
 
-If `structural := Bool`, then the `fn` is a lambda picking out exactly one argument.
+If `structural := Bool`, then the `fn` is a lambda picking out exactly one measure.
 -/
-structure TerminationArgument where
+structure TerminationMeasure where
   ref : Syntax
   structural : Bool
   fn : Expr
 deriving Inhabited
 
-/-- A complete set of `TerminationArgument`s, as applicable to a single clique.  -/
-abbrev TerminationArguments := Array TerminationArgument
+/-- A complete set of `TerminationMeasure`s, as applicable to a single clique.  -/
+abbrev TerminationMeasures := Array TerminationMeasure
 
 /--
-Elaborates a `TerminationBy` to an `TerminationArgument`.
+Elaborates a `TerminationBy` to an `TerminationMeasure`.
 
 * `type` is the full type of the original recursive function, including fixed prefix.
 * `hint : TerminationBy` is the syntactic `TerminationBy`.
 -/
-def TerminationArgument.elab (funName : Name) (type : Expr) (arity extraParams : Nat)
-    (hint : TerminationBy) : TermElabM TerminationArgument := withDeclName funName do
+def TerminationMeasure.elab (funName : Name) (type : Expr) (arity extraParams : Nat)
+    (hint : TerminationBy) : TermElabM TerminationMeasure := withDeclName funName do
   assert! extraParams ≤ arity
 
   if h : hint.vars.size > extraParams then
@@ -73,7 +73,7 @@ def TerminationArgument.elab (funName : Name) (type : Expr) (arity extraParams :
         -- Structural recursion: The body has to be a single parameter, whose index we return
         if hint.structural then unless (ys ++ xs).contains body do
           let params := MessageData.andList ((ys ++ xs).toList.map (m!"'{·}'"))
-          throwErrorAt hint.ref m!"The termination argument of a structurally recursive " ++
+          throwErrorAt hint.ref m!"The termination measure of a structurally recursive " ++
             m!"function must be one of the parameters {params}, but{indentExpr body}\nisn't " ++
             m!"one of these."
 
@@ -87,24 +87,24 @@ def TerminationArgument.elab (funName : Name) (type : Expr) (arity extraParams :
     | 1 => "one parameter"
     | n => m!"{n} parameters"
 
-def TerminationArgument.structuralArg (termArg : TerminationArgument) : MetaM Nat := do
-  assert! termArg.structural
-  lambdaTelescope termArg.fn fun ys e => do
+def TerminationMeasure.structuralArg (measure : TerminationMeasure) : MetaM Nat := do
+  assert! measure.structural
+  lambdaTelescope measure.fn fun ys e => do
     let .some idx := ys.indexOf? e
-      | panic! "TerminationArgument.structuralArg: body not one of the parameters"
+      | panic! "TerminationMeasure.structuralArg: body not one of the parameters"
     return idx
 
 
 open PrettyPrinter Delaborator SubExpr Parser.Termination Parser.Term in
 /--
-Delaborates a `TerminationArgument` back to a `TerminationHint`, e.g. for `termination_by?`.
+Delaborates a `TerminationMeasure` back to a `TerminationHint`, e.g. for `termination_by?`.
 
 This needs extra information:
 * `arity` is the value arity of the recursive function
-* `extraParams` indicates how many of the functions arguments are bound “after the colon”.
+* `extraParams` indicates how many of the function's parameters are bound “after the colon”.
 -/
-def TerminationArgument.delab (arity : Nat) (extraParams : Nat) (termArg : TerminationArgument) : MetaM (TSyntax ``terminationBy) := do
-  lambdaBoundedTelescope termArg.fn (arity - extraParams) fun _ys e => do
+def TerminationMeasure.delab (arity : Nat) (extraParams : Nat) (measure : TerminationMeasure) : MetaM (TSyntax ``terminationBy) := do
+  lambdaBoundedTelescope measure.fn (arity - extraParams) fun _ys e => do
     pure (← delabCore e (delab := go extraParams #[])).1
   where
     go : Nat → TSyntaxArray `ident → DelabM (TSyntax ``terminationBy)
@@ -119,7 +119,7 @@ def TerminationArgument.delab (arity : Nat) (extraParams : Nat) (termArg : Termi
       -- drop trailing underscores
       let mut vars := vars
       while ! vars.isEmpty && vars.back!.raw.isOfKind ``hole do vars := vars.pop
-      if termArg.structural then
+      if measure.structural then
         if vars.isEmpty then
           `(terminationBy|termination_by structural $stxBody)
         else