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

fix: export String.find? and String.contains lemmas (#12807)

Browse source 
This PR makes the lemmas about `String.find?` and `String.contains` that
were added recently into public declarations.
This commit is contained in:
Markus Himmel 2026-03-05 11:00:17 +01:00 • committed by GitHub
parent 8d42ad4796
commit fe1ad52f88
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 14 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Init/Data/String/Lemmas/Pattern/Find/Char.lean
View file

@ -7,6 +7,8 @@ module
prelude
public import Init.Data.String.Slice
public import Init.Data.String.Search
public import Init.Data.String.Lemmas.Splits
import Init.Data.String.Lemmas.Pattern.Find.Basic
import Init.Data.String.Lemmas.Pattern.Char
import Init.Data.String.Lemmas.Basic
@ -17,6 +19,8 @@ import Init.Grind
import Init.Data.Option.Lemmas
import Init.Data.String.OrderInstances
public section
namespace String.Slice
theorem find?_char_eq_some_iff {c : Char} {s : Slice} {pos : s.Pos} :
@ -98,7 +102,7 @@ end Slice
theorem Pos.find?_char_eq_some_iff {c : Char} {s : String} {pos pos' : s.Pos} :
pos.find? c = some pos' ↔
pos ≤ pos' ∧ (∃ h, pos'.get h = c) ∧
∀ pos'', pos ≤ pos'' → (h' : pos'' < pos') → pos''.get (Pos.ne_endPos_of_lt h') ≠ c := by
∀ pos'', pos ≤ pos'' → (h' : pos'' < pos') → pos''.get (by exact Pos.ne_endPos_of_lt h') ≠ c := by
simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_some_iff,
Slice.Pos.find?_char_eq_some_iff, ne_eq, endPos_toSlice]
refine ⟨?_, ?_⟩
@ -157,7 +161,7 @@ theorem contains_char_eq_contains_beq {c : Char} {s : String} :
theorem find?_char_eq_some_iff {c : Char} {s : String} {pos : s.Pos} :
s.find? c = some pos ↔
∃ h, pos.get h = c ∧ ∀ pos', (h' : pos' < pos) → pos'.get (Pos.ne_endPos_of_lt h') ≠ c := by
∃ h, pos.get h = c ∧ ∀ pos', (h' : pos' < pos) → pos'.get (by exact Pos.ne_endPos_of_lt h') ≠ c := by
simp only [find?_eq_find?_toSlice, Option.map_eq_some_iff, Slice.find?_char_eq_some_iff, ne_eq,
endPos_toSlice, exists_and_right]
refine ⟨?_, ?_⟩

12
src/Init/Data/String/Lemmas/Pattern/Find/Pred.lean
View file

@ -7,6 +7,8 @@ module
prelude
public import Init.Data.String.Slice
public import Init.Data.String.Search
public import Init.Data.String.Lemmas.Splits
import all Init.Data.String.Slice
import all Init.Data.String.Search
import Init.Data.String.Lemmas.Pattern.Find.Basic
@ -19,6 +21,8 @@ import Init.Grind
import Init.Data.Option.Lemmas
import Init.Data.String.OrderInstances
public section
namespace String.Slice
theorem find?_bool_eq_some_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} :
@ -178,7 +182,7 @@ theorem Pos.find?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos pos' :
pos.find? p = some pos' ↔
pos ≤ pos' ∧ (∃ h, p (pos'.get h)) ∧
∀ pos'', pos ≤ pos'' → (h' : pos'' < pos') →
p (pos''.get (Pos.ne_endPos_of_lt h')) = false := by
p (pos''.get (by exact Pos.ne_endPos_of_lt h')) = false := by
simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_some_iff,
Slice.Pos.find?_bool_eq_some_iff, endPos_toSlice]
refine ⟨?_, ?_⟩
@ -231,7 +235,7 @@ theorem Pos.find?_prop_eq_some_iff {p : Char → Prop} [DecidablePred p] {s : St
pos.find? p = some pos' ↔
pos ≤ pos' ∧ (∃ h, p (pos'.get h)) ∧
∀ pos'', pos ≤ pos'' → (h' : pos'' < pos') →
¬ p (pos''.get (Pos.ne_endPos_of_lt h')) := by
¬ p (pos''.get (by exact Pos.ne_endPos_of_lt h')) := by
simp only [Pos.find?_prop_eq_find?_decide, Pos.find?_bool_eq_some_iff, decide_eq_true_eq,
decide_eq_false_iff_not]
@ -256,7 +260,7 @@ theorem Pos.find?_prop_eq_none_iff_of_splits {p : Char → Prop} [DecidablePred
theorem find?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos : s.Pos} :
s.find? p = some pos ↔
∃ h, p (pos.get h) ∧ ∀ pos', (h' : pos' < pos) → p (pos'.get (Pos.ne_endPos_of_lt h')) = false := by
∃ h, p (pos.get h) ∧ ∀ pos', (h' : pos' < pos) → p (pos'.get (by exact Pos.ne_endPos_of_lt h')) = false := by
simp only [find?_eq_find?_toSlice, Option.map_eq_some_iff, Slice.find?_bool_eq_some_iff,
endPos_toSlice, exists_and_right]
refine ⟨?_, ?_⟩
@ -281,7 +285,7 @@ theorem find?_bool_eq_some_iff_splits {p : Char → Bool} {s : String} {pos : s.
theorem find?_prop_eq_some_iff {p : Char → Prop} [DecidablePred p] {s : String} {pos : s.Pos} :
s.find? p = some pos ↔
∃ h, p (pos.get h) ∧ ∀ pos', (h' : pos' < pos) → ¬ p (pos'.get (Pos.ne_endPos_of_lt h')) := by
∃ h, p (pos.get h) ∧ ∀ pos', (h' : pos' < pos) → ¬ p (pos'.get (by exact Pos.ne_endPos_of_lt h')) := by
simp only [find?_prop_eq_find?_decide, find?_bool_eq_some_iff, decide_eq_true_eq,
decide_eq_false_iff_not]