fix: WF.Fix: deduplicate subsumed goals before running tactic (leanpr…

…over#3024)

before code like

    def dup (a : Nat) (b : Nat := a) := a + b

    def rec : Nat → Nat
     | 0 => 1
     | n+1 => dup (dup (dup (rec n)))
    decreasing_by decreasing_tactic

would run the `decreasing_tactic` 8 tims, because the recursive call
`rec n` gets duplicate due to the default paramter. Similar effects can
be observed due to dependent types or tactics like `cases`.

This is wasteful, and is confusing to the user when they use
`decreasing_by` interactively. Therfore, we now go through the proof
obligations (MVars) and if solving one would imply solving another one,
we assign the mvars to each other accordingly.

This PR is a sibling of leanprover#3004.

src/Lean/Data/Array.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+import Init.Data.Array
+
+namespace Array
+
+/-!
+This module contains utility functions involving Arrays that are useful in a few places
+of the lean code base, but too specialized to live in `Init.Data.Array`, which arguably
+is part of the public, user-facing standard library.
+-/
+
+/--
+Given an array `a`, runs `f xᵢ xⱼ` for all `i < j`, removes those entries for which `f` returns
+`false` (and will subsequently skip pairs if one element is removed), and returns the array of
+remaining elements.
+
+This can be used to remove elements from an array where a “better” element, in some partial
+order, exists in the array.
+-/
+def filterPairsM {m} [Monad m] {α} (a : Array α) (f : α → α → m (Bool × Bool)) :
+    m (Array α) := do
+  let mut removed := Array.mkArray a.size false
+  let mut numRemoved := 0
+  for h1 : i in [:a.size] do for h2 : j in [i+1:a.size] do
+    unless removed[i]! || removed[j]! do
+      let xi := a[i]'h1.2
+      let xj := a[j]'h2.2
+      let (keepi, keepj) ← f xi xj
+      unless keepi do
+        numRemoved := numRemoved + 1
+        removed := removed.set! i true
+      unless keepj do
+        numRemoved := numRemoved + 1
+        removed := removed.set! j true
+  let mut a' := Array.mkEmpty numRemoved
+  for h : i in [:a.size] do
+    unless removed[i]! do
+      a' := a'.push (a[i]'h.2)
+  return a'
+
+end Array

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.Data.Array
 
 namespace Lean.Elab.WF
 open Meta
@@ -165,8 +166,29 @@ private def applyDefaultDecrTactic (mvarId : MVarId) : TermElabM Unit := do
   unless remainingGoals.isEmpty do
     Term.reportUnsolvedGoals remainingGoals
 
+/-
+Given an array of MVars, assign MVars with equal type and subsumed local context to each other.
+Returns those MVar that did not get assigned.
+-/
+def assignSubsumed (mvars : Array MVarId) : MetaM (Array MVarId) :=
+  mvars.filterPairsM fun mv₁ mv₂ => do
+    let mvdecl₁ ← mv₁.getDecl
+    let mvdecl₂ ← mv₂.getDecl
+    if mvdecl₁.type == mvdecl₂.type then
+      -- same goals; check contexts.
+        if mvdecl₁.lctx.isSubPrefixOf mvdecl₂.lctx then
+          -- mv₁ is better
+          mv₂.assign (.mvar mv₁)
+          return (true, false)
+        if mvdecl₂.lctx.isSubPrefixOf mvdecl₁.lctx then
+          -- mv₂ is better
+          mv₁.assign (.mvar mv₂)
+          return (false, true)
+    return (true, true)
+
 def solveDecreasingGoals (decrTactic? : Option Syntax) (value : Expr) : MetaM Expr := do
   let goals ← getMVarsNoDelayed value
+  let goals ← assignSubsumed goals
   goals.forM fun goal => Lean.Elab.Term.TermElabM.run' <|
     match decrTactic? with
     | none => do

tests/lean/issue2981.lean.expected.out

@@ -1,14 +1,4 @@
 Tactic is run (ideally only once)
-Tactic is run (ideally only once)
-Tactic is run (ideally only once)
-Tactic is run (ideally only once)
-Tactic is run (ideally only once)
-Tactic is run (ideally only once)
-Tactic is run (ideally only once)
-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)
@@ -18,16 +8,9 @@ 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)
 Tactic is run (ideally only once, in most general context)
 n : Nat
 ⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 n (Nat.succ n)
-n : Nat h : n ≠ n ⊢ (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)
 Tactic is run (ideally only twice, in most general context)
@@ -39,7 +22,3 @@ h : n ≠ n
 n m : Nat
 ⊢ (invImage (fun a => PSigma.casesOn a fun x1 snd => sizeOf x1) instWellFoundedRelation).1 { fst := n, snd := m + 1 }
     { fst := Nat.succ n, snd := m }
-n m : Nat
-h : n ≠ n
-⊢ (invImage (fun a => PSigma.casesOn a fun x1 snd => sizeOf x1) instWellFoundedRelation).1 { fst := n, snd := m + 1 }
-    { fst := Nat.succ n, snd := m }