feat: termination arguments for String.ValidPos and String.Slice.Pos

[TwoFX]

This PR adds the basic infrastructure to perform termination proofs about String.ValidPos and String.Slice.Pos.

We choose approach where the intended way to do termination arguments is to argue about the position itself rather than some projection of it like remainingBytes.

The types String.ValidPos and String.Slice.Pos are equipped with a WellFoundedRelation instance given by the greater-than relation. This means that if a function takes a position p and performs a recursive call on q, then the decreasing obligation will be p < q. This works well in the common case where q is p.next h, in which case the goal p < p.next h is solved by the simplifier.

For stepping through a string backwards, we introduce a type synonym with a WellFoundedRelation instance given by the less-than relation. This means that if a function takes a position p and performs a recursive call on q and specifies termination_by p.down, then the decreasing obligation will be q < p. This works well in the case where q is p.prev h, in which case the goal p.prev h < p is solved by the simplifier.

For termination arguments invoving multiple strings, the lower-level primitive p.remainingBytes (landing in Nat) is also available.

In a future PR, we will additionally provide the necessary typeclasses instances to register String.ValidPos and String.Slice.Pos with grind to make complex termination arguments more convenient in user code.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 59573646c227d940962c08a1e77ce51177a024ea --onto efbbb0b230ce95653d25b59c83fd24a51a8bf363. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-23 16:45:01)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-10-25 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-25 14:24:45)
• 💥 Mathlib branch lean-pr-testing-10933 build failed against this PR. (2025-10-26 17:40:37) View Log
• ✅ Mathlib branch lean-pr-testing-10933 has successfully built against this PR. (2025-10-27 09:31:40) View Log

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 59573646c227d940962c08a1e77ce51177a024ea --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-23 16:45:03)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-25 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-10-25 14:24:46)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-26 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-10-26 16:42:35)