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

Co-authored-by: François G. Dorais <[email protected]>

Author: ammkrn

Batteries/Data/String.lean

@@ -1,3 +1,4 @@
+import Batteries.Data.String.AsciiCasing
 import Batteries.Data.String.Basic
 import Batteries.Data.String.Lemmas
 import Batteries.Data.String.Matcher

Batteries/Data/String/AsciiCasing.lean

@@ -0,0 +1,82 @@
+/-
+Copyright (c) 2025 Christopher Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christopher Bailey, F. G. Dorais
+-/
+import Batteries.Data.Char
+import Batteries.Data.Char.AsciiCasing
+
+namespace String
+
+/-- Case folding for ASCII characters only.
+
+Alphabetic ASCII characters are mapped to their lowercase form, all other characters are left
+unchanged. This agrees with the Unicode case folding algorithm for ASCII characters.
+
+```
+#eval "ABC".caseFoldAsciiOnly == "abc" -- true
+#eval "x".caseFoldAsciiOnly == "y" -- false
+#eval "Àà".caseFoldAsciiOnly == "Àà" -- true
+#eval "1$#!".caseFoldAsciiOnly == "1$#!" -- true
+```
+-/
+abbrev caseFoldAsciiOnly (s : String) := s.map Char.caseFoldAsciiOnly
+
+-- TODO: Reimplement with finite iterators/streams when available for `String`.
+private partial def beqCaseInsensitiveAsciiOnlyImpl (s₁ s₂ : String) : Bool :=
+  s₁.length == s₂.length && loop (ToStream.toStream s₁) (ToStream.toStream s₂)
+where
+  loop i₁ i₂ := match Stream.next? i₁, Stream.next? i₂ with
+    | some (c₁, i₁), some (c₂, i₂) => c₁.beqCaseInsensitiveAsciiOnly c₂ && loop i₁ i₂
+    | none, none => true
+    | _, _ => false
+
+/--
+Bool-valued comparison of two `String`s for *ASCII*-case insensitive equality.
+
+#eval "abc".beqCaseInsensitiveAsciiOnly "ABC" -- true
+#eval "cba".beqCaseInsensitiveAsciiOnly "ABC" -- false
+#eval "$".beqCaseInsensitiveAsciiOnly "$" -- true
+#eval "a".beqCaseInsensitiveAsciiOnly "b" -- false
+#eval "γ".beqCaseInsensitiveAsciiOnly "Γ" -- false
+-/
+@[implemented_by beqCaseInsensitiveAsciiOnlyImpl]
+def beqCaseInsensitiveAsciiOnly (s₁ s₂ : String) : Bool :=
+  s₁.caseFoldAsciiOnly == s₂.caseFoldAsciiOnly
+
+theorem beqCaseInsensitiveAsciiOnly.eqv : Equivalence (beqCaseInsensitiveAsciiOnly · ·) := {
+  refl _ := BEq.rfl
+  trans _ _ := by simp_all [beqCaseInsensitiveAsciiOnly]
+  symm := by simp_all [beqCaseInsensitiveAsciiOnly]
+}
+
+/--
+Setoid structure on `String` usig `beqCaseInsensitiveAsciiOnly`
+-/
+def beqCaseInsensitiveAsciiOnly.isSetoid : Setoid String :=
+  ⟨(beqCaseInsensitiveAsciiOnly · ·), beqCaseInsensitiveAsciiOnly.eqv⟩
+
+-- TODO: Reimplement with finite iterators/streams when available for `String`.
+private partial def cmpCaseInsensitiveAsciiOnlyImpl (s₁ s₂ : String) : Ordering :=
+  loop (ToStream.toStream s₁) (ToStream.toStream s₂)
+where
+  loop i₁ i₂ := match Stream.next? i₁, Stream.next? i₂ with
+    | some (c₁, i₁), some (c₂, i₂) => c₁.cmpCaseInsensitiveAsciiOnly c₂ |>.then (loop i₁ i₂)
+    | some _, none => .gt
+    | none, some _ => .lt
+    | none, none => .eq
+
+/--
+ASCII-case insensitive implementation comparison returning an `Ordering`. Useful for sorting.
+
+```
+#eval cmpCaseInsensitiveAsciiOnly "a" "A" -- eq
+#eval cmpCaseInsensitiveAsciiOnly "a" "a" -- eq
+#eval cmpCaseInsensitiveAsciiOnly "$" "$" -- eq
+#eval cmpCaseInsensitiveAsciiOnly "a" "b" -- lt
+#eval cmpCaseInsensitiveAsciiOnly "γ" "Γ" -- gt
+```
+-/
+@[implemented_by cmpCaseInsensitiveAsciiOnlyImpl]
+def cmpCaseInsensitiveAsciiOnly (s₁ s₂ : String) : Ordering :=
+  compare s₁.caseFoldAsciiOnly s₂.caseFoldAsciiOnly

