feat: GuessLex: print inferred termination argument (#3012)

With

    set_option showInferredTerminationBy true

this prints a message like

    Inferred termination argument:
    termination_by
      ackermann n m => (sizeOf n, sizeOf m)

it tries hard to use names that

 * match the names that the user used, if present
 * have no daggers (so that it can be copied)
 * do not shadow each other
 * do not shadow anything from the environment (just to be nice)

it does so by appending sufficient `'` to the name.

Some of the emitted `sizeOf` calls are unnecessary, but they are needed
sometimes with dependent parameters. A follow-up PR will not emit them
for non-dependent arguments, so that in most cases the output is pretty.

Somewhen down the road we also want a code action, maybe triggered by
`termination_by?`. This should come after #2921, as that simplifies that
feature (no need to merge termination arguments from different cliques
for example.)

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

@@ -66,23 +66,39 @@ open Lean Meta Elab
 
 namespace Lean.Elab.WF.GuessLex
 
+register_builtin_option showInferredTerminationBy : Bool := {
+  defValue := false
+  descr    := "In recursive definitions, show the inferred `termination_by` measure."
+}
+
 /--
 Given a predefinition, find good variable names for its parameters.
 Use user-given parameter names if present; use x1...xn otherwise.
+
 The length of the returned array is also used to determine the arity
 of the function, so it should match what `packDomain` does.
+
+The names ought to accessible (no macro scopes) and still fresh wrt to the current environment,
+so that with `showInferredTerminationBy` we can print them to the user reliably.
+We do that by appending `'` as needed.
 -/
+partial
 def naryVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Name):= do
   lambdaTelescope preDef.value fun xs _ => do
     let xs := xs.extract fixedPrefixSize xs.size
