feat: lemmas about Nat.toDigits

[marcusrossel]

As discussed in leanprover/lean4#8673.

[fgdorais]

Please summarize the discussion rather than just linking to it. That makes it easier for people here to catch up.

[eric-wieser]

Arguably this should be

Suggested change

	theorem isDigit_digitChar_iff_lt : n.digitChar.isDigit ↔ (n < 10) :=
	@[simp]
	theorem isDigit_digitChar : n.digitChar.isDigit = n.blt 10 :=

[Rob23oba]

Nat.blt though..? I'd rather do decide (n < 10) in that case

[eric-wieser]

I don't mind much about the RHS, I just assumed that blt was simp-normal

[Rob23oba]

Nat.blt is only used in the construction of DecidableLT Nat (and in some other places where fast kernel reduction matters)

[eric-wieser]

I'm surprised that there's not a simp lemma in either direction

[ghost]

Mathlib CI status (docs):

• ✅ Mathlib branch batteries-pr-testing-1267 has successfully built against this PR. (2025-06-08 01:09:52) View Log
• ✅ Mathlib branch batteries-pr-testing-1267 has successfully built against this PR. (2025-06-08 15:22:59) View Log
• ✅ Mathlib branch batteries-pr-testing-1267 has successfully built against this PR. (2025-06-08 17:52:29) View Log
• ✅ Mathlib branch batteries-pr-testing-1267 has successfully built against this PR. (2025-06-09 00:50:39) View Log
• ✅ Mathlib branch batteries-pr-testing-1267 has successfully built against this PR. (2025-06-09 17:34:43) View Log
• ✅ Mathlib branch batteries-pr-testing-1267 has successfully built against this PR. (2025-06-09 21:56:29) View Log

[marcusrossel]

I've added the lemma toDigits_of_lt_base, and generalized the title of this PR accordingly.

[marcusrossel]

I've added the lemma toDigits_append_toDigits.

[Rob23oba]

I think there should be some general characterisation lemmas to avoid using Nat.toDigitsCore, e.g.:

theorem toDigits_base_zero (n : Nat) : toDigits 0 n = [n.digitChar]
theorem toDigits_base_one (n : Nat) : toDigits 1 n = List.replicate (n + 1) '0'
theorem toDigits_zero (b : Nat) : toDigits b 0 = ['0']
theorem toDigits_of_lt_base (h : n < b) : toDigits b n = [n.digitChar]
theorem toDigits_of_base_le (h : 1 < b) (h' : b ≤ n) : toDigits b n = toDigits b (n / b) ++ [(n % b).digitChar]

Then some of the others might be able to be proven with these instead of toDigitCore.

[marcusrossel]

@Rob23oba Is it desirable to have characterisation lemmas for bases 0 and 1? I feel like this almost encourages relying on these "garbage values".

[Rob23oba]

You're right; but at the same time, we characterize garbage values for division etc. I agree that this is a bit different though, so let's maybe wait with those two until there is consensus on leanprover/lean4#8686.

[fgdorais]

I'm on the fence about this PR. Several lemmas belong in Char and not Nat, but the main issue is that the functions involved are right on the edge with "implementation details".

I do think it's important to have theorems to prove facts about these. I would recommend a different approach:

1. Add a function that calculates the representation in an arbitrary base b ≥ 2 of a Nat (as a List (Fin b) or an Array (Fin b) or both, whichever is most convenient).
2. Add theorems that prove the basic arithmetic properties of the base b representation for the function from item 1.
3. Prove the correctness of core's implementation by proving that it is a map of the function from item 1 for relevant bases.

I don't think string representation is too relevant. For example, Batteries will eventually need to support Base-64 encoding, which is incompatible with traditional representation in bases 2, 8, 10, 16.

[eric-wieser]

1. Add a function that calculates the representation in an arbitrary base b ≥ 2 of a Nat (as a List (Fin b) or an Array (Fin b) or both, whichever is most convenient).

Isn't this basically the Nat.digits function that's already in mathlib?

[fgdorais]

Perhaps. If so, that should make it easier to adapt this PR!

[eric-wieser]

I'm not sure I understand the proposal; surely we don't want a third version of this function?

Is the suggestion to upstream Nat.digits? If so, it probably would save a lot of review time to just copy the file exactly from mathlib, and then make a subsequence cleanup if necessary.

[fgdorais]

I checked out Nat.digits in Mathlib. It is not suitable for Batteries but what is needed would be a more efficient drop-in replacement for Nat.digitsAux. I'm happy to do that in the next couple of weeks.

@marcusrossel How urgent is your need for this PR?

[marcusrossel]

@fgdorais not urgent at all :)
I'd also be happy to help with the version you have in mind.

[fgdorais]

WIP PR #1293 adds the functions I'm thinking about. The toDigitsBE function is the main one needed here. However, I haven't finished proving its correctness. toDigitsLE .. |>.reverse can be used in the mean time but that function is not as efficient as toDigitsBE.

@marcusrossel If you are still inclined to help, you can start reviewing this PR when you have time. The parts leading up to toDigitsBE are unlikely to change in non-trivial ways before final version.

[marcusrossel]

I'll be rather busy the next 2 weeks, but if it's not too late by then, I'll take a look :)

[marcusrossel]

Uh, @fgdorais was this merge intentional?

[fgdorais]

Yes! We can improve this later and it doesn't hurt to have it now.