any time i have a manual termination proof, I can't simp

Stream: lean4

[Quinn]

minimal (approximately) reproducer:

def minimal (digits1 digits2 : Array UInt64) (carry : UInt64) (acc : Array UInt64) (i : Nat) : Array UInt64 :=
    if i ≥ max digits1.size digits2.size then
      if carry ≠ 0 then acc.push carry
      else acc
    else
      let ai := if h1 : i < digits1.size then digits1[i]'h1 else 0
      let bi := if h2 : i < digits2.size then digits2[i]'h2 else 0
      let sum := ai + bi
      let newCarry := sum % 2
      minimal digits1 digits2 newCarry (acc.push sum) (i + 1)
    termination_by (max digits1.size digits2.size - i)
    decreasing_by
      have h : i < max digits1.size digits2.size := by omega
      generalize g : max digits1.size digits2.size = m
      induction m <;> rw [g] at h <;> omega

def minimk (a b :Array UInt64) : Array UInt64 := minimal a b 0 #[] 0

example : forall x y, minimk x y = minimk y z := by
  intros x y
  simp [minimk]
  simp [minimal]

I love being able to manually specify evidence to the termination checker, theoretically, but I can never actually leverage it when I need to prove stuff.

difficult recursive functions have their imperative equivalents with the identity monad, but it's maybe impossible to exploit inductive structure in an identity monadic "run", so something like a commutativity proof wouldn't work. (?).

However, I can't prove anything like this because stack overflow.

tactic 'simp' failed, nested error:
maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information

setting the options higher doesn't work even when I set it so high that i need to let it run for ten minutes.

[Joachim Breitner]

Often such recursive functions have equations that are not terminating as rewrite rules, so don't use simp to unfold such functions, but use more careful tactics like rw or unfold.

[Quinn]

oh nice! unfold got what i wanted