feat: include congruence theorems at simp diagnostic information (#4043)

src/Lean/Meta/Diagnostics.lean

@@ -35,7 +35,8 @@ structure DiagSummary where
 def DiagSummary.isEmpty (s : DiagSummary) : Bool :=
   s.data.isEmpty
 
-def mkDiagSummary (counters : PHashMap Name Nat) (threshold : Nat) (p : Name → Bool := fun _ => true) : MetaM DiagSummary := do
+def mkDiagSummary (counters : PHashMap Name Nat) (p : Name → Bool := fun _ => true) : MetaM DiagSummary := do
+  let threshold := diagnostics.threshold.get (← getOptions)
   let entries := collectAboveThreshold counters threshold p Name.lt
   if entries.isEmpty then
     return {}
@@ -46,21 +47,18 @@ def mkDiagSummary (counters : PHashMap Name Nat) (threshold : Nat) (p : Name →
     return { data, max := entries[0]!.2 }
 
 def mkDiagSummaryForUnfolded (counters : PHashMap Name Nat) (instances := false) : MetaM DiagSummary := do
-  let threshold := diagnostics.threshold.get (← getOptions)
   let env ← getEnv
-  mkDiagSummary counters threshold fun declName =>
+  mkDiagSummary counters fun declName =>
     getReducibilityStatusCore env declName matches .semireducible
     && isInstanceCore env declName == instances
 
 def mkDiagSummaryForUnfoldedReducible (counters : PHashMap Name Nat) : MetaM DiagSummary := do
-  let threshold := diagnostics.threshold.get (← getOptions)
   let env ← getEnv
-  mkDiagSummary counters threshold fun declName =>
+  mkDiagSummary counters fun declName =>
     getReducibilityStatusCore env declName matches .reducible
 
 def mkDiagSummaryForUsedInstances : MetaM DiagSummary := do
-  let threshold := diagnostics.threshold.get (← getOptions)
-  mkDiagSummary (← get).diag.heuristicCounter threshold
+  mkDiagSummary (← get).diag.heuristicCounter
 
 def appendSection (m : MessageData) (cls : Name) (header : String) (s : DiagSummary) : MessageData :=
   if s.isEmpty then
@@ -71,12 +69,11 @@ def appendSection (m : MessageData) (cls : Name) (header : String) (s : DiagSumm
 
 def reportDiag : MetaM Unit := do
   if (← isDiagnosticsEnabled) then
-    let threshold := diagnostics.threshold.get (← getOptions)
     let unfoldCounter := (← get).diag.unfoldCounter
     let unfoldDefault ← mkDiagSummaryForUnfolded unfoldCounter
     let unfoldInstance ← mkDiagSummaryForUnfolded unfoldCounter (instances := true)
     let unfoldReducible ← mkDiagSummaryForUnfoldedReducible unfoldCounter
-    let heu ← mkDiagSummary (← get).diag.heuristicCounter threshold
+    let heu ← mkDiagSummary (← get).diag.heuristicCounter
     let inst ← mkDiagSummaryForUsedInstances
     unless unfoldDefault.isEmpty && unfoldInstance.isEmpty && unfoldReducible.isEmpty && heu.isEmpty && inst.isEmpty do
       let m := MessageData.nil

src/Lean/Meta/Tactic/Simp/Diagnostics.lean

@@ -36,6 +36,7 @@ def reportDiag (diag : Simp.Diagnostics) (diagOrig : Meta.Diagnostics) : MetaM U
   if (← isDiagnosticsEnabled) then
     let used ← mkSimpDiagSummary diag.usedThmCounter
     let tried ← mkSimpDiagSummary diag.triedThmCounter diag.usedThmCounter
+    let congr ← mkDiagSummary diag.congrThmCounter
     let unfoldCounter := subCounters (← get).diag.unfoldCounter diagOrig.unfoldCounter
     let unfoldDefault ← mkDiagSummaryForUnfolded unfoldCounter
     let unfoldInstance ← mkDiagSummaryForUnfolded unfoldCounter (instances := true)
@@ -44,6 +45,7 @@ def reportDiag (diag : Simp.Diagnostics) (diagOrig : Meta.Diagnostics) : MetaM U
       let m := MessageData.nil
       let m := appendSection m `simp "used theorems" used
       let m := appendSection m `simp "tried theorems" tried
+      let m := appendSection m `simp "tried congruence theorems" congr
       let m := appendSection m `reduction "unfolded declarations" unfoldDefault
       let m := appendSection m `reduction "unfolded instances" unfoldInstance
       let m := appendSection m `reduction "unfolded reducible declarations" unfoldReducible

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -520,6 +520,7 @@ def processCongrHypothesis (h : Expr) : SimpM Bool := do
 
 /-- Try to rewrite `e` children using the given congruence theorem -/
 def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Result) := withNewMCtxDepth do
+  recordCongrTheorem c.theoremName
   trace[Debug.Meta.Tactic.simp.congr] "{c.theoremName}, {e}"
   let thm ← mkConstWithFreshMVarLevels c.theoremName
   let (xs, bis, type) ← forallMetaTelescopeReducing (← inferType thm)

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -90,6 +90,7 @@ structure Context where
   -/
   parent?           : Option Expr := none
   dischargeDepth    : UInt32 := 0
+
   deriving Inhabited
 
 def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
@@ -103,6 +104,8 @@ structure Diagnostics where
   usedThmCounter : PHashMap Origin Nat := {}
   /-- Number of times each simp theorem has been tried. -/
   triedThmCounter : PHashMap Origin Nat := {}
+  /-- Number of times each congr theorem has been tried. -/
+  congrThmCounter : PHashMap Name Nat := {}
   deriving Inhabited
 
 structure State where
@@ -308,14 +311,14 @@ Save current cache, reset it, execute `x`, and then restore original cache.
   withFreshCache <| withReader (fun r => { MethodsRef.toMethods r with discharge? }.toMethodsRef) x
 
 def recordTriedSimpTheorem (thmId : Origin) : SimpM Unit := do
-  modifyDiag fun { usedThmCounter, triedThmCounter } =>
+  modifyDiag fun { usedThmCounter, triedThmCounter, congrThmCounter } =>
     let cNew := if let some c := triedThmCounter.find? thmId then c + 1 else 1
-    { usedThmCounter, triedThmCounter := triedThmCounter.insert thmId cNew }
+    { usedThmCounter, triedThmCounter := triedThmCounter.insert thmId cNew, congrThmCounter }
 
 def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
-  modifyDiag fun { usedThmCounter, triedThmCounter } =>
+  modifyDiag fun { usedThmCounter, triedThmCounter, congrThmCounter } =>
     let cNew := if let some c := usedThmCounter.find? thmId then c + 1 else 1
-    { usedThmCounter := usedThmCounter.insert thmId cNew, triedThmCounter }
+    { usedThmCounter := usedThmCounter.insert thmId cNew, triedThmCounter, congrThmCounter }
   /-
   If `thmId` is an equational theorem (e.g., `foo.eq_1`), we should record `foo` instead.
   See issue #3547.
@@ -335,6 +338,11 @@ def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
     let n := s.usedTheorems.size
     { s with usedTheorems := s.usedTheorems.insert thmId n }
 
+def recordCongrTheorem (declName : Name) : SimpM Unit := do
+  modifyDiag fun { usedThmCounter, triedThmCounter, congrThmCounter } =>
+    let cNew := if let some c := congrThmCounter.find? declName then c + 1 else 1
+    { congrThmCounter := congrThmCounter.insert declName cNew, triedThmCounter, usedThmCounter }
+
 def Result.getProof (r : Result) : MetaM Expr := do
   match r.proof? with
   | some p => return p