Skip to content

[Merged by Bors] - feat: grind golf in Mathlib.Data.List #29492

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
Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - feat: grind golf in Mathlib.Data.List #29492

wants to merge 8 commits into from

Conversation

@kim-em
Copy link
Contributor

@kim-em kim-em commented Sep 10, 2025

Much of this comes from locations identified by the new linter.tacticAnalysis.terminalToGrind, and then cleaning up in flagged files.

@github-actions github-actions bot added the t-data Data (lists, quotients, numbers, etc) label Sep 10, 2025
@github-actions
Copy link

github-actions bot commented Sep 10, 2025 •
edited
Loading

PR summary f4506f7151

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ cons_bagInteger
+ inter_cons
+ lookmap_cons

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

eric-wieser
eric-wieser reviewed Sep 10, 2025
View reviewed changes
Mathlib/Data/List/Basic.lean
Comment on lines 162 to +163
theorem exists_mem_cons_iff (p : α → Prop) (a : α) (l : List α) :
(∃ x ∈ a :: l, p x) ↔ p a ∨ ∃ x ∈ l, p x :=
Iff.intro or_exists_of_exists_mem_cons fun h =>
Or.elim h (exists_mem_cons_of l) exists_mem_cons_of_exists
(∃ x ∈ a :: l, p x) ↔ p a ∨ ∃ x ∈ l, p x := by grind
Copy link
Member

Choose a reason for hiding this comment

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

For this one specifically I quite like how the old proof spells out exactly what the names of the individual pieces are.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I disagree. This is a triviality, and I can't imagine how anyone could learn anything from the proof that they didn't already understand from the statement. In fact, this seems like one of the most extreme examples possible of this. :-) But I appreciate that my eyes glaze over on theorem names faster than most peoples'.

eric-wieser
eric-wieser reviewed Sep 10, 2025
View reviewed changes
Mathlib/Data/List/Lattice.lean
Comment on lines +181 to +183
@[grind =]
theorem cons_bagInteger :
(a :: l₁).bagInter l₂ = if a ∈ l₂ then a :: l₁.bagInter (l₂.erase a) else l₁.bagInter l₂ := by
Copy link
Member

Choose a reason for hiding this comment

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

Is the general rule with grind that unlike simp, we should encourage expansion of ifs? Could this be document somewhere (perhaps including but not limited to the commit message)?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I've finally started writing a document about this, in progress at leanprover/reference-manual#586.

euprunin
euprunin approved these changes Sep 11, 2025
View reviewed changes
Copy link
Collaborator

@euprunin euprunin left a comment

Choose a reason for hiding this comment

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

Line count: +74 -231

Impressive!

@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 15, 2025
@mathlib4-merge-conflict-bot
Copy link
Collaborator

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 16, 2025
@fpvandoorn
Copy link
Member

bors d+

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Sep 24, 2025

✌️ kim-em can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Sep 24, 2025
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 24, 2025
@mathlib4-merge-conflict-bot
Copy link
Collaborator

This pull request has conflicts, please merge master and resolve them.

@kim-em
Copy link
Contributor Author

kim-em commented Sep 24, 2025

bors merge

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Sep 24, 2025

👎 Rejected by label

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Sep 24, 2025
@kim-em kim-em removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 24, 2025
@kim-em
Copy link
Contributor Author

kim-em commented Sep 24, 2025

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Sep 24, 2025
@kim-em
feat: grind golf in Mathlib.Data.List (#29492)
365203e 
Much of this comes from locations identified by the new `linter.tacticAnalysis.terminalToGrind`, and then cleaning up in flagged files.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Sep 24, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: grind golf in Mathlib.Data.List [Merged by Bors] - feat: grind golf in Mathlib.Data.List Sep 24, 2025
@mathlib-bors mathlib-bors bot closed this Sep 24, 2025
joelriou pushed a commit to joelriou/mathlib4 that referenced this pull request Oct 2, 2025
@kim-em @joelriou
feat: grind golf in Mathlib.Data.List (leanprover-community#29492)
1ac5a96 
Much of this comes from locations identified by the new `linter.tacticAnalysis.terminalToGrind`, and then cleaning up in flagged files.
zhuyizheng pushed a commit to zhuyizheng/mathlib4 that referenced this pull request Oct 2, 2025
@kim-em @zhuyizheng
feat: grind golf in Mathlib.Data.List (leanprover-community#29492)
58bc00c 
Much of this comes from locations identified by the new `linter.tacticAnalysis.terminalToGrind`, and then cleaning up in flagged files.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

+1 more reviewer

@euprunin euprunin euprunin approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-data Data (lists, quotients, numbers, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@kim-em @mathlib4-merge-conflict-bot @fpvandoorn @eric-wieser @euprunin @leanprover-community-mathlib4-bot