English
For fixed b and f, the length of the result of toDigitsCore with argument (c :: tl) equals the length with tl, plus 1.
Русский
Для фиксированных b и f длина результата toDigitsCore при аргументе (c :: tl) равна длине при tl плюс 1.
LaTeX
$$$ (\\mathrm{toDigitsCore}\\ b\\ f\\ n\\ (c :: tl)).length = (\\mathrm{toDigitsCore}\\ b\\ f\\ n\\ tl).length + 1 $$$
Lean4
theorem toDigitsCore_lens_eq_aux (b f : Nat) :
∀ (n : Nat) (l1 l2 : List Char),
l1.length = l2.length → (Nat.toDigitsCore b f n l1).length = (Nat.toDigitsCore b f n l2).length :=
by
induction f with (simp only [Nat.toDigitsCore]; intro n l1 l2 hlen)
| zero => assumption
| succ f ih =>
if hx : n / b = 0 then simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
else
simp only [hx, if_false]
specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih
exact ih trivial
