[Merged by Bors] - feat(tactic/to_additive): Improvements to to_additive #5487

alexjbest · 2020-12-23T22:21:39Z

Change a couple of things in to_additive:

First add a tactic.copy_attribute' intended for user attributes with parameters very similar to tactic.copy_attribute that just copies the parameter over when setting the attribute. This allows to_additive after many other attributes to transfer those attributes properly (e.g. norm_cast)
Have to additive register generated equation lemmas as such, this necessitates a bit of restructuring, first all declarations must be generated (including equational lemmas), then the equational lemmas need their attributes, then they are registered as equation lemmas, finally the attributes are added to the main declaration.
I also fixup the library in many places to account for these changes simplifying the source files, only one new lemma was added, in src/analysis/normed/group/quotient.lean quotient_norm_mk_le' to replace the unprimed version in the proof of norm_normed_mk_le as simp got better thanks to the new simp lemmas introduced by this PR. Probably many more handwritten additive versions can now be deleted in a future PR, especially defs and instances.
All other library changes are just simplifications by using to additive for some hand generated declarations, and many more attributes on the generated lemmas.
The attribute mono is trickier as it contains for its parameter not actual exprs containing names but exprs making names from strings, so I don't see how to handle it right now. We now warn the user about this, and fix the library in a couple of places.

See also #5468

…here possible

src/tactic/transform_decl.lean

alexjbest · 2021-01-04T11:33:38Z

Thanks for reviewing this @robertylewis, I hope to come back to it soon,

fpvandoorn · 2021-01-08T03:42:02Z

What you're doing is almost the same as https://leanprover-community.github.io/mathlib_docs/tactic/core.html#tactic.set_attribute
The only difference seem to be the parameter we give to the new attribute. Maybe we can find a common generalization that takes as argument some kind of tactic that generates the parameter for us?

fpvandoorn · 2021-01-08T03:46:44Z

This issue closes #1639, right?

EDIT: At least, if you add `ext to the list (unless there is a reason that @[ext] behaves differently)

into norm_cast_to_additive

src/analysis/normed_space/normed_group_quotient.lean

Since #9138 and #5487 to_additive got a lot better, so a lot of duplication in the library becomes unnecessary and makes maintenence a burden. So we remove a large number of copy-pasted declarations that can now be generated automatically.

fpvandoorn

These are great improvements.

I have some suggestions, but since this PR is so big and desired, I'm also happy if they are done in follow-up PRs.

bors d+

fpvandoorn · 2021-10-18T17:47:56Z

src/tactic/transform_decl.lean

+tactic unit := do
+  get_decl tgt <|> fail!"unknown declaration {tgt}",
+  -- if the source doesn't have the attribute we do not error and simply return
+  mwhen (succeeds (has_attribute attr_name src)) $


Suggested change

mwhen (succeeds (has_attribute attr_name src)) $

tt ← has_attribute' attr_name src | skip,

if you do this you don't have to indent / add a nested do on the next line.

Oh this is smart! Thanks

fpvandoorn · 2021-10-18T18:09:30Z

src/algebra/group/to_additive.lean

+      mwhen (has_attribute' `mono src)
+        (trace $ "to_additive does not work with mono, apply the mono attribute to both" ++
+          "versions after"),


There are a couple ways to fix mono.

Maybe we have a way to modify mono so that it accepts the attribute when it's provided with a (wrong) first argument. This might be tricky.

We could also modify to_additive so that it works with mono.
We can add a clause to copy_attribute' special-casing mono. Something like if attr_name = "mono" then [add the attribute, but with `none` as first component]

Another way I thought of, but which is worse:
We can copy the attribute by using tactic.set_attribute. In this case

We should fix the inhabited instance of mono_selection to evaluate to mono_selection.both

We should probably check that the original parameter was also equal to both (and otherwise fail).

To be honest I didn't think too much about fixing mono recently, once I realised what the issue with it seemed too annoying to tackle for the relative gain. But I'll have a think about your suggestions :)

bors · 2021-10-18T18:10:10Z

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

alexjbest · 2021-10-18T18:14:58Z

Thanks Floris, I will take you at your word and make any changes in a follow up so we can hopefully avoid merge conflicts.

bors r+

