feat: GuessLex: if no measure is found, explain why (leanprover#2960)

by showing the matrix of calls and measures, and what we know about that
call (=, <, ≤, ?), e.g.

guessLexFailures.lean:27:0-33:31: error: Could not find a decreasing
measure.
    The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
               x1 x2 x3
    1) 29:6-25  =  =  =
    2) 30:6-23  =  ?  <
    3) 31:6-23  <  _  _
    Please use `termination_by` to specify a decreasing measure

It’s a bit more verbose for mutual functions.

It will use the user-specified argument names for functions written
```
foo (n : Nat) := …
```
but not with pattern matching like
```
foo : Nat → … 
  | n => …
```
This can be refined later and separately (and maybe right away in
`expandMatchAltsWhereDecls`).

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

@@ -207,6 +207,8 @@ def SavedLocalContext.run {α} (slc : SavedLocalContext) (k : MetaM α) :
 /-- A `RecCallWithContext` focuses on a single recursive call in a unary predefinition,
 and runs the given action in the context of that call.  -/
 structure RecCallWithContext where
+  /-- Syntax location of reursive call -/
+  ref : Syntax
   /-- Function index of caller -/
   caller : Nat
   /-- Parameters of caller -/
@@ -218,9 +220,9 @@ structure RecCallWithContext where
   ctxt : SavedLocalContext
 
 /-- Store the current recursive call and its context. -/
-def RecCallWithContext.create (caller : Nat) (params : Array Expr) (callee : Nat) (args : Array Expr) :
-    MetaM RecCallWithContext := do
-  return { caller, params, callee, args, ctxt := (← SavedLocalContext.create) }
+def RecCallWithContext.create (ref : Syntax) (caller : Nat) (params : Array Expr) (callee : Nat)
+    (args : Array Expr) : MetaM RecCallWithContext := do
+  return { ref, caller, params, callee, args, ctxt := (← SavedLocalContext.create) }
 
 /-- Given the packed argument of a (possibly) mutual and (possibly) nary call,
 return the function index that is called and the arguments individually.
