From e758c0e35ca3c9f902cd973d1a435ccb4fab76e4 Mon Sep 17 00:00:00 2001 From: Markus Himmel <2065352+TwoFX@users.noreply.github.com> Date: Thu, 19 Mar 2026 12:02:56 +0100 Subject: [PATCH] feat: `String.toNat?` lemmas (#12828) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR redefines the `String.isNat` function to use less state and perform short-circuiting. It then verifies the `String.isNat` and `String.toNat?` functions. Recall that `isNat` and `toNat?` allow `_` as a digit separator. This is why we get the complicated statement ```lean public theorem isNat_iff {s : String} : s.isNat = true ↔ s ≠ "" ∧ (∀ c ∈ s.toList, c.isDigit ∨ c = '_') ∧ ¬ ['_', '_'] <:+: s.toList ∧ s.toList.head? ≠ some '_' ∧ s.toList.getLast? ≠ some '_' ``` For `toNat?`, we prove the fully general ```lean public theorem toNat?_eq_some_ofDigitChars {s : String} (h : s.isNat = true) : s.toNat? = some (Nat.ofDigitChars 10 (s.toList.filter (· != '_')) 0) ``` as well as the useful `(Nat.repr n).toNat? = some n` (and the corollary that `Nat.repr` is injective). For people implementing formatting routines that involve digit separators, we have ```lean public theorem isNat_of_isDigit {s : String} (hne : s ≠ "") (hdigit : ∀ c ∈ s.toList, c.isDigit) : s.isNat = true public theorem isNat_append_underscore_append {s t : String} (hs : s.isNat = true) (ht : t.isNat = true) : (s ++ "_" ++ t).isNat = true public theorem toNat?_append_underscore_append_eq_some {s t : String} {n m : Nat} (hs : s.toNat? = some n) (ht : t.toNat? = some m) : (s ++ "_" ++ t).toNat? = some (10 ^ (t.toList.filter (· != '_')).length * n + m) ``` The missing bit here is `(s.leftpad k '0').toNat? = s.toNat?`, which is missing because we don't have `String.leftpad` (yet). For any reasonable definition of `leftpad`, this will follow from `toNat?_eq_some_ofDigitChars` since we prove the necessary ingredients about `ofDigitChars`. There are some rough edges around `ofDigitChars`, and in the future it will be nice to connect this all to mathlib's `Nat.digits` and `Nat.ofDigits`, which are similar but different. --- src/Init/Data/Nat/ToString.lean | 72 ++++++ src/Init/Data/String/Iterate.lean | 28 +++ src/Init/Data/String/Lemmas/Iterate.lean | 21 ++ src/Init/Data/String/Search.lean | 29 --- src/Init/Data/String/Slice.lean | 29 ++- src/Std/Data.lean | 1 + src/Std/Data/String.lean | 9 + src/Std/Data/String/ToNat.lean | 301 +++++++++++++++++++++++ 8 files changed, 446 insertions(+), 44 deletions(-) create mode 100644 src/Std/Data/String.lean create mode 100644 src/Std/Data/String/ToNat.lean diff --git a/src/Init/Data/Nat/ToString.lean b/src/Init/Data/Nat/ToString.lean index 4390acc5b4..73ed2053bc 100644 --- a/src/Init/Data/Nat/ToString.lean +++ b/src/Init/Data/Nat/ToString.lean @@ -19,6 +19,7 @@ import Init.Data.Nat.Bitwise import Init.Data.Nat.Simproc import Init.WFTactics import Init.Data.Char.Lemmas +import Init.Data.Nat.Div.Lemmas public section @@ -118,6 +119,11 @@ private theorem isDigit_of_mem_toDigitsCore theorem isDigit_of_mem_toDigits (hb₁ : 0 < b) (hb₂ : b ≤ 10) (hc : c ∈ toDigits b n) : c.isDigit := isDigit_of_mem_toDigitsCore (fun _ => by contradiction) hb₁ hb₂ hc +@[simp] +theorem underscore_not_in_toDigits {n : Nat} : ¬'_' ∈ Nat.toDigits 10 n := by + intro h + simpa using isDigit_of_mem_toDigits (by decide) (by decide) h + private theorem toDigitsCore_of_lt_base (hb : n < b) (hf : n < fuel) : toDigitsCore b fuel n cs = n.digitChar :: cs := by unfold toDigitsCore @@ -194,6 +200,11 @@ theorem length_toDigits_pos {b n : Nat} : · rw [toDigitsCore_eq_toDigitsCore_nil_append] simp +@[simp] +theorem toDigits_ne_nil {n b : Nat} : Nat.toDigits b n ≠ [] := by + rw [← List.length_pos_iff] + exact Nat.length_toDigits_pos + theorem length_toDigits_le_iff {n k : Nat} (hb : 1 < b) (h : 0 < k) : (Nat.toDigits b n).length ≤ k ↔ n < b ^ k := by match k with @@ -219,6 +230,14 @@ theorem repr_eq_ofList_toDigits {n : Nat} : n.repr = .ofList (toDigits 10 n) := (rfl) +@[simp] +theorem toList_repr {n : Nat} : n.repr.toList = Nat.toDigits 10 n := by + simp [repr_eq_ofList_toDigits] + +@[simp] +theorem repr_ne_empty {n : Nat} : n.repr ≠ "" := by + simp [← String.toList_inj] + theorem toString_eq_ofList_toDigits {n : Nat} : toString n = .ofList (toDigits 10 n) := (rfl) @@ -259,4 +278,57 @@ theorem length_repr_le_iff {n k : Nat} (h : 0 < k) : n.repr.length ≤ k ↔ n < 10 ^ k := by simpa [repr_eq_ofList_toDigits] using length_toDigits_le_iff (by omega) h +/-- +Transforms a list of characters into a natural number, *assuming that all characters are in the +range from `'0'` to `'9'`*. +-/ +def ofDigitChars (b : Nat) (l : List Char) (init : Nat) : Nat := + l.foldl (init := init) (fun sofar c => b * sofar + (c.toNat - '0'.toNat)) + +theorem ofDigitChars_eq_foldl {b : Nat} {l : List Char} {init : Nat} : + ofDigitChars b l init = l.foldl (init := init) (fun sofar c => b * sofar + (c.toNat - '0'.toNat)) := + (rfl) + +@[simp] +theorem ofDigitChars_nil {init : Nat} : ofDigitChars b [] init = init := by + simp [ofDigitChars] + +theorem ofDigitChars_cons {c : Char} {cs : List Char} {init : Nat} : + ofDigitChars b (c::cs) init = ofDigitChars b cs (b * init + (c.toNat - '0'.toNat)) := by + simp [ofDigitChars] + +theorem ofDigitChars_cons_digitChar_of_lt_ten {n : Nat} (hn : n < 10) {cs : List Char} {init : Nat} : + ofDigitChars 10 (n.digitChar :: cs) init = ofDigitChars 10 cs (10 * init + n) := by + simp [ofDigitChars_cons, Nat.toNat_digitChar_sub_48_of_lt_ten hn] + +theorem ofDigitChars_eq_ofDigitChars_zero {l : List Char} {init : Nat} : + ofDigitChars 10 l init = 10 ^ l.length * init + ofDigitChars 10 l 0 := by + induction l generalizing init with + | nil => simp [ofDigitChars] + | cons hd tl ih => + simp only [ofDigitChars, ↓Char.isValue, Char.reduceToNat, List.foldl_cons, List.length_cons, + Nat.mul_zero, Nat.zero_add] at ⊢ ih + rw [ih, ih (init := hd.toNat - 48), Nat.pow_succ, Nat.mul_add, Nat.mul_assoc, Nat.add_assoc] + +theorem ofDigitChars_append {l m : List Char} (init : Nat) : + ofDigitChars b (l ++ m) init = ofDigitChars b m (ofDigitChars b l init) := by + simp [ofDigitChars] + +@[simp] +theorem ofDigitChars_replicate_zero {n : Nat} : ofDigitChars b (List.replicate n '0') init = b ^ n * init := by + induction n generalizing init with + | zero => simp + | succ n ih => simp [List.replicate_succ, ofDigitChars_cons, ih, Nat.pow_succ, Nat.mul_assoc] + +@[simp] +theorem ofDigitChars_toDigits {n : Nat} : ofDigitChars 10 (toDigits 10 n) 0 = n := by + have : 1 < 10 := by decide + induction n using base_induction 10 this with + | single m hm => + simp [Nat.toDigits_of_lt_base hm, ofDigitChars_cons_digitChar_of_lt_ten hm] + | digit m k hk hm ih => + rw [← Nat.toDigits_append_toDigits this hm hk, + ofDigitChars_append, ih, Nat.toDigits_of_lt_base hk, + ofDigitChars_cons_digitChar_of_lt_ten hk, ofDigitChars_nil] + end Nat diff --git a/src/Init/Data/String/Iterate.lean b/src/Init/Data/String/Iterate.lean index f7407aec26..27157f8e03 100644 --- a/src/Init/Data/String/Iterate.lean +++ b/src/Init/Data/String/Iterate.lean @@ -462,4 +462,32 @@ def revBytes (s : String) := instance {m : Type u → Type v} [Monad m] : ForIn m String Char where forIn s b f := ForIn.forIn s.toSlice b f +/-- +Folds a function over a string from the start, accumulating a value starting with {name}`init`. The +accumulated value is combined with each character in order, using {name}`f`. + +Examples: + * {lean}`"coffee tea water".foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 2` + * {lean}`"coffee tea and water".foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 3` + * {lean}`"coffee tea water".foldl (·.push ·) "" = "coffee tea water"` +-/ +@[inline] def foldl {α : Type u} (f : α → Char → α) (init : α) (s : String) : α := + s.toSlice.foldl f init + +@[export lean_string_foldl] +def Internal.foldlImpl (f : String → Char → String) (init : String) (s : String) : String := + String.foldl f init s + +/-- +Folds a function over a string from the right, accumulating a value starting with {lean}`init`. The +accumulated value is combined with each character in reverse order, using {lean}`f`. + +Examples: + * {lean}`"coffee tea water".foldr (fun c n => if c.isWhitespace then n + 1 else n) 0 = 2` + * {lean}`"coffee tea and water".foldr (fun c n => if c.isWhitespace then n + 1 else n) 0 = 3` + * {lean}`"coffee tea water".foldr (fun c s => s.push c) "" = "retaw aet eeffoc"` +-/ +@[inline] def foldr {α : Type u} (f : Char → α → α) (init : α) (s : String) : α := + s.toSlice.foldr f init + end String diff --git a/src/Init/Data/String/Lemmas/Iterate.lean b/src/Init/Data/String/Lemmas/Iterate.lean index 578e2ad156..51fca51f4b 100644 --- a/src/Init/Data/String/Lemmas/Iterate.lean +++ b/src/Init/Data/String/Lemmas/Iterate.lean @@ -190,6 +190,17 @@ theorem forIn_eq_forIn_toList {m : Type u → Type v} [Monad m] [LawfulMonad m] ForIn.forIn s b f = ForIn.forIn s.copy.toList b f := by rw [forIn_eq_forIn_chars, ← Std.Iter.forIn_toList, toList_chars] +@[simp] +theorem foldl_eq_foldl_toList {α : Type u} {f : α → Char → α} {init : α} {s : Slice} : + s.foldl f init = s.copy.toList.foldl f init := by + rw [foldl, ← Std.Iter.foldl_toList, toList_chars] + +@[simp] +theorem foldr_eq_foldr_toList {α : Type u} {f : Char → α → α} {init : α} {s : Slice} : + s.foldr f init = s.copy.toList.foldr f init := by + rw [foldr, ← Std.Iter.foldl_toList, toList_revChars, List.foldl_reverse] + congr + end Slice /-- @@ -355,4 +366,14 @@ theorem forIn_eq_forIn_toList {m : Type u → Type v} [Monad m] [LawfulMonad m] ForIn.forIn s b f = ForIn.forIn s.toList b f := by rw [forIn_eq_forIn_chars, ← Std.Iter.forIn_toList, toList_chars] +@[simp] +theorem foldl_eq_foldl_toList {α : Type u} {f : α → Char → α} {init : α} {s : String} : + s.foldl f init = s.toList.foldl f init := by + simp [foldl] + +@[simp] +theorem foldr_eq_foldr_toList {α : Type u} {f : Char → α → α} {init : α} {s : String} : + s.foldr f init = s.toList.foldr f init := by + simp [foldr] + end String diff --git a/src/Init/Data/String/Search.lean b/src/Init/Data/String/Search.lean index b7a4826846..64104ace18 100644 --- a/src/Init/Data/String/Search.lean +++ b/src/Init/Data/String/Search.lean @@ -278,43 +278,14 @@ def splitInclusive (s : String) (pat : ρ) [ToForwardSearcher pat σ] := def foldlAux {α : Type u} (f : α → Char → α) (s : String) (stopPos : Pos.Raw) (i : Pos.Raw) (a : α) : α := s.slice! (s.pos! i) (s.pos! stopPos) |>.foldl f a -/-- -Folds a function over a string from the start, accumulating a value starting with {name}`init`. The -accumulated value is combined with each character in order, using {name}`f`. - -Examples: - * {lean}`"coffee tea water".foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 2` - * {lean}`"coffee tea and water".foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 3` - * {lean}`"coffee tea water".foldl (·.push ·) "" = "coffee tea water"` --/ -@[inline] def foldl {α : Type u} (f : α → Char → α) (init : α) (s : String) : α := - s.toSlice.foldl f init - -@[export lean_string_foldl] -def Internal.foldlImpl (f : String → Char → String) (init : String) (s : String) : String := - String.foldl f init s - @[deprecated String.Slice.foldr (since := "2025-11-25")] def foldrAux {α : Type u} (f : Char → α → α) (a : α) (s : String) (i begPos : Pos.Raw) : α := s.slice! (s.pos! begPos) (s.pos! i) |>.foldr f a -/-- -Folds a function over a string from the right, accumulating a value starting with {lean}`init`. The -accumulated value is combined with each character in reverse order, using {lean}`f`. - -Examples: - * {lean}`"coffee tea water".foldr (fun c n => if c.isWhitespace then n + 1 else n) 0 = 2` - * {lean}`"coffee tea and water".foldr (fun c n => if c.isWhitespace then n + 1 else n) 0 = 3` - * {lean}`"coffee tea water".foldr (fun c s => s.push c) "" = "retaw aet eeffoc"` --/ -@[inline] def foldr {α : Type u} (f : Char → α → α) (init : α) (s : String) : α := - s.toSlice.foldr f init - @[deprecated String.Slice.any (since := "2025-11-25")] def anyAux (s : String) (stopPos : Pos.Raw) (p : Char → Bool) (i : Pos.Raw) : Bool := s.slice! (s.pos! i) (s.pos! stopPos) |>.any p - /-- Checks whether a string has a match of the pattern {name}`pat` anywhere. diff --git a/src/Init/Data/String/Slice.lean b/src/Init/Data/String/Slice.lean index fc50967b82..3170a59b57 100644 --- a/src/Init/Data/String/Slice.lean +++ b/src/Init/Data/String/Slice.lean @@ -906,21 +906,20 @@ Examples: * {lean}`"12__34".toSlice.isNat = false` -/ @[inline] -def isNat (s : Slice) : Bool := - if s.isEmpty then - false - else - -- Track: isFirst, lastWasUnderscore, lastCharWasDigit, valid - let result := s.foldl (fun (isFirst, lastWasUnderscore, _lastCharWasDigit, valid) c => - let isDigit := c.isDigit - let isUnderscore := c = '_' - let newValid := valid && (isDigit || isUnderscore) && - !(isFirst && isUnderscore) && -- Cannot start with underscore - !(lastWasUnderscore && isUnderscore) -- No consecutive underscores - (false, isUnderscore, isDigit, newValid)) - (true, false, false, true) - -- Must be valid and last character must have been a digit (not underscore) - result.2.2.2 && result.2.2.1 +def isNat (s : Slice) : Bool := Id.run do + let mut lastWasDigit := false + + for c in s do + if c = '_' then + if !lastWasDigit then + return false + lastWasDigit := false + else if c.isDigit then + lastWasDigit := true + else + return false + + return lastWasDigit /-- Interprets a slice as the decimal representation of a natural number, returning it. Returns diff --git a/src/Std/Data.lean b/src/Std/Data.lean index 47f60a9ff2..5bb3d05f3d 100644 --- a/src/Std/Data.lean +++ b/src/Std/Data.lean @@ -34,3 +34,4 @@ public import Std.Data.TreeSet.Raw public import Std.Data.Iterators public import Std.Data.ByteSlice +public import Std.Data.String diff --git a/src/Std/Data/String.lean b/src/Std/Data/String.lean new file mode 100644 index 0000000000..a2eba4e767 --- /dev/null +++ b/src/Std/Data/String.lean @@ -0,0 +1,9 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +module + +prelude +public import Std.Data.String.ToNat diff --git a/src/Std/Data/String/ToNat.lean b/src/Std/Data/String/ToNat.lean new file mode 100644 index 0000000000..9b112c7216 --- /dev/null +++ b/src/Std/Data/String/ToNat.lean @@ -0,0 +1,301 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +module + +prelude +public import Init.Data.String.Slice +public import Init.Data.String.Search +public import Init.Data.Nat.ToString +import all Init.Data.String.Slice +import all Init.Data.String.Search +import Init.Data.String.Lemmas.Iterate +import Std.Tactic.Do +import Init.Data.List.Sublist + +section NoRepetition + +structure NoRepetition {α : Type u} (a : α) (l : List α) : Prop where + not_isInfix : ¬ [a, a] <:+: l + +theorem noRepetition_iff {α : Type u} {a : α} {l : List α} : NoRepetition a l ↔ ¬ [a, a] <:+: l := + ⟨fun ⟨h⟩ => h, fun h => ⟨h⟩⟩ + +theorem NoRepetition.right_of_append {α : Type u} {a : α} {l m : List α} : + NoRepetition a (l ++ m) → NoRepetition a m := by + simpa [noRepetition_iff] using mt List.infix_append_of_infix_right + +theorem NoRepetition.left_of_append {α : Type u} {a : α} {l m : List α} : + NoRepetition a (l ++ m) → NoRepetition a l := by + simpa [noRepetition_iff] using mt List.infix_append_of_infix_left + +theorem not_noRepetition_append_of_right {α : Type u} {a : α} {l m : List α} : + ¬ NoRepetition a m → ¬ NoRepetition a (l ++ m) := + mt NoRepetition.right_of_append + +theorem not_noRepetition_append_of_left {α : Type u} {a : α} {l m : List α} : + ¬ NoRepetition a l → ¬ NoRepetition a (l ++ m) := + mt NoRepetition.left_of_append + +theorem not_noRepetition_append_singleton_of_suffix {α : Type u} {a : α} {l : List α} + (h : [a] <:+ l) : ¬ NoRepetition a (l ++ [a]) := by + simpa [noRepetition_iff] using (List.suffix_append_self_iff.2 h).isInfix + +theorem NoRepetition.not_isSuffix_of_append_singleton {α : Type u} {a : α} {l : List α} : + NoRepetition a (l ++ [a]) → ¬ [a] <:+ l := by + simpa using mt not_noRepetition_append_singleton_of_suffix + +theorem NoRepetition.append_singleton_of_not_suffix {α : Type u} {a : α} {l : List α} + (h : NoRepetition a l) (h' : ¬ [a] <:+ l) : NoRepetition a (l ++ [a]) := by + simp only [noRepetition_iff, List.infix_concat_iff, not_or] at ⊢ h + + exact ⟨by rwa [← List.singleton_append, List.suffix_append_self_iff], h⟩ + +theorem NoRepetition.append_singleton_of_ne {α : Type u} {a b : α} {l : List α} + (h : NoRepetition a l) (h' : a ≠ b) : NoRepetition a (l ++ [b]) := by + simp only [noRepetition_iff, List.infix_concat_iff, not_or] at ⊢ h + refine ⟨?_, h⟩ + rw [← List.singleton_append, List.suffix_append_inj_of_length_eq (by simp)] + simp [h'] + +@[simp] +theorem noRepetition_singleton {α : Type u} {a b : α} : NoRepetition a [b] := by + simpa [noRepetition_iff] using fun h => by simpa using h.length_le + +theorem noRepetition_cons_append_append_iff {α : Type u} {a : α} {l : List α} : + NoRepetition a (a :: (l ++ [a])) ↔ + l ≠ [] ∧ ¬ [a, a] <:+: l ∧ l.head? ≠ some a ∧ l.getLast? ≠ some a := by + simp only [noRepetition_iff, List.infix_cons_iff, List.cons_prefix_cons, true_and, + List.infix_concat_iff, not_or, ne_eq, ← List.singleton_prefix_iff_head?_eq_some, + ← List.singleton_suffix_iff_getLast?_eq_some] + conv => enter [1, 2]; rw [← List.singleton_append, List.suffix_append_self_iff] + refine ⟨fun ⟨h₁, h₂, h₃⟩ => ⟨?_, h₃, ?_, h₂⟩, fun ⟨h₁, h₂, h₃, h₄⟩ => ⟨?_, h₄, h₂⟩⟩ + · rintro rfl + simp_all + · exact fun h => h₁ (List.prefix_append_of_prefix h) + · cases l <;> simp_all + +theorem noRepetition_append_cons_of_noRepetition_append_singleton {α : Type u} {a : α} {l m : List α} + (h : NoRepetition a (l ++ [a])) (h' : NoRepetition a (a :: m)) : NoRepetition a (l ++ a :: m) := by + simp [noRepetition_iff] at h h' ⊢ + simp [List.infix_append_iff_ne_nil] + refine ⟨(h <| List.infix_append_of_infix_left ·), h', + fun l₁ hl₁ l₂ hl₂ h₁ h₂ h₃ => h (List.IsSuffix.isInfix ?_)⟩ + obtain ⟨rfl, rfl⟩ : l₁ = [a] ∧ l₂ = [a] := by + match l₁, hl₁, l₂, hl₂ with + | [b], _, [c], _ => + simp only [List.cons_append, List.nil_append, List.cons.injEq, and_true] at h₁ + obtain ⟨rfl, rfl⟩ := h₁ + simp + | b::b'::bs, _, c::cs, _ => simp at h₁ + rwa [← List.singleton_append, List.suffix_append_self_iff] + +end NoRepetition + +namespace String.Slice + +open Std.Do in +set_option mvcgen.warning false in +theorem isNat_iff' {s : String.Slice} : + s.isNat = true ↔ + s.copy.toList ≠ [] ∧ + (∀ c ∈ s.copy.toList, c.isDigit ∨ c = '_') ∧ + NoRepetition '_' ('_' :: s.copy.toList ++ ['_']) := by + generalize h : s.isNat = res + apply Id.of_wp_run_eq h + simp only [↓Char.isValue, Bool.not_eq_eq_eq_not, Bool.not_true, forIn_eq_forIn_toList, ne_eq, + WP.bind, SPred.entails_nil, SPred.down_pure, forall_const] + mvcgen invariants + | inv1 => Invariant.withEarlyReturnNewDo + (fun cursor lastWasDigit => ⌜lastWasDigit = ¬ (['_'] <:+ ('_' :: cursor.prefix)) ∧ + (∀ c ∈ cursor.prefix, c.isDigit ∨ c = '_') ∧ NoRepetition '_' ('_' :: cursor.prefix)⌝) + (fun res lastWasDigit => ⌜res = false ∧ + ((∃ c ∈ s.copy.toList, c.isDigit = false ∧ c ≠ '_') ∨ ¬ NoRepetition '_' ('_' :: s.copy.toList))⌝) + next pref c suff h b hc h₁ h₂ => + subst hc + simp only [h₁, ↓Char.isValue, eq_iff_iff, false_iff, Decidable.not_not, + reduceCtorEq, h, List.mem_append, List.mem_cons, ne_eq, false_and, and_false, exists_const, + or_false, Option.some.injEq, Bool.false_eq, true_and, and_self_left, exists_eq_left, + false_or] at ⊢ h₂ + rw [List.append_cons, ← List.cons_append, ← List.cons_append] + exact Or.inr (not_noRepetition_append_of_left (not_noRepetition_append_singleton_of_suffix h₂.2.1)) + next pref c suff h b hc h₁ h₂ => + subst hc + simp only [h₁, ↓Char.isValue, eq_iff_iff, true_iff, reduceCtorEq, h, List.mem_append, + List.mem_cons, ne_eq, false_and, and_false, exists_const, or_false, Bool.false_eq_true, + List.suffix_cons_append, not_true_eq_false, List.not_mem_nil, + forall_or_imp_or_self_right_right, true_and] at ⊢ h₂ + refine ⟨h₂.2.2.1, ?_⟩ + rw [← List.cons_append] + exact NoRepetition.append_singleton_of_not_suffix h₂.2.2.2 h₂.2.1 + next pref c suff h b hc hc' h₁ => + simp only [↓Char.isValue, eq_iff_iff, reduceCtorEq, h, List.mem_append, List.mem_cons, ne_eq, + false_and, and_false, exists_const, or_false, List.singleton_suffix_cons_append_singleton_iff, + Ne.symm hc, not_false_eq_true, List.not_mem_nil, forall_or_eq_imp, hc', true_or, and_true, + true_and] at ⊢ h₁ + refine ⟨h₁.2.2.1, ?_⟩ + rw [← List.cons_append] + exact NoRepetition.append_singleton_of_ne h₁.2.2.2 (Ne.symm hc) + next pref c suff h b hc hc' h₁ => simpa [h] using Or.inl ⟨c, by simp_all⟩ + next => simp + next r b h₁ h₂ => + simp only [h₁, reduceCtorEq, ↓Char.isValue, eq_iff_iff, false_and, Option.some.injEq, ne_eq, + true_and, exists_eq_left', false_or] at h₂ + simp only [h₂.1, Bool.false_eq_true, toList_eq_nil_iff, copy_eq_empty_iff, Bool.not_eq_true, + ↓Char.isValue, List.cons_append, false_iff, not_and] + intro hx hy + obtain (⟨c, hc₁, hc₂, hc₃⟩|hn) := h₂.2 + · have := hy c + simp_all + · rw [← List.cons_append] + exact not_noRepetition_append_of_left hn + next r h₁ h₂ => + generalize s.copy.toList = l at * + simp only [h₁, ↓Char.isValue, eq_iff_iff, true_and, reduceCtorEq, ne_eq, false_and, + exists_const, or_false, List.cons_append] at ⊢ h₂ + rw [h₂.1] + refine ⟨fun h => ⟨?_, h₂.2.1, ?_⟩, fun ⟨h₁, _, h₂⟩ => ?_⟩ + · rintro rfl + simp at h + · rw [← List.cons_append] + apply NoRepetition.append_singleton_of_not_suffix h₂.2.2 h + · rw [← List.cons_append] at h₂ + exact h₂.not_isSuffix_of_append_singleton + +public theorem isNat_iff {s : String.Slice} : + s.isNat = true ↔ + s.isEmpty = false ∧ + (∀ c ∈ s.copy.toList, c.isDigit ∨ c = '_') ∧ + ¬ ['_', '_'] <:+: s.copy.toList ∧ + s.copy.toList.head? ≠ some '_' ∧ + s.copy.toList.getLast? ≠ some '_' := by + simp +contextual [isNat_iff', noRepetition_cons_append_append_iff] + +public theorem isNat_of_isDigit {s : String.Slice} (hne : s.isEmpty = false) + (hdigit : ∀ c ∈ s.copy.toList, c.isDigit) : s.isNat = true := by + rw [isNat_iff] + refine ⟨hne, fun c hc => Or.inl (hdigit c hc), fun h => ?_, fun h => ?_, fun h => ?_⟩ + · have := hdigit _ (by simpa using h.subset) + simp at this + · have := hdigit _ (s.copy.toList.mem_of_head? h) + simp at this + · have := hdigit _ (s.copy.toList.mem_of_getLast? h) + simp at this + +@[simp] +public theorem isSome_toNat? {s : String.Slice} : s.toNat?.isSome = s.isNat := by + simp only [toNat?, ↓Char.isValue, Char.reduceToNat, foldl_eq_foldl_toList] + split <;> simp_all + +public theorem isNat_of_toNat?_eq_some {s : String.Slice} (h : s.toNat? = some n) : s.isNat = true := by + simp [← isSome_toNat?, h] + +@[simp] +public theorem toNat?_eq_none_iff {s : String.Slice} : s.toNat? = none ↔ s.isNat = false := by + simp [← Option.isNone_iff_eq_none, ← Option.not_isSome, isSome_toNat?] + +public theorem toNat?_eq_none {s : String.Slice} (h : s.isNat = false) : s.toNat? = none := + toNat?_eq_none_iff.2 h + +public theorem toNat?_eq_some_ofDigitChars {s : String.Slice} (h : s.isNat = true) : + s.toNat? = some (Nat.ofDigitChars 10 (s.copy.toList.filter (· != '_')) 0) := by + rw [toNat?, if_pos h, Option.some.injEq] + simp [Nat.ofDigitChars_eq_foldl, ↓Char.isValue, Char.reduceToNat, foldl_eq_foldl_toList, List.foldl_ite_right, + bne_eq, Bool.beq_eq_decide_eq, Nat.mul_comm 10] + +end String.Slice + +namespace String + +@[simp] +public theorem isNat_toSlice {s : String} : s.toSlice.isNat = s.isNat := + (rfl) + +@[simp] +public theorem toNat?_toSlice {s : String} : s.toSlice.toNat? = s.toNat? := + (rfl) + +public theorem isNat_iff {s : String} : + s.isNat = true ↔ + s ≠ "" ∧ + (∀ c ∈ s.toList, c.isDigit ∨ c = '_') ∧ + ¬ ['_', '_'] <:+: s.toList ∧ + s.toList.head? ≠ some '_' ∧ + s.toList.getLast? ≠ some '_' := by + simp [← isNat_toSlice, Slice.isNat_iff] + +public theorem isNat_of_isDigit {s : String} (hne : s ≠ "") + (hdigit : ∀ c ∈ s.toList, c.isDigit) : s.isNat = true := by + apply Slice.isNat_of_isDigit <;> simpa + +@[simp] +public theorem isSome_toNat? {s : String} : s.toNat?.isSome = s.isNat := by + simp [← isNat_toSlice, ← toNat?_toSlice] + +public theorem isNat_of_toNat?_eq_some {s : String} (h : s.toNat? = some n) : s.isNat = true := by + rw [← isNat_toSlice, Slice.isNat_of_toNat?_eq_some (by simpa)] + +@[simp] +public theorem toNat?_eq_none_iff {s : String} : s.toNat? = none ↔ s.isNat = false := by + simp [← isNat_toSlice, ← toNat?_toSlice] + +public theorem toNat?_eq_none {s : String} (h : s.isNat = false) : s.toNat? = none := + toNat?_eq_none_iff.2 h + +public theorem toNat?_eq_some_ofDigitChars {s : String} (h : s.isNat = true) : + s.toNat? = some (Nat.ofDigitChars 10 (s.toList.filter (· != '_')) 0) := by + rw [← toNat?_toSlice, Slice.toNat?_eq_some_ofDigitChars (by simpa), copy_toSlice] + +public theorem isNat_append_underscore_append {s t : String} + (hs : s.isNat = true) (ht : t.isNat = true) : + (s ++ "_" ++ t).isNat = true := by + rw [← isNat_toSlice, Slice.isNat_iff'] at hs ht ⊢ + simp only [copy_toSlice, ne_eq, toList_eq_nil_iff, ↓Char.isValue, List.cons_append, toList_append, + String.reduceToList, List.append_assoc, List.nil_append, List.append_eq_nil_iff, reduceCtorEq, + and_false, not_false_eq_true, List.mem_append, List.mem_cons, or_imp, imp_or_right_iff_true, + true_and, forall_and] at hs ht ⊢ + refine ⟨⟨hs.2.1, ht.2.1⟩, ?_⟩ + have : '_' :: (s.toList ++ '_' :: (t.toList ++ ['_'])) = + ('_' :: s.toList) ++ '_' :: (t.toList ++ ['_']) := by simp + exact this ▸ noRepetition_append_cons_of_noRepetition_append_singleton hs.2.2 ht.2.2 + +public theorem toNat?_append_underscore_append_eq_some {s t : String} {n m : Nat} + (hs : s.toNat? = some n) (ht : t.toNat? = some m) : + (s ++ "_" ++ t).toNat? = + some (10 ^ (t.toList.filter (· != '_')).length * n + m) := by + rw [toNat?_eq_some_ofDigitChars (isNat_append_underscore_append + (isNat_of_toNat?_eq_some hs) (isNat_of_toNat?_eq_some ht))] + simp only [toNat?_eq_some_ofDigitChars (isNat_of_toNat?_eq_some hs), + toNat?_eq_some_ofDigitChars (isNat_of_toNat?_eq_some ht), ↓Char.isValue, + Option.some.injEq] at hs ht + simp only [↓Char.isValue, toList_append, String.reduceToList, List.append_assoc, List.cons_append, + List.nil_append, List.filter_append, bne_self_eq_false, Bool.false_eq_true, not_false_eq_true, + List.filter_cons_of_neg, Nat.ofDigitChars_append, hs, Option.some.injEq] + rw [Nat.ofDigitChars_eq_ofDigitChars_zero, ht] + +end String + +namespace Nat + +@[simp] +public theorem isNat_repr (n : Nat) : (Nat.repr n).isNat = true := by + apply String.isNat_of_isDigit (by simp) + simpa using fun c hc => isDigit_of_mem_toDigits (by omega) (by omega) hc + +@[simp] +public theorem toNat?_repr (n : Nat) : (Nat.repr n).toNat? = some n := by + simp only [String.toNat?_eq_some_ofDigitChars (isNat_repr _), ↓Char.isValue, toList_repr, + Option.some.injEq] + rw [List.filter_bne_eq_self_of_not_mem (by simp)] + simp + +public theorem repr_injective {m n : Nat} (h : Nat.repr m = Nat.repr n) : m = n := by + rw [← Option.some.injEq, ← toNat?_repr n, ← toNat?_repr m, h] + +@[simp] +public theorem repr_inj {m n : Nat} : Nat.repr m = Nat.repr n ↔ m = n := + ⟨repr_injective, (· ▸ rfl)⟩ + +end Nat