Change a couple of things in to_additive: - First add a `tactic.copy_attribute'` intended for user attributes with parameters very similar to `tactic.copy_attribute` that just copies the parameter over when setting the attribute. This allows to_additive after many other attributes to transfer those attributes properly (e.g. norm_cast) - Have to additive register generated equation lemmas as such, this necessitates a bit of restructuring, first all declarations must be generated (including equational lemmas), then the equational lemmas need their attributes, then they are registered as equation lemmas, finally the attributes are added to the main declaration. - I also fixup the library in many places to account for these changes simplifying the source files, only one new lemma was added, in src/analysis/normed/group/quotient.lean `quotient_norm_mk_le'` to replace the unprimed version in the proof of `norm_normed_mk_le` as simp got better thanks to the new simp lemmas introduced by this PR. Probably many more handwritten additive versions can now be deleted in a future PR, especially defs and instances. - All other library changes are just simplifications by using to additive for some hand generated declarations, and many more attributes on the generated lemmas. - The attribute mono is trickier as it contains for its parameter not actual exprs containing names but exprs making names from strings, so I don't see how to handle it right now. We now warn the user about this, and fix the library in a couple of places.

bors · 2021-10-18T21:08:01Z

Build failed (retrying...):

Build mathlib

Change a couple of things in to_additive: - First add a `tactic.copy_attribute'` intended for user attributes with parameters very similar to `tactic.copy_attribute` that just copies the parameter over when setting the attribute. This allows to_additive after many other attributes to transfer those attributes properly (e.g. norm_cast) - Have to additive register generated equation lemmas as such, this necessitates a bit of restructuring, first all declarations must be generated (including equational lemmas), then the equational lemmas need their attributes, then they are registered as equation lemmas, finally the attributes are added to the main declaration. - I also fixup the library in many places to account for these changes simplifying the source files, only one new lemma was added, in src/analysis/normed/group/quotient.lean `quotient_norm_mk_le'` to replace the unprimed version in the proof of `norm_normed_mk_le` as simp got better thanks to the new simp lemmas introduced by this PR. Probably many more handwritten additive versions can now be deleted in a future PR, especially defs and instances. - All other library changes are just simplifications by using to additive for some hand generated declarations, and many more attributes on the generated lemmas. - The attribute mono is trickier as it contains for its parameter not actual exprs containing names but exprs making names from strings, so I don't see how to handle it right now. We now warn the user about this, and fix the library in a couple of places.

bors · 2021-10-19T02:23:52Z

Pull request successfully merged into master.

Build succeeded:

Since #9138 and #5487 to_additive got a lot better, so a lot of duplication in the library becomes unnecessary and makes maintenence a burden. So we remove a large number of copy-pasted declarations that can now be generated automatically.

Change a couple of things in to_additive: - First add a `tactic.copy_attribute'` intended for user attributes with parameters very similar to `tactic.copy_attribute` that just copies the parameter over when setting the attribute. This allows to_additive after many other attributes to transfer those attributes properly (e.g. norm_cast) - Have to additive register generated equation lemmas as such, this necessitates a bit of restructuring, first all declarations must be generated (including equational lemmas), then the equational lemmas need their attributes, then they are registered as equation lemmas, finally the attributes are added to the main declaration. - I also fixup the library in many places to account for these changes simplifying the source files, only one new lemma was added, in src/analysis/normed/group/quotient.lean `quotient_norm_mk_le'` to replace the unprimed version in the proof of `norm_normed_mk_le` as simp got better thanks to the new simp lemmas introduced by this PR. Probably many more handwritten additive versions can now be deleted in a future PR, especially defs and instances. - All other library changes are just simplifications by using to additive for some hand generated declarations, and many more attributes on the generated lemmas. - The attribute mono is trickier as it contains for its parameter not actual exprs containing names but exprs making names from strings, so I don't see how to handle it right now. We now warn the user about this, and fix the library in a couple of places.

Since #9138 and #5487 to_additive got a lot better, so a lot of duplication in the library becomes unnecessary and makes maintenence a burden. So we remove a large number of copy-pasted declarations that can now be generated automatically.

alexjbest added 5 commits December 23, 2020 17:16

allow to_additive to run after norm cast, copy the options over too

af735a0

fix test

5af9124

remove old by hand norm cast attributes and replace with decorators w…

d16a80e

…here possible

add a docstring

d538c89

fix long line

b8e42ca

alexjbest added awaiting-review The author would like community review of the PR t-meta Tactics, attributes or user commands labels Dec 24, 2020

alexjbest added 2 commits December 24, 2020 00:36

fix docstring

01aa363

add continuity to to_additive also

40a4306

alexjbest changed the title ~~feat(tactic/to_additive) Allow to_additive after norm_cast~~ feat(tactic/to_additive) Allow to_additive after norm_cast or continuity Dec 24, 2020

robertylewis reviewed Dec 24, 2020

View reviewed changes

src/tactic/transform_decl.lean Show resolved Hide resolved

src/tactic/transform_decl.lean Outdated Show resolved Hide resolved

src/tactic/transform_decl.lean Outdated Show resolved Hide resolved

