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

feat: Add some theorems for String.substrEq and String.isPrefixOf #782

Closed
wants to merge 8 commits into from
Closed

feat: Add some theorems for String.substrEq and String.isPrefixOf #782

wants to merge 8 commits into from
+109 −2

Conversation

tjf801
Copy link
Contributor

@tjf801 tjf801 commented May 6, 2024

No description provided.

tjf801 added 2 commits May 6, 2024 14:55
@tjf801
Add lemmas necessary for isPrefixOf proofs
0489657 
- `String.cons_append`
- `String.Pos.empty_valid`
- `String.Pos.Valid.cons_addChar`
- `String.Pos.Valid.cons_zero_or_ge_head`

Update Lemmas.lean

Update Lemmas.lean
@tjf801
Add isPrefixOf proofs
b4afe21
@tjf801
Copy link
Contributor Author

tjf801 commented May 6, 2024

awaiting-review

@github-actions github-actions bot added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label May 6, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label May 7, 2024
semorrison
semorrison reviewed May 13, 2024
View reviewed changes
Std/Data/String/Lemmas.lean Outdated
@@ -60,6 +60,9 @@ instance : Std.BEqOrd String := .compareOfLessAndEq String.lt_irrefl

@[simp] theorem data_append (s t : String) : (s ++ t).1 = s.1 ++ t.1 := rfl

@[simp] theorem cons_append (c : Char) (cs : List Char) (t : String) :
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm skeptical this should be a @[simp] lemma.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You don't seem to have removed this (or explained why you think it should stay).

semorrison
semorrison approved these changes May 13, 2024
View reviewed changes
Copy link
Collaborator

@semorrison semorrison left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Otherwise LGTM.

@semorrison
Copy link
Collaborator

Please merge main and resolve the conflict.

@semorrison semorrison added awaiting-author Waiting for PR author to address issues and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels May 13, 2024
@tjf801
Copy link
Contributor Author

tjf801 commented May 13, 2024

awaiting-review

@github-actions github-actions bot added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed awaiting-author Waiting for PR author to address issues labels May 13, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label May 13, 2024
@semorrison semorrison added awaiting-author Waiting for PR author to address issues and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels May 13, 2024
@tjf801
Copy link
Contributor Author

tjf801 commented May 13, 2024

awaiting-review

@github-actions github-actions bot added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed awaiting-author Waiting for PR author to address issues labels May 13, 2024
@tjf801 tjf801 changed the title Add some theorems for String.substrEq and String.isPrefixOf feat: Add some theorems for String.substrEq and String.isPrefixOf May 18, 2024
@chabulhwi
Copy link
Contributor

chabulhwi commented May 23, 2024 •
edited

@chabulhwi said:

By the way, I proved that List.IsPrefix is equivalent to List.isPrefixOf, and List.IsSuffix is equivalent to List.isSuffixOf. It'll be nice if Lean can automatically generate lemmas for isPrefixOf and isSuffixOf whenever I prove those for IsPrefix and IsSuffix. Do you think this is a good idea? If so, how do we do that?

@digama0 said:

the idea is to have all the lemmas about IsPrefix, and have a simp lemma saying isPrefixOf l1 l2 <-> IsPrefix l1 l2, and then you never have to worry about isPrefixOf again

@tjf801 I'm pretty sure String.IsPrefix and String.isPrefixOf are equivalent, as List.IsPrefix and List.isPrefixOf do. I suggest you replace your theorems about isPrefixOf with the IsPrefix counterparts.

chabulhwi
chabulhwi reviewed May 23, 2024
View reviewed changes
Batteries/Data/String/Lemmas.lean
Comment on lines -782 to -783
-- TODO: substrEq
-- TODO: isPrefixOf
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please don't remove these lines! These are two of the ten unproved theorems specifying string operations, which I'll prove in the future.

@tjf801
Copy link
Contributor Author

tjf801 commented May 23, 2024 •
edited

I'm pretty sure that String.IsPrefix is in Mathlib, so all of that would require upstreaming that definition from there. (On a related note, if String and List eventually both have IsPrefix in Batteries, would it be a good idea to turn the <+: operator, which currently is an alias for List.isPrefixOf into a typeclass? But that's a question for another time.)

However, in the time that this PR has been opened, I used these theorems to actually prove the equivalence between String.isPrefixOf and List.isPrefixOf, and at least the way I did it, it was non-trivial and uses most of these theorems about isPrefixOf specifically as dependencies. At this point in time, it's probably better to just close this PR and do a new one with all of these changes.

Also, I'm sorry! I didn't realize those two lines served a specific purpose. Won't make that mistake again 🫡

@tjf801 tjf801 closed this May 23, 2024
@tjf801 tjf801 mentioned this pull request May 23, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@semorrison semorrison semorrison approved these changes

@chabulhwi chabulhwi chabulhwi left review comments

Assignees
No one assigned
Labels
awaiting-review This PR is ready for review; the author thinks it is ready to be merged.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@tjf801 @semorrison @chabulhwi @leanprover-community-mathlib4-bot