Skip to content

Comments

[Merged by Bors] - chore: classify simp can do this porting notes#10619

Closed
pitmonticone wants to merge 22 commits intomasterfrom
pitmonticone/porting-notes
Closed

[Merged by Bors] - chore: classify simp can do this porting notes#10619
pitmonticone wants to merge 22 commits intomasterfrom
pitmonticone/porting-notes

Conversation

@pitmonticone
Copy link
Member

@pitmonticone pitmonticone commented Feb 15, 2024 •
edited
Loading

Classify by adding issue number (#10618) to porting notes claiming anything semantically equivalent to simp can prove this or simp can simplify this.

eric-wieser
eric-wieser approved these changes Feb 15, 2024
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

I've skimmed this on the assumption it's in good faith. This looks good to me, and means that when grepping for untriaged porting notes we can exclude these.

@pitmonticone
Copy link
Member Author

pitmonticone commented Feb 15, 2024 •
edited
Loading

Thank you @eric-wieser.

Should I include these two?

mathlib4/Mathlib/Topology/Instances/AddCircle.lean

Lines 173 to 179 in 83adb4c

/- Porting note: `simp` attribute removed because linter reports:
simp can prove this:
by simp only [@mem_zmultiples, @QuotientAddGroup.mk_add_of_mem]
-/
theorem coe_add_period (x : 𝕜) : ((x + p : 𝕜) : AddCircle p) = x := by
rw [coe_add, ← eq_sub_iff_add_eq', sub_self, coe_period]
#align add_circle.coe_add_period AddCircle.coe_add_period

mathlib4/Mathlib/SetTheory/Lists.lean

Lines 86 to 89 in d15436a

-- porting notes: removed @[simp]
-- simp can prove this: by simp only [@Lists'.toList, @Sigma.eta]
theorem toList_cons (a : Lists α) (l) : toList (cons a l) = a :: l.toList := by simp
#align lists'.to_list_cons Lists'.toList_cons

PS: Included.

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 15, 2024
kbuzzard
kbuzzard approved these changes Feb 15, 2024
View reviewed changes
Copy link
Member

@kbuzzard kbuzzard left a comment •
edited
Loading

Choose a reason for hiding this comment

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

I've done a manual pass through this and it looks fine, but there are four instances which are not of the form "the following theorem used to be simp in lean 3 and we're removing the attribute here", which I've flagged as perhaps needing further attention.

Mathlib/CategoryTheory/Limits/IsLimit.lean
attribute [reassoc (attr := simp)] IsColimit.fac

-- Porting note: simp can prove this. Linter claims it still is tagged with simp
-- Porting note (#10618): simp can prove this. Linter claims it still is tagged with simp
Copy link
Member

@kbuzzard kbuzzard Feb 15, 2024

Choose a reason for hiding this comment

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

What is going on with this one? Is this a bug in the simpNF linter?

Copy link
Member Author

@pitmonticone pitmonticone Feb 20, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

This question should probably be reported in the corresponding issue #10618.

Copy link
Member Author

@pitmonticone pitmonticone Feb 20, 2024

Choose a reason for hiding this comment

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

Now this question can be found here.

Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
attribute [inherit_doc IsBilimit] IsBilimit.isLimit IsBilimit.isColimit

-- Porting note: simp can prove this, linter doesn't notice it is removed
-- Porting note (#10618): simp can prove this, linter doesn't notice it is removed
Copy link
Member

@kbuzzard kbuzzard Feb 15, 2024

Choose a reason for hiding this comment

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

And this one!

Copy link
Member Author

@pitmonticone pitmonticone Feb 20, 2024

Choose a reason for hiding this comment

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

Now this question can be found here.

Mathlib/Data/Vector.lean

/-- A nil vector maps to a nil list. -/
@[simp, nolint simpNF] -- Porting note: simp can prove this in the future
@[simp, nolint simpNF] -- Porting note (#10618): simp can prove this in the future
Copy link
Member

@kbuzzard kbuzzard Feb 15, 2024

Choose a reason for hiding this comment

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

Is this the correct solution for this problem?

Copy link
Member Author

@pitmonticone pitmonticone Feb 20, 2024

Choose a reason for hiding this comment

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

Now this question can be found here.

@pitmonticone pitmonticone added the porting-notes Mathlib3 to Mathlib4 porting notes. label Feb 17, 2024
@pitmonticone pitmonticone changed the title chore: add issue number to simp porting notes chore: classify porting notes with simp can prove this or simp can simplify this Feb 18, 2024
@pitmonticone pitmonticone changed the title chore: classify porting notes with simp can prove this or simp can simplify this chore: classify simp can do this porting notes Feb 18, 2024
@pitmonticone pitmonticone changed the title chore: classify simp can do this porting notes chore: classify simp can prove / simplify this porting notes Feb 18, 2024
@pitmonticone pitmonticone changed the title chore: classify simp can prove / simplify this porting notes chore: classify simp can prove / simplify this porting notes Feb 18, 2024
@pitmonticone pitmonticone changed the title chore: classify simp can prove / simplify this porting notes chore: classify simp can do this porting notes Feb 18, 2024
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Feb 18, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 20, 2024
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Feb 20, 2024
@Vierkantor Vierkantor mentioned this pull request Feb 20, 2024
Closed
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 20, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 20, 2024
@pitmonticone pitmonticone mentioned this pull request Feb 20, 2024
Closed
jcommelin
jcommelin approved these changes Feb 20, 2024
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Feb 20, 2024
mathlib-bors bot pushed a commit that referenced this pull request Feb 20, 2024
@pitmonticone
chore: classify simp can do this porting notes (#10619)
de765f6 
Classify by adding issue number (#10618) to porting notes claiming anything semantically equivalent to `simp can prove this` or `simp can simplify this`.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Feb 20, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: classify simp can do this porting notes [Merged by Bors] - chore: classify simp can do this porting notes Feb 20, 2024
@mathlib-bors mathlib-bors bot closed this Feb 20, 2024
@mathlib-bors mathlib-bors bot deleted the pitmonticone/porting-notes branch February 20, 2024 23:51
thorimur pushed a commit that referenced this pull request Feb 24, 2024
@pitmonticone @thorimur
chore: classify simp can do this porting notes (#10619)
f21a0fe 
Classify by adding issue number (#10618) to porting notes claiming anything semantically equivalent to `simp can prove this` or `simp can simplify this`.
thorimur pushed a commit that referenced this pull request Feb 26, 2024
@pitmonticone @thorimur
chore: classify simp can do this porting notes (#10619)
2f6f7c6 
Classify by adding issue number (#10618) to porting notes claiming anything semantically equivalent to `simp can prove this` or `simp can simplify this`.
riccardobrasca pushed a commit that referenced this pull request Mar 1, 2024
@pitmonticone @riccardobrasca
chore: classify simp can do this porting notes (#10619)
9112b06 
Classify by adding issue number (#10618) to porting notes claiming anything semantically equivalent to `simp can prove this` or `simp can simplify this`.
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@pitmonticone @dagurtomas
chore: classify simp can do this porting notes (#10619)
4b292e8 
Classify by adding issue number (#10618) to porting notes claiming anything semantically equivalent to `simp can prove this` or `simp can simplify this`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin approved these changes

@mattrobball mattrobball Awaiting requested review from mattrobball

@Vierkantor Vierkantor Awaiting requested review from Vierkantor

@eric-wieser eric-wieser Awaiting requested review from eric-wieser

@kbuzzard kbuzzard Awaiting requested review from kbuzzard

Assignees

No one assigned

Labels

porting-notes Mathlib3 to Mathlib4 porting notes. ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@pitmonticone @eric-wieser @jcommelin @kbuzzard