-    let mut ns := #[]
+    let mut ns : Array Name := #[]
     for h : i in [:xs.size] do
       let n ← (xs[i]'h.2).fvarId!.getUserName
-      if n.hasMacroScopes then
-        ns := ns.push (← mkFreshUserName (.mkSimple s!"x{i+1}"))
-      else
-        ns := ns.push n
+      let n := if n.hasMacroScopes then .mkSimple s!"x{i+1}" else n
+      ns := ns.push (← freshen ns n)
     return ns
+  where
+    freshen  (ns : Array Name) (n : Name): MetaM Name := do
+      if !(ns.elem n) && (← resolveGlobalName n).isEmpty then
+        return n
+      else
+        freshen ns (n.appendAfter "'")
+
 
 /-- Internal monad used by `withRecApps` -/
 abbrev M (recFnName : Name) (α β : Type) : Type :=
@@ -537,15 +553,14 @@ def buildTermWF (declNames : Array Name) (varNamess : Array (Array Name))
   for h : funIdx in [:varNamess.size] do
     let vars := (varNamess[funIdx]'h.2).map mkIdent
     let body ← mkTupleSyntax (← measures.mapM fun
-      | .args varIdxs =>
+      | .args varIdxs => do
           let v := vars.get! (varIdxs[funIdx]!)
-          let sizeOfIdent := mkIdent ``sizeOf
+          let sizeOfIdent := mkIdent (← unresolveNameGlobal ``sizeOf)
           `($sizeOfIdent $v)
       | .func funIdx' => if funIdx' == funIdx then `(1) else `(0)
       )
     let declName := declNames[funIdx]!
 
-    trace[Elab.definition.wf] "Using termination {declName}: {vars} => {body}"
     termByElements := termByElements.push
       { ref := .missing
         declName, vars, body,
@@ -688,6 +703,14 @@ def guessLex (preDefs : Array PreDefinition)  (unaryPreDef : PreDefinition)
   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
+
+    if showInferredTerminationBy.get (← getOptions) then
+      logInfo m!"Inferred termination argument:{wfStx}"
+
     return wf
   | .none =>
     let explanation ← explainFailure (preDefs.map (·.declName)) varNamess rcs

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

@@ -186,6 +186,17 @@ def expandTerminationBy (hint? : Option Syntax) (cliques : Array (Array Name)) :
   else
       return TerminationBy.core TerminationHint.none
 
+open Parser.Command in
+def TerminationWF.unexpand : TerminationWF → MetaM Syntax
+  | .ext elements => do
+    let elementStxs ← elements.mapM fun element => do
+      let fn : Ident := mkIdent (← unresolveNameGlobal element.declName)
+      let body : Term := ⟨element.body⟩
+      let vars : Array Ident := element.vars.map TSyntax.mk
+      `(terminationByElement|$fn $vars* => $body)
+    `(terminationBy|termination_by $elementStxs*)
+  | .core _ => unreachable! -- we don't synthetize termination_by' syntax
+
 def TerminationBy.markAsUsed (t : TerminationBy) (cliqueNames : Array Name) : TerminationBy :=
   match t with
   | core hint   => core (hint.markAsUsed cliqueNames)

tests/lean/run/guessLex.lean → tests/lean/guessLex.lean

@@ -8,6 +8,8 @@ When writing tests for GuesLex, keep in mind that it doesn't do anything
 when there is only one plausible measure (one function, only one varying argument).
 -/
 
+set_option showInferredTerminationBy true
+
 def ackermann (n m : Nat) := match n, m with
   | 0, m => m + 1
   | .succ n, 0 => ackermann n 1
@@ -95,7 +97,6 @@ def dependent : (n : Nat) → (m : Fin n) → Nat
  | .succ (.succ n), ⟨.succ m, h⟩ =>
   dependent (.succ (.succ n)) ⟨m, Nat.lt_of_le_of_lt (Nat.le_succ _) h⟩
 
-
 -- An example based on a real world problem, condensed by Leo
 inductive Expr where
   | add (a b : Expr)
@@ -111,3 +112,33 @@ def eval_add (a : Expr × Expr) : Nat :=
   match a with
   | (x, y) => eval x + eval y
 end
+
+namespace VarNames
+
+/-! Test that varnames are inferred nicely. -/
+
+def shadow1 (x2 : Nat) : Nat → Nat
+  | 0 => 0
+  | .succ n => shadow1 (x2 + 1) n
+decreasing_by decreasing_tactic
+
+
+def some_n : Nat := 1
+def shadow2 (some_n : Nat) : Nat → Nat
+  | 0 => 0
+  | .succ n => shadow2 (some_n + 1) n
+decreasing_by decreasing_tactic
+
+def shadow3 (sizeOf : Nat) : Nat → Nat
+  | 0 => 0
+  | .succ n => shadow3 (sizeOf + 1) n
+decreasing_by decreasing_tactic
+
+def sizeOf : Nat := 2 -- should cause sizeOf to be qualfied below
+
+def qualifiedSizeOf (m : Nat) : Nat → Nat
+  | 0 => 0
+  | .succ n => qualifiedSizeOf (m + 1) n
+decreasing_by decreasing_tactic
+
+end VarNames

tests/lean/guessLex.lean.expected.out

@@ -0,0 +1,50 @@
+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 =>
+  (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

tests/lean/run/guessLexTricky.lean → tests/lean/guessLexTricky.lean

@@ -12,6 +12,8 @@ gets smaller. This needs a backtracking proof search, it seems, which we build h
 (`search_lex`).
 -/
 
+set_option showInferredTerminationBy true
+
 macro_rules | `(tactic| decreasing_trivial) =>
               `(tactic| apply Nat.le_refl)
 macro_rules | `(tactic| decreasing_trivial) =>

tests/lean/guessLexTricky.lean.expected.out

@@ -0,0 +1,5 @@
+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)

tests/lean/run/guessLexTricky2.lean → tests/lean/guessLexTricky2.lean

@@ -6,6 +6,8 @@ Isabelle/HOL” by Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow,
 Works out of the box!
 -/
 
+set_option showInferredTerminationBy true
+
 mutual
 def pedal : Nat → Nat → Nat → Nat
   | 0, _m, c => c

tests/lean/guessLexTricky2.lean.expected.out

@@ -0,0 +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)