feat: tweak behavior of congrN to match lean 3 (#1798)

src/Lean/Meta/Tactic/Congr.lean

@@ -14,17 +14,16 @@ namespace Lean
 open Meta
 
 /--
-Postprocessor after applying congruence theorem.
+Preprocessor before applying congruence theorem.
 Tries to close new goals using `Eq.refl`, `HEq.refl`, and `assumption`.
 It also tries to apply `heq_of_eq`.
 -/
-private def congrPost (mvarIds : List MVarId) : MetaM (List MVarId) :=
-  mvarIds.filterMapM fun mvarId => do
-    let mvarId ← mvarId.heqOfEq
-    try mvarId.refl; return none catch _ => pure ()
-    try mvarId.hrefl; return none catch _ => pure ()
-    if (← mvarId.assumptionCore) then return none
-    return some mvarId
+def MVarId.congrPre (mvarId : MVarId) : MetaM (Option MVarId) := do
+  let mvarId ← mvarId.heqOfEq
+  try mvarId.refl; return none catch _ => pure ()
+  try mvarId.hrefl; return none catch _ => pure ()
+  if (← mvarId.assumptionCore) then return none
+  return some mvarId
 
 /--
 Asserts the given congruence theorem as fresh hypothesis, and then applies it.
@@ -75,11 +74,10 @@ def MVarId.congrImplies? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
 
 /--
 Given a goal of the form `⊢ f as = f bs`, `⊢ (p → q) = (p' → q')`, or `⊢ HEq (f as) (f bs)`, try to apply congruence.
-It takes proof irrelevance into account, the fact that `Decidable p` is a subsingleton.
-If `closeEasy := true`, it tries to close new subgoals using `Eq.refl`, `HEq.refl`, and `assumption`.
+It takes proof irrelevance into account, and the fact that `Decidable p` is a subsingleton.
 -/
-def MVarId.congr (mvarId : MVarId) (closeEasy := true) : MetaM (List MVarId) := do
-  let mvarIds ← if let some mvarIds ← mvarId.congr? then
+def MVarId.congrCore (mvarId : MVarId) : MetaM (List MVarId) := do
+  if let some mvarIds ← mvarId.congr? then
     pure mvarIds
   else if let some mvarIds ← mvarId.hcongr? then
     pure mvarIds
@@ -87,26 +85,33 @@ def MVarId.congr (mvarId : MVarId) (closeEasy := true) : MetaM (List MVarId) :=
     pure mvarIds
   else
     throwTacticEx `congr mvarId "failed to apply congruence"
-  if closeEasy then
-    congrPost mvarIds
-  else
-    return mvarIds
 
 /--
-Applies `congr` recursively up to depth `n`.
+Given a goal of the form `⊢ f as = f bs`, `⊢ (p → q) = (p' → q')`, or `⊢ HEq (f as) (f bs)`, try to apply congruence.
+It takes proof irrelevance into account, and the fact that `Decidable p` is a subsingleton.
+
+* Applies `congr` recursively up to depth `depth`.
+* If `closePre := true`, it will attempt to close new goals
+  using `Eq.refl`, `HEq.refl`, and `assumption` with reducible transparency.
+* If `closePost := true`, it will try again on goals on which `congr` failed to make progress
+  with default transparency.
 -/
-def MVarId.congrN (mvarId : MVarId) (n : Nat) : MetaM (List MVarId) := do
-  if n == 1 then
-    mvarId.congr
-  else
-    let (_, s) ← go n mvarId |>.run #[]
-    return s.toList
+def MVarId.congrN (mvarId : MVarId) (depth : Nat := 1000000) (closePre := true) (closePost := true) : MetaM (List MVarId) := do
+  let (_, s) ← go depth mvarId |>.run #[]
+  return s.toList
 where
+  post (mvarId : MVarId) : StateRefT (Array MVarId) MetaM Unit := do
+    if closePost && (← getTransparency) != .reducible then
+      if let some mvarId ← mvarId.congrPre then
+        modify (·.push mvarId)
+    else
+      modify (·.push mvarId)
+
   go (n : Nat) (mvarId : MVarId) : StateRefT (Array MVarId) MetaM Unit := do
-    match n with
-    | 0 => modify (·.push mvarId)
-    | n+1 =>
-      let some mvarIds ← observing? (m := MetaM) mvarId.congr
-        | modify (·.push mvarId)
-      mvarIds.forM (go n)
-end Lean
+    if let some mvarId ← if closePre then withReducible mvarId.congrPre else pure mvarId then
+      match n with
+      | 0 => post mvarId
+      | n+1 =>
+        let some mvarIds ← observing? (m := MetaM) mvarId.congrCore
+          | post mvarId
+        mvarIds.forM (go n)