congr tactic hitting max recursion depth

Stream: mathlib4

[David Renshaw]

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Tactic.Ring

theorem foo (x : ℤ) :
   ∑ i in Finset.range 89, ((x + i) + 1)^2 =
   ∑ i in Finset.range 89, (x^2 + 2 * x * ((i:ℤ) + 1) + ((i:ℤ) + 1)^2) := by

  -- The presence of this lemma causes the `congr` below to fail.
  -- The proof works if I comment this out.
  have h : ∑ i in Finset.range 89, ((i:ℤ) + 1) = ∑ i in Finset.range 90, (i:ℤ) := sorry

  congr -- maximum recursion depth has been reached
  funext
  ring

[David Renshaw]

the exactly analogous lean 3 code works without a problem

[David Renshaw]

(This came up here: https://github.com/dwrensha/math-puzzles-in-lean4/commit/a3fb8f0df595030dde7b914672f189cbe98871b8 )

[David Renshaw]

It succeeds if I turn off closePost:

syntax (name:= congrPrime) "congr'" : tactic

elab_rules :tactic | `(tactic| congr') => do
  Lean.Elab.Tactic.liftMetaTactic fun mvarId => mvarId.congrN (closePost := false)

[David Renshaw]

It looks to me like this isDefEq is where the recursion depth gets exceeded: https://github.com/leanprover/lean4/blob/a125a36bcc79a28963ed5786f94c5d97648a8f99/src/Lean/Meta/Tactic/Assumption.lean#L15

[David Renshaw]

Is there a reason that isDefEq would have trouble with expressions like ∑ i in Finset.range 89, ((i:ℤ) + 1) ?

[Mario Carneiro]

you can use with_reducible congr to avoid the more expensive defeq check

[Mario Carneiro]

The current implementation tries a weak refl before descending into subterms, and a strong refl if we don't have any better ideas. The strong refl can potentially explode if you have a big definition stack and similar looking terms

[Mario Carneiro]

the same thing presumably happens if you attempt to prove the goal using exact h

[David Renshaw]

yep

[Mario Carneiro]

I believe this design was lifted straight from lean 3, so perhaps the difference is not in congr but in some @[irreducible] markings?

[David Renshaw]

yeah, my hypothesis is that something about finsets is less opaque than it was in lean 3

[David Renshaw]

with_reducible makes it work: https://github.com/dwrensha/math-puzzles-in-lean4/commit/f0f50f570e6f1f2b5f3ba024cbce89c43a63371b