Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
TwoFX merged 1 commit into from
Mar 5, 2026
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 6 additions & 2 deletions src/Init/Data/String/Lemmas/Pattern/Find/Char.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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} :
Expand Down Expand Up @@ -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 ⟨?_, ?_⟩
Expand Down Expand Up @@ -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 ⟨?_, ?_⟩
Expand Down
12 changes: 8 additions & 4 deletions src/Init/Data/String/Lemmas/Pattern/Find/Pred.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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} :
Expand Down Expand Up @@ -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 ⟨?_, ?_⟩
Expand Down Expand Up @@ -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]

Expand All @@ -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 ⟨?_, ?_⟩
Expand All @@ -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]

Expand Down
Loading