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 String.isPrefixOf theorems #809

Open
wants to merge 16 commits into
base: main
Choose a base branch
from
Open

feat: Add String.isPrefixOf theorems #809

wants to merge 16 commits into from

Conversation

tjf801
Copy link
Contributor

@tjf801 tjf801 commented May 23, 2024

This PR is a redo of #782, but adds the following:

  • Auxiliary theorems used to prove the theorems below
  • Proof of equivalence between String.isPrefixOf s t and ∃ t, s = p ++ t
    • (This is analogous to how List.IsPrefix is defined.)
  • Proof of equivalence between String.isPrefixOf s t and List.isPrefixOf s.data t.data

tjf801 and others added 13 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 @kim-em
add info about unusedHavesSuffices lint
b0ac67f 
Co-authored-by: Kim Morrison <[email protected]>
@tjf801
remove unnecessary data_append theorem
9c1bf76
@tjf801
Merge branch 'main' into isPrefixOf-theorems
10a27cc
@tjf801
Revert "remove unnecessary data_append theorem"
cc2174d 
This reverts commit 9c1bf76.
@tjf801
make cons_append not @[simp]
c7d6250
@tjf801
Merge branch 'leanprover-community:main' into isPrefixOf-theorems
8895e19
@tjf801
Add substrEq_cons
c2eedba
@tjf801
Add isPrefixOf lemmas
2aabdc1 
- `isPrefixOf_cons`
- `exists_append_of_isPrefixOf`
- `isPrefixOf_iff_exists_append`
- `isPrefixOf_trans`
- `data_isPrefixOf_iff_isPrefixOf`
@tjf801 @chabulhwi
Keep TODOs in for future unproven string theorems
8b65f75 
Co-Authored-By: Bulhwi Cha <[email protected]>
@tjf801
Fix linter fail
c0e34b1 
Oddly enough, this line wasn't 100 characters long, so my editor's linter didn't even flag this 🤔
@tjf801
fix unusedHavesSuffices x3
4c1b33e
@tjf801 tjf801 force-pushed the isPrefixOf-theorems-2 branch from 4323ce0 to 4c1b33e Compare May 23, 2024 17:37
@tjf801
Copy link
Contributor Author

tjf801 commented May 24, 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 24, 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 Jun 7, 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 Jun 10, 2024
tjf801 and others added 2 commits June 14, 2024 11:13
@tjf801
Update isPrefixOf lemmas for v4.9.0
e5bb255 
- remove `@[nolint unusedHavesSuffices]` since leanprover/lean4#4143 has been merged
- some `termination_by` arguments can now be inferred
@fgdorais
chore: merge main and trigger Mathlib check
3142684
@fgdorais fgdorais 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 Oct 5, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-author Waiting for PR author to address issues
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@tjf801 @fgdorais @leanprover-community-mathlib4-bot