grind explodes on a simple example with `Array.range`

[math-fehr]

Description

The following grind call timeouts due to an explosion of applied lemmas:

example (n : Nat) : (Array.range (n + 1)).drop n = #[n] := by
  grind

deactivating two grind patterns removes the timeout:

example (n : Nat) : (Array.range (n + 1)).drop n = #[n] := by
  grind [-Array.range'_append, -Array.range'_append_1]

Here is the grind diagnostics of the exploding grind:

[diag] Diagnostics ▼
  [reduction] unfolded declarations (max: 194611, num: 19): ▼
    [] Array.ofFn ↦ 194611 
    [] Array.range ↦ 190157 
    [] List.rec ↦ 128301 
    [] Nat.rec ↦ 100075 
    [] Add.add ↦ 63713 
    [] HAdd.hAdd ↦ 63713 
    [] HSub.hSub ↦ 32616 
    [] Sub.sub ↦ 32616 
    [] Array.extract ↦ 7907 
    [] Array.ofFn.go✝ ↦ 4781 
    [] Array.range' ↦ 4454 
    [] Append.append ↦ 598 
    [] HAppend.hAppend ↦ 598 
    [] Array.append ↦ 557 
    [] Array.foldl ↦ 557 
    [] Array.foldlM ↦ 557 
    [] OfNat.ofNat ↦ 338 
    [] LE.le ↦ 314 
    [] NatCast.natCast ↦ 90 
  [reduction] unfolded reducible declarations (max: 392221, num: 11): ▼
    [] Array.toList ↦ 392221 
    [] Nat.casesOn ↦ 380208 
    [] List.casesOn ↦ 195797 
    [] Decidable.casesOn ↦ 1614 
    [] Bool.casesOn ↦ 1352 
    [] Nat.cast ↦ 997 
    [] optParam ↦ 593 
    [] List.toArray ↦ 408 
    [] outParam ↦ 56 
    [] Array.take ↦ 30 
    [] List.extract ↦ 30 

Steps to Reproduce

Here is a live.lean-lang.org link:
https://live.lean-lang.org/#codez=KYDwhgtgDgNsAEAKAdvAXPAcmALgSnSQEEAnEsATwDpzkBzBFeAangEY88qATEgeyjxUAXngBiANrIAuulEAjCgCh48OiQCWybvAC0unBojA%2BAVxxKloSLEaoM2fIUSly1WgySpWHLrwFC8KKSMnLwiipqmtrwErqulDRg9MAA5AD6YFBQwNoANHoJ7skMGVk52uls0kpAA

Versions

This fails in lean version v4.35.0-rc1 and v4.34.0

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[gadscand]

I'm working on this issue.

• Edit
  This problem doesn't seem related to the number of maxHeartbeats, but to how grind is unfolding tatics/properties to solve the given example; Therefore, I would highly suggest that such a problem may be addressed by working on the grind it'self, in particular: E‑matching,