@@ -273,18 +275,21 @@ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (ariti
       let arg := args[fixedPrefixSize]!
       let (caller, params) ← unpackArg arities param
       let (callee, args) ← unpackArg arities arg
-      RecCallWithContext.create caller params callee args
+      RecCallWithContext.create (← getRef) caller params callee args
 
 /-- A `GuessLexRel` described how a recursive call affects a measure; whether it
 decreases strictly, non-strictly, is equal, or else.  -/
 inductive GuessLexRel | lt | eq | le | no_idea
 deriving Repr, DecidableEq
 
+instance : ToString GuessLexRel where
+  toString | .lt => "<"
+           | .eq => "="
+           | .le => "≤"
+           | .no_idea => "?"
+
 instance : ToFormat GuessLexRel where
-  format | .lt => "<"
-         | .eq => "="
-         | .le => "≤"
-         | .no_idea => "?"
+  format r := toString r
 
 /-- Given a `GuessLexRel`, produce a binary `Expr` that relates two `Nat` values accordingly. -/
 def GuessLexRel.toNatRel : GuessLexRel → Expr
@@ -370,16 +375,13 @@ def RecCallCache.eval (rc: RecCallCache) (paramIdx argIdx : Nat) : MetaM GuessLe
     rc.cache.modify (·.modify paramIdx (·.set! argIdx res))
     return res
 
-/-- Pretty-print the cache entries -/
-def RecCallCache.pretty (rc : RecCallCache) : IO Format := do
-  let mut r := Format.nil
-  let d ← rc.cache.get
-  for h₁ : paramIdx in [:d.size] do
-    for h₂ : argIdx in [:(d[paramIdx]'h₁.2).size] do
-      if let .some entry := (d[paramIdx]'h₁.2)[argIdx]'h₂.2 then
-        r := r ++
-          f!"(Param {paramIdx}, arg {argIdx}): {entry}" ++ Format.line
-  return r
+
+/-- Print a single cache entry as a string, without forcing it -/
+def RecCallCache.prettyEntry (rcc : RecCallCache) (paramIdx argIdx : Nat) : MetaM String := do
+  let cachedEntries ← rcc.cache.get
+  return match cachedEntries[paramIdx]![argIdx]! with
+  | .some rel => toString rel
+  | .none => "_"
 
 /-- The measures that we order lexicographically can be comparing arguments,
 or numbering the functions -/
@@ -551,6 +553,103 @@ def buildTermWF (declNames : Array Name) (varNamess : Array (Array Name))
       }
   return .ext termByElements
 
+
+/--
+Given a matrix (row-major) of strings, arranges them in tabular form.
+First column is left-aligned, others right-aligned.
+Single space as column separator.
+-/
+def formatTable : Array (Array String) → String := fun xss => Id.run do
+  let mut colWidths := xss[0]!.map (fun _ => 0)
+  for i in [:xss.size] do
+    for j in [:xss[i]!.size] do
+      if xss[i]![j]!.length > colWidths[j]! then
+        colWidths := colWidths.set! j xss[i]![j]!.length
+  let mut str := ""
+  for i in [:xss.size] do
+    for j in [:xss[i]!.size] do
+      let s := xss[i]![j]!
+      if j > 0 then -- right-align
+        for _ in [:colWidths[j]! - s.length] do
+          str := str ++ " "
+      str := str ++ s
+      if j = 0 then -- left-align
+        for _ in [:colWidths[j]! - s.length] do
+          str := str ++ " "
+      if j + 1 < xss[i]!.size then
+        str := str ++ " "
+    if i + 1 < xss.size then
+      str := str ++ "\n"
+  return str
+
+/-- Concise textual representation of the source location of a recursive call  -/
+def RecCallWithContext.posString (rcc : RecCallWithContext) : MetaM String := do
+  let fileMap ← getFileMap
+  let .some pos := rcc.ref.getPos? | return ""
+  let position := fileMap.toPosition pos
+  let endPosStr := match rcc.ref.getTailPos? with
+  | some endPos =>
+    let endPosition := fileMap.toPosition endPos
+    if endPosition.line = position.line then
+      s!"-{endPosition.column}"
+    else
+      s!"-{endPosition.line}:{endPosition.column}"
+  | none        => ""
+  return s!"{position.line}:{position.column}{endPosStr}"
+
+
+/-- Explain what we found out about the recursive calls (non-mutual case) -/
+def explainNonMutualFailure (varNames : Array Name) (rcs : Array RecCallCache) : MetaM Format := do
+  let header := varNames.map (·.eraseMacroScopes.toString)
+  let mut table : Array (Array String) := #[#[""] ++ header]
+  for i in [:rcs.size], rc in rcs do
+    let mut row := #[s!"{i+1}) {← rc.rcc.posString}"]
+    for argIdx in [:varNames.size] do
+      row := row.push (← rc.prettyEntry argIdx argIdx)
+    table := table.push row
+
+  return formatTable table
+
+/-- Explain what we found out about the recursive calls (mutual case) -/
+def explainMutualFailure (declNames : Array Name) (varNamess : Array (Array Name))
+    (rcs : Array RecCallCache) : MetaM Format := do
+  let mut r := Format.nil
+
+  for rc in rcs do
+    let caller := rc.rcc.caller
+    let callee := rc.rcc.callee
+    r := r ++ f!"Call from {declNames[caller]!} to {declNames[callee]!} " ++
+      f!"at {← rc.rcc.posString}:\n"
+
+    let header := varNamess[caller]!.map (·.eraseMacroScopes.toString)
+    let mut table : Array (Array String) := #[#[""] ++ header]
+    if caller = callee then
+      -- For self-calls, only the diagonal is interesting, so put it into one row
+      let mut row := #[""]
+      for argIdx in [:varNamess[caller]!.size] do
+        row := row.push (← rc.prettyEntry argIdx argIdx)
+      table := table.push row
+    else
+      for argIdx in [:varNamess[callee]!.size] do
+        let mut row := #[]
+        row := row.push varNamess[callee]![argIdx]!.eraseMacroScopes.toString
+        for paramIdx in [:varNamess[caller]!.size] do
+          row := row.push (← rc.prettyEntry paramIdx argIdx)
+        table := table.push row
+    r := r ++ formatTable table ++ "\n"
+
+  return r
+
+def explainFailure (declNames : Array Name) (varNamess : Array (Array Name))
+    (rcs : Array RecCallCache) : MetaM Format := do
+  let mut r : Format := "The arguments relate at each recursive call as follows:\n" ++
+    "(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)\n"
+  if declNames.size = 1 then
+    r := r ++ (← explainNonMutualFailure varNamess[0]! rcs)
+  else
+    r := r ++ (← explainMutualFailure declNames varNamess rcs)
+  return r
+
 end Lean.Elab.WF.GuessLex
 
 namespace Lean.Elab.WF
@@ -566,33 +665,32 @@ terminates. See the module doc string for a high-level overview.
 def guessLex (preDefs : Array PreDefinition)  (unaryPreDef : PreDefinition)
     (fixedPrefixSize : Nat) (decrTactic? : Option Syntax) :
     MetaM TerminationWF := do
-  try
-    let varNamess ← preDefs.mapM (naryVarNames fixedPrefixSize ·)
-    let arities := varNamess.map (·.size)
-    trace[Elab.definition.wf] "varNames is: {varNamess}"
-
-    let forbiddenArgs ← preDefs.mapM fun preDef =>
-      getForbiddenByTrivialSizeOf fixedPrefixSize preDef
-
-    -- The list of measures, including the measures that order functions.
-    -- The function ordering measures come last
-    let measures ← generateMeasures forbiddenArgs arities
-
-    -- If there is only one plausible measure, use that
-    if let #[solution] := measures then
-      return ← buildTermWF (preDefs.map (·.declName)) varNamess #[solution]
-
-    -- Collect all recursive calls and extract their context
-    let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities
-    let rcs ← recCalls.mapM (RecCallCache.mk decrTactic? ·)
-    let callMatrix := rcs.map (inspectCall ·)
-
-    match ← liftMetaM <| solve measures callMatrix with
-    | .some solution => do
-      let wf ← buildTermWF (preDefs.map (·.declName)) varNamess solution
-      return wf
-    | .none => throwError "Cannot find a decreasing lexicographic order"
-  catch _ =>
-    -- Hide all errors from guessing lexicographic orderings, as before
-    -- Future work: explain the failure to the user, like  Isabelle does
-    throwError "failed to prove termination, use `termination_by` to specify a well-founded relation"
+  let varNamess ← preDefs.mapM (naryVarNames fixedPrefixSize ·)
+  let arities := varNamess.map (·.size)
+  trace[Elab.definition.wf] "varNames is: {varNamess}"
+
+  let forbiddenArgs ← preDefs.mapM fun preDef =>
+    getForbiddenByTrivialSizeOf fixedPrefixSize preDef
+
+  -- The list of measures, including the measures that order functions.
+  -- The function ordering measures come last
+  let measures ← generateMeasures forbiddenArgs arities
+
+  -- If there is only one plausible measure, use that
+  if let #[solution] := measures then
+    return ← buildTermWF (preDefs.map (·.declName)) varNamess #[solution]
+
+  -- Collect all recursive calls and extract their context
+  let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities
+  let rcs ← recCalls.mapM (RecCallCache.mk decrTactic? ·)
+  let callMatrix := rcs.map (inspectCall ·)
+
+  match ← liftMetaM <| solve measures callMatrix with
+  | .some solution => do
+    let wf ← buildTermWF (preDefs.map (·.declName)) varNamess solution
+    return wf
+  | .none =>
+    let explanation ← explainFailure (preDefs.map (·.declName)) varNamess rcs
+    Lean.throwError <| "Could not find a decreasing measure.\n" ++
+      explanation ++ "\n" ++
+      "Please use `termination_by` to specify a decreasing measure."

tests/lean/guessLexFailures.lean

@@ -17,21 +17,117 @@ def nonTerminating2 : Nat → Nat → Nat
   | n, m => nonTerminating2 (.succ n) (.succ m)
 decreasing_by decreasing_tactic
 
+def noArguments : Nat := noArguments
 
--- The GuessLex code does not like eta-contracted motives in `casesOn`.
--- At the time of writing, the error message is swallowed
--- When guessing the lexicographic order becomes more verbose this will improve.
+def noNonFixedArguments (n : Nat) : Nat := noNonFixedArguments n
+
+def Array.sum (xs : Array Nat) : Nat := xs.foldl (init := 0) Nat.add
+
+namespace InterestingMatrix
+def f : (n m l : Nat) → Nat
+  | n+1, m+1, l+1 => #[
+      f (n+1) (m+1) (l+1),
+      f (n+1) (m-1) (l),
+      f (n)   (m+1) (l) ].sum
+  | _, _, _ => 0
+decreasing_by decreasing_tactic
+end InterestingMatrix
+
+namespace InterestingMatrixWithForbiddenArguments
+def f : (n m : Nat) → (h : True) → Nat → Nat
+  | n+1, m+1, h, l+1 => #[
+      f (n+1) (m+1) h (l+1),
+      f (n+1) (m-1) h (l),
+      f (n)   (m+1) h (l) ].sum
+  | _, _, _, _ => 0
+decreasing_by decreasing_tactic
+end InterestingMatrixWithForbiddenArguments
+
+namespace InterestingMatrixWithNames
+-- Hopefully eventually lean will pick up names even with pattern match syntax
+def f (n m l : Nat) : Nat := match n, m, l with
+  | n+1, m+1, l+1 => #[
+      f (n+1) (m+1) (l+1),
+      f (n+1) (m-1) (l),
+      f (n)   (m+1) (l) ].sum
+  | _, _, _ => 0
+decreasing_by decreasing_tactic
+end InterestingMatrixWithNames
+
+namespace Mutual
+mutual
+  def f (fixed n m l : Nat) : Nat := match n, m, l with
+    | n+1, m+1, l+1 => #[
+        f fixed (n+1) (m+1) (l+1),
+        f fixed (n+1) (m-1) (l),
+        g fixed (n)   (m+1) trivial (l)].sum
+    | _, _, _ => 0
+
+  def g (fixed n m : Nat) (H : True) (l : Nat) : Nat := match n, m, l with
+    | n+1, m+1, l+1 => #[
+        g fixed (m+1) (n+1) H (l+1),
+        g fixed (m+1) (n-1) H (l),
+        h fixed (m)   (n+1)  ].sum
+    | _, _, _ => 0
+
+  def h (fixed : Nat) : (n m : Nat) -> Nat
+    | n+1, m+1 => #[
+        f fixed (n+1) (m+1) (n+1),
+        h fixed (n+1) (m-1),
+        h fixed (n)   (m+1) ].sum
+    | _, _ => 0
+end
+end Mutual
+
+
+namespace DuplicatedCall
+
+def dup (a : Nat) (b : Nat := a) := a + b
+
+def f : (n m : Nat) → Nat
+  | 0, m => m
+  | n+1, m => dup (f (n+2) (m+1))
+
+end DuplicatedCall
+
+namespace TrickyCode
+
+-- These tests run GuessLex on peculiar code that it once stumbled over, or might
+-- stumble over in the future.
+
+-- The GuessLex code at some point did not like eta-contracted motives in `casesOn`.
 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
 decreasing_by decreasing_tactic
