fix: GuessLex: deduplicate recursive calls (leanprover#3004)

The elaborator is prone to duplicate terms, including recursive calls,
even if the user only wrote a single one. This duplication is wasteful
if we run the tactics on duplicated calls, and confusing in the output
of GuessLex. So prune the list of recursive calls, and remove those
where another call exists that has the same goal and context that is no
more specific.

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.Data.Array
 
 
 /-!
@@ -240,6 +241,29 @@ def RecCallWithContext.create (ref : Syntax) (caller : Nat) (params : Array Expr
     (args : Array Expr) : MetaM RecCallWithContext := do
   return { ref, caller, params, callee, args, ctxt := (← SavedLocalContext.create) }
 
+
+/--
+The elaborator is prone to duplicate terms, including recursive calls, even if the user
+only wrote a single one. This duplication is wasteful if we run the tactics on duplicated
+calls, and confusing in the output of GuessLex. So prune the list of recursive calls,
+and remove those where another call exists that has the same goal and context that is no more
+specific.
+-/
+def filterSubsumed (rcs : Array RecCallWithContext ) : Array RecCallWithContext := Id.run do
+  rcs.filterPairsM fun rci rcj => do
+    if rci.caller == rcj.caller && rci.callee == rcj.callee &&
+      rci.params == rcj.params && rci.args == rcj.args then
+      -- same goals; check contexts.
+        let lci := rci.ctxt.savedLocalContext
+        let lcj := rcj.ctxt.savedLocalContext
+        if lci.isSubPrefixOf lcj then
+          -- rci is better
+          return (true, false)
+        else if lcj.isSubPrefixOf lci then
+          -- rcj is better
+          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.
 
@@ -697,6 +721,7 @@ def guessLex (preDefs : Array PreDefinition)  (unaryPreDef : PreDefinition)
 
   -- 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 callMatrix := rcs.map (inspectCall ·)
 

tests/lean/guessLexFailures.lean.expected.out

@@ -122,7 +122,6 @@ The arguments relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
             x1 x2
 1) 89:19-32  ?  ?
-2) 89:19-32  _  _
 Please use `termination_by` to specify a decreasing measure.
 guessLexFailures.lean:100:0-103:31: error: Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:

tests/lean/issue2981.lean.expected.out

@@ -1,23 +1,12 @@
 Tactic is run (ideally only once)
 Tactic is run (ideally only twice)
 Tactic is run (ideally only twice)
-Tactic is run (ideally only twice)
-Tactic is run (ideally only twice)
-Tactic is run (ideally only twice)
-Tactic is run (ideally only twice)
-Tactic is run (ideally only twice)
-Tactic is run (ideally only twice)
-Tactic is run (ideally only twice)
 Tactic is run (ideally only once, in most general context)
 n : Nat
 ⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 n (Nat.succ n)
 Tactic is run (ideally only twice, in most general context)
 Tactic is run (ideally only twice, in most general context)
-Tactic is run (ideally only twice, in most general context)
-n : Nat
-⊢ sizeOf n < sizeOf (Nat.succ n)
 n : Nat
-h : n ≠ n
 ⊢ sizeOf n < sizeOf (Nat.succ n)
 n m : Nat
 ⊢ (invImage (fun a => PSigma.casesOn a fun x1 snd => sizeOf x1) instWellFoundedRelation).1 { fst := n, snd := m + 1 }