max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: String.toNat? lemmas (#12828)

Browse source 
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.
This commit is contained in:
Markus Himmel 2026-03-19 12:02:56 +01:00 • committed by GitHub
parent 747262e498
commit e758c0e35c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
8 changed files with 446 additions and 44 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

72
src/Init/Data/Nat/ToString.lean
View file

@ -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

28
src/Init/Data/String/Iterate.lean
View file

@ -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

21
src/Init/Data/String/Lemmas/Iterate.lean
View file

@ -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

29
src/Init/Data/String/Search.lean
View file

@ -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.

29
src/Init/Data/String/Slice.lean
View file

@ -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

1
src/Std/Data.lean
View file

@ -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

9
src/Std/Data/String.lean Normal file
View file

@ -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

301
src/Std/Data/String/ToNat.lean Normal file
View file

@ -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