--- termination_by badCasesOn n => n
 
 
--- Like above, but now with a `casesOn` alternative with insufficient lambdas
-def Fin_succ_comp (f : (n : Nat) → Fin (n + 1)) : (n : Nat) → Fin (n + 2) := fun n => Fin.succ (f n)
+-- This actually also fails with an explicit termination_by, and could be fixed
+-- by eta-expanding the motive.
+-- TODO: Fix by using eta-expanding variant of lambdaTelescope, e.g.
+-- 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
+decreasing_by decreasing_tactic
+
+-- The GuessLex code at does not like `casesOn` alternative with insufficient lambdas
+-- TODO: Fix by using eta-expanding variant of lambdaTelescope, e.g.
+-- https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Going.20under.20exactly.20one.20lambda/near/404278529
+def Fin_succ_comp (f : (n : Nat) → Fin (n + 1)) : (n : Nat) → Fin (n + 2) := fun n => Fin.succ (f n)
+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
+decreasing_by decreasing_tactic
+
+
+-- Same test, explicit termination_by
+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 => badCasesOn2 n (.succ m)))
+      (Fin_succ_comp (fun n => badCasesOn4 n (.succ m)))
+termination_by badCasesOn4 n m => n
 decreasing_by decreasing_tactic
--- termination_by badCasesOn2 n => n
+
+end TrickyCode