Batteries/Data/String/Lemmas.lean

@@ -728,6 +728,26 @@ theorem takeWhileAux_of_valid (p : Char → Bool) : ∀ l m r,
     cases p c <;> simp
     simpa [← Nat.add_assoc, Nat.add_right_comm] using takeWhileAux_of_valid p (l++[c]) m r
 
+@[simp]
+theorem data_eq_nil_iff (s : String) : s.data = [] ↔ s = "" :=
+  ⟨fun h => ext (id h), congrArg data⟩
+
+@[simp]
+theorem map_eq_empty_iff (s : String) (f : Char → Char) : (s.map f) = "" ↔ s = "" := by
+  simp only [map_eq, ← data_eq_nil_iff, List.map_eq_nil_iff]
+
+@[simp]
+theorem map_isEmpty_eq_isEmpty (s : String) (f : Char → Char) : (s.map f).isEmpty = s.isEmpty := by
+  rw [Bool.eq_iff_iff]; simp [isEmpty_iff, map_eq_empty_iff]
+
+@[simp]
+theorem length_map (s : String) (f : Char → Char) : (s.map f).length = s.length := by
+  simp only [length, map_eq, List.length_map]
+
+theorem length_eq_of_map_eq {a b : String} {f g : Char → Char} :
+  a.map f = b.map g → a.length = b.length := by
+  intro h; rw [← length_map a f, ← length_map b g, h]
+
 end String
 
 open String

BatteriesTest/String.lean

@@ -0,0 +1,44 @@
+import Batteries.Data.String.AsciiCasing
+
+#guard "ABC".caseFoldAsciiOnly == "abc"
+#guard "x".caseFoldAsciiOnly != "y"
+#guard "Àà".caseFoldAsciiOnly == "Àà"
+#guard "1$#!".caseFoldAsciiOnly == "1$#!"
+
+#guard "abc".beqCaseInsensitiveAsciiOnly "ABC" == true
+#guard "cba".beqCaseInsensitiveAsciiOnly "ABC" == false
+#guard "a".beqCaseInsensitiveAsciiOnly "a" == true
+#guard "$".beqCaseInsensitiveAsciiOnly "$" == true
+#guard "a".beqCaseInsensitiveAsciiOnly "b" == false
+#guard "γ".beqCaseInsensitiveAsciiOnly "Γ" == false
+#guard "ä".beqCaseInsensitiveAsciiOnly "Ä" == false
+
+#guard  "abc".cmpCaseInsensitiveAsciiOnly "ABC" == .eq
+#guard  "abc".cmpCaseInsensitiveAsciiOnly "xyz" == .lt
+#guard  "a".cmpCaseInsensitiveAsciiOnly "a" == .eq
+#guard  "$".cmpCaseInsensitiveAsciiOnly "$" == .eq
+#guard  "a__".cmpCaseInsensitiveAsciiOnly "b__" == .lt
+#guard  "γ".cmpCaseInsensitiveAsciiOnly "Γ" == .gt
+#guard  "ä".cmpCaseInsensitiveAsciiOnly "Ä" == .gt
+
+#guard [
+  ("", ""),
+  ("  ", "  "),
+  ("a", "A"),
+  ("abc", "ABC"),
+  ("aBc", "AbC"),
+  ("123", "123"),
+  ("国际化与本地化", "国际化与本地化"),
+  ("ABC😂🔰🍑xyz", "abc😂🔰🍑XYZ")
+].all (fun (a, b) => a.beqCaseInsensitiveAsciiOnly b && a.cmpCaseInsensitiveAsciiOnly b = .eq)
+
+#guard [
+  ("国际化", "国际化与本地化"),
+  ("", " "),
+  ("a", "b"),
+  ("ab", "ba"),
+  ("123", "124"),
+  ("😂", "🍑"),
+  ("🔰🍑", "😂🔰🍑aaa")
+] |>.all fun (a, b) =>
+  a ≠ b && !(a.beqCaseInsensitiveAsciiOnly b) && a.cmpCaseInsensitiveAsciiOnly b != .eq