src/tactic/transform_decl.lean Outdated Show resolved Hide resolved

robertylewis added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Dec 24, 2020

bryangingechen mentioned this pull request Jan 2, 2021

[Merged by Bors] - feat(algebra/ordered_group): add linear_ordered_comm_group and linear_ordered_cancel_comm_monoid #5286

Closed

bryangingechen changed the title ~~feat(tactic/to_additive) Allow to_additive after norm_cast or continuity~~ feat(tactic/to_additive): Allow to_additive after norm_cast or continuity Jan 2, 2021

github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jan 27, 2021

alexjbest added the please-adopt This PR/issue may have been abandoned by the original contributor. You are welcome to take it over. label Mar 15, 2021

Merge branch 'master' of https://github.com/leanprover-community/mathlib

721d5ff

into norm_cast_to_additive

github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jun 1, 2021

alexjbest removed the please-adopt This PR/issue may have been abandoned by the original contributor. You are welcome to take it over. label Jun 1, 2021

alexjbest added 3 commits June 1, 2021 18:29

more potential

40ba790

fix bad merge

c970d15

new simp lemmas broke some proofs

e08bbca

alexjbest commented Jun 2, 2021

View reviewed changes

src/analysis/normed_space/normed_group_quotient.lean Outdated Show resolved Hide resolved

github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jun 4, 2021

alexjbest added 2 commits June 4, 2021 08:56

no_rsimp

82026a0

ematch

cb152d7

alexjbest added 6 commits October 17, 2021 16:23

fix some mono examples

b21c83b

fix namespace?

3b7df0f

add more comments

cb3d6d5

remove errant comma

9b364d3

fix tests

4fb0b21

unused arg

aa26c00

alexjbest added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 17, 2021

fix it properly

624e564

alexjbest mentioned this pull request Oct 18, 2021

[Merged by Bors] - chore(*): clean up the library using to_additive #9790

Closed

1 task

fix accidental ext breakage

47f1b37

fpvandoorn approved these changes Oct 18, 2021

View reviewed changes

github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Oct 18, 2021

bors bot changed the title ~~feat(tactic/to_additive): Improvements to to_additive~~ [Merged by Bors] - feat(tactic/to_additive): Improvements to to_additive Oct 19, 2021

bors bot closed this Oct 19, 2021

bors bot deleted the norm_cast_to_additive branch October 19, 2021 02:23

fpvandoorn mentioned this pull request Nov 8, 2021

to_additive should copy simps and extensionality #1639

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(tactic/to_additive): Improvements to to_additive #5487

[Merged by Bors] - feat(tactic/to_additive): Improvements to to_additive #5487

alexjbest commented Dec 23, 2020 •

edited

Loading

alexjbest commented Jan 4, 2021 •

edited

Loading

fpvandoorn commented Jan 8, 2021 •

edited

Loading

fpvandoorn commented Jan 8, 2021 •

edited

Loading

fpvandoorn left a comment

fpvandoorn Oct 18, 2021

alexjbest Oct 18, 2021

fpvandoorn Oct 18, 2021

alexjbest Oct 18, 2021

bors bot commented Oct 18, 2021

alexjbest commented Oct 18, 2021

bors bot commented Oct 18, 2021

bors bot commented Oct 19, 2021

	mwhen (succeeds (has_attribute attr_name src)) $
	tt ← has_attribute' attr_name src \| skip,

[Merged by Bors] - feat(tactic/to_additive): Improvements to to_additive #5487

[Merged by Bors] - feat(tactic/to_additive): Improvements to to_additive #5487

Conversation

alexjbest commented Dec 23, 2020 • edited Loading

alexjbest commented Jan 4, 2021 • edited Loading

fpvandoorn commented Jan 8, 2021 • edited Loading

fpvandoorn commented Jan 8, 2021 • edited Loading

fpvandoorn left a comment

Choose a reason for hiding this comment

fpvandoorn Oct 18, 2021

Choose a reason for hiding this comment

alexjbest Oct 18, 2021

Choose a reason for hiding this comment

fpvandoorn Oct 18, 2021

Choose a reason for hiding this comment

alexjbest Oct 18, 2021

Choose a reason for hiding this comment

bors bot commented Oct 18, 2021

alexjbest commented Oct 18, 2021

bors bot commented Oct 18, 2021

bors bot commented Oct 19, 2021

alexjbest commented Dec 23, 2020 •

edited

Loading

alexjbest commented Jan 4, 2021 •

edited

Loading

fpvandoorn commented Jan 8, 2021 •

edited

Loading

fpvandoorn commented Jan 8, 2021 •

edited

Loading