Skip to content
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

Jump to bottom

Definition of String.splitOn is incorrect #3829

Closed
chabulhwi opened this issue Apr 3, 2024 · 1 comment · Fixed by #3832
Closed

Definition of String.splitOn is incorrect #3829

chabulhwi opened this issue Apr 3, 2024 · 1 comment · Fixed by #3832
Labels
bug Something isn't working

Comments

@chabulhwi
Copy link
Contributor

chabulhwi commented Apr 3, 2024 •
edited
Loading

Description

#eval "012".splitOn "12" -- output: ["0", ""]
#eval "007".splitOn "07" -- ["007"]

The value of the second expression above should be ["0", ""].

Context

I was trying to prove String.splitOn_of_valid in Std.Data.List.Lemmas, but I realized that the current definition of String.splitOn is flawed. See leanprover-community/batteries#719.

I think @digama0's definition of List.splitOnList in Std.Data.List.SplitOnList is correct, as can be seen below:

import Std.Data.List.SplitOnList

#eval ("012".1.splitOnList "12".1).map String.mk -- output: ["0", ""]
#eval ("007".1.splitOnList "07".1).map String.mk -- ["0", ""]

Discussions on the Lean Zulip chat: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/current.20definition.20of.20.60String.2EsplitOn.60.20is.20incorrect/near/430930535

Version

4.7.0-rc2

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
@chabulhwi chabulhwi added the bug Something isn't working label Apr 3, 2024
@chabulhwi chabulhwi mentioned this issue Apr 3, 2024
Closed
@chabulhwi
Copy link
Contributor Author

#3832 fixes this bug.

@digama0 digama0 mentioned this issue Apr 4, 2024
Merged
github-merge-queue bot pushed a commit that referenced this issue Apr 4, 2024
@digama0
fix: String.splitOn bug (#3832)
e41cd31 
Fixes #3829. As reported on Zulip (both
[recently](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/current.20definition.20of.20.60String.2EsplitOn.60.20is.20incorrect/near/430930535)
and [a year
ago](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/should.20we.20redefine.20.60String.2EsplitOnAux.60.3F/near/365899332)),
`String.splitOn` has a bug when dealing with separators of more than one
character (which are luckily rare). The code change here is very small,
replacing a `i` with `i - j`, but it makes termination more complex so
that's where the rest of the line count goes.
@Kha Kha closed this as completed in #3832 Apr 4, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something isn't working
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: String.splitOn bug digama0/lean4
1 participant
@chabulhwi