Termination of range function

Stream: general

[Anders Christiansen Sørby]

I'm trying to implement a function which generates a range from a bounded Nat (BNat)

def BNat.range {min max} {h' : min ≤ max} : List $ BNat min max h' :=
  let rec @[specialize] it : BNat min max h' → (List $ BNat min max h') := (λ n =>
    if h : n.val < max then
      List.cons n $ it
        { val := Nat.succ n.val
        , isLe := (by apply h)
        , isGe := (by
          apply ge_is_le
          apply Nat.le_of_lt
          apply Nat.lt_succ_of_le
          apply n.isGe
        )
        }
    else
      [BNat.mk n.val (by apply n.isLe) n.isGe]
  )
  it (BNat.mk min h' (by apply ge_refl))
termination_by measure λ b => b.snd.snd.snd.val
decreasing_by exact (by simp)

How do I prove that the function will eventually reach n.val = max and terminate?

[Yaël Dillies]

I assume this is Lean 4? You might want to migrate to #lean4