Maximum recursion depth error

Stream: lean4

[Pim Otte]

In the following example, the last line gives a maximum recursion depth error. Increasing the depth just causes a crash. Any pointers on what I'm doing wrong/how to debug this? (Context: I'm trying to hack a UInt24ish format)

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic.Linarith

def le_sub_one_of_lt (h : n < m) : n ≤ m - 1 := by
  induction h with
  | refl => simp_arith
  | step h ih => {
    simp_arith
    exact Nat.le_trans ih (by simp_arith)
  }

def mwe (a b c : Fin 256) : a.val * 2^16 + b.val * 2^8 + c.val ≤ 2^24 := by
  have h1 : b.val * 2^8 ≤ (2^8-1)*2^8 :=
    Nat.mul_le_mul_of_nonneg_right (le_sub_one_of_lt b.isLt)


  have h2 : a.val * 2^16 ≤ (2^8-1)*2^16 :=
    Nat.mul_le_mul_of_nonneg_right (le_sub_one_of_lt a.isLt)

  have rhs : 2^24 = (2^8-1)*2^16 + (2^8-1)*2^8 + 2^8 := by simp_arith
  simp [ UInt8.toNat, rhs, Nat.add_assoc]
  set_option maxRecDepth 4096 in
  exact Nat.add_le_add (Nat.add_le_add h2 h1) (c.isLt)

[Kyle Miller]

It looks like this works:

theorem mwe (a b c : Fin 256) : a.val * 2^16 + b.val * 2^8 + c.val ≤ 2^24 := by
  have h1 : b.val * 2^8 ≤ (2^8-1)*2^8 :=
    Nat.mul_le_mul_of_nonneg_right (le_sub_one_of_lt b.isLt)

  have h2 : a.val * 2^16 ≤ (2^8-1)*2^16 :=
    Nat.mul_le_mul_of_nonneg_right (le_sub_one_of_lt a.isLt)

  have h3 := Nat.add_le_add (Nat.add_le_add h2 h1) c.isLt.le
  exact h3

[Kyle Miller]

Changing have h3 := to exact causes it to do a maximum recursion depth error.

[Pim Otte]

Thanks! A little experimentation lead me to:

def ineq_uint24 (a b c : Fin 256) : a.val * 2^16 + b.val * 2^8 + c.val < 2^24 := by
  linarith [a.isLt, b.isLt, c.isLt]

which just works.

Do you have any idea why this causes recursion in the first place? Is it trying to unpack the inequality all the way or something?