feat: add case insensitive comparison for strings (ASCII only)

[ammkrn]

Adds ASCII-only case insensitive comparison to Char and String.

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch batteries-pr-testing-1283 build failed against this PR. (2025-06-18 13:41:30) View Log
• 💥 Mathlib branch batteries-pr-testing-1283 build failed against this PR. (2025-06-21 15:50:34) View Log

[fgdorais]

I will review this in a couple of days. Regarding names, I think the core style would prefer ASCII over Ascii (though counterexamples exist, e.g Json vs JSON).

PS: If you need Unicode locale-independent case folding then please add a feature request to UnicodeBasic. I'm planning to add a few more normalization features this summer and this is an easy addition to the pile.

[fgdorais]

There's a lot here! A lot of which is great!

Let's split it though. Can you make a separate PR for the Char stuff only and make this PR depend on the new one?

Let me know if you need instructions or other assistance doing that.

[ammkrn]

There's a lot here! A lot of which is great!

Let's split it though. Can you make a separate PR for the Char stuff only and make this PR depend on the new one?

I believe I was able to do this, let me know if I did something different.

Regarding names, I think the core style would prefer ASCII over Ascii (though counterexamples exist, e.g Json vs JSON).

I'll make the appropriate changes if the verdict is that ASCII is preferable.

[fgdorais]

Now that #1312 is merged, we can start working on this. This one will be much easier since we already figured out a lot in #1312. Thank you for your patience and responsiveness with the review process. I look forward to completing this PR when you're ready.

[ammkrn]

I tried to match the Char setup in a way that made sense.

[ammkrn]

I implemented the requested changes with one modification: String.Iterator does not seem to have an instance of Stream (I was getting a 'failed to synthesize...' error). There's one for Substring which is accessible via ToStream.toStream, so I used that.

[fgdorais]

Looks good!

After much consideration, the quotient type CaseInsensitiveAsciiOnly is not a good fit for Batteries. There are two primary reasons:

1. It has very limited functionality and adding more functions is tricky since it requires lifting.
2. It is not very efficient since most functions end up applying caseFoldAsciiOnly and then another string function.

In fact, I would recommend using the subtype { s : String // s = s.caseFoldAsciiOnly } instead of the quotient type.

Please delete the CaseInsensitiveAsciiOnly file and we will be ready to merge.

[fgdorais]

@ammkrn Have you tried the subtype approach I suggested? I'm curious to hear whether that works for your project.

[ammkrn]

@ammkrn Have you tried the subtype approach I suggested? I'm curious to hear whether that works for your project.

I have not, but I have removed the requested files and squashed the commits.

[fgdorais]

I fixed a tiny thing: = is better than iff for Bool expressions.

Our Mathlib check is unreliable right now. I will have to do a manual check just to be sure. I'm juggling several pots, pans and plates right now, so please ping me again if that check takes more than a couple of weeks.

Thanks for your patience!

[fgdorais]

Local Mathlib tests have passed. Since it's unlikely that this PR would break Mathlib, this is strong enough evidence that the alleged failure is a malfunction of our CI. I am proceeding with the merge.