Skip to content

chore(GroupTheory/Coset): reduce defeq abuse#15483

Open
astrainfinita wants to merge 6 commits intomasterfrom
FR_real_quotientgroup_defeqabuse
Open

chore(GroupTheory/Coset): reduce defeq abuse#15483
astrainfinita wants to merge 6 commits intomasterfrom
FR_real_quotientgroup_defeqabuse

Conversation

@astrainfinita
Copy link
Copy Markdown
Collaborator

@astrainfinita astrainfinita commented Aug 4, 2024 •
edited by Parcly-Taxel
Loading

@astrainfinita astrainfinita added the t-algebra Algebra (groups, rings, fields, etc) label Aug 4, 2024
@astrainfinita astrainfinita mentioned this pull request Aug 4, 2024
Closed
@mergify
Copy link
Copy Markdown

mergify bot commented Aug 4, 2024

⚠️ The sha of the head commit of this PR conflicts with #15482. Mergify cannot evaluate rules on this PR. ⚠️

@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 4, 2024 •
edited
Loading

PR summary 69418e6d36

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ congr'
+ induction_on₂
+ map'
+ map'_mk
+ mk
+ ofQuotient
+ ofQuotient_mk
+ ofQuotient_toQuotient
+ toQuotient
+ toQuotient_mk
+ toQuotient_ofQuotient

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.

@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 4, 2024
@mergify
Copy link
Copy Markdown

mergify bot commented Aug 4, 2024

⚠️ The sha of the head commit of this PR conflicts with #15482. Mergify cannot evaluate rules on this PR. ⚠️

@astrainfinita astrainfinita force-pushed the FR_real_quotientgroup_defeqabuse branch from 138c3ae to efc402f Compare August 4, 2024 11:51
@astrainfinita astrainfinita force-pushed the FR_real_quotientgroup_defeqabuse branch from efc402f to dd5fa22 Compare August 4, 2024 11:57
@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Aug 4, 2024

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Aug 4, 2024

Here are the benchmark results for commit b292044.
There were significant changes against commit 10a631f:

  Benchmark                         Metric         Change
  =======================================================
+ ~Mathlib.GroupTheory.CosetCover   instructions   -18.1%

@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 5, 2024
@ghost
Copy link
Copy Markdown

ghost commented Aug 5, 2024

This PR/issue depends on:

eric-wieser
eric-wieser reviewed Aug 5, 2024
View reviewed changes
Mathlib/GroupTheory/Coset.lean
Comment on lines +354 to +357
/-- Reinterpret `x : Quotient (leftRel s)` as an element of `α ⧸ s`. -/
@[to_additive "Reinterpret `x : Quotient (leftRel s)` as an element of `α ⧸ s`."]
def ofQuotient (x : Quotient (leftRel s)) : α ⧸ s :=
x
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser Aug 5, 2024

Choose a reason for hiding this comment

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

This all seems a bit weird to me; do we even want these to be separate types in the first place? Would making HasQuotient and its projections reducible work instead?

Copy link
Copy Markdown
Member

@urkud urkud Aug 7, 2024

Choose a reason for hiding this comment

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

Another option is to make HasQuotient output a Setoid, then take a quotient w.r.t. this setoid. I don't know what will be slow/fast, though.

Copy link
Copy Markdown
Collaborator Author

@astrainfinita astrainfinita Aug 7, 2024

Choose a reason for hiding this comment

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

#15585 #15586 I think if making QuotientAddGroup.mk an abbrev, neither method will resolve the timeout.

Copy link
Copy Markdown
Member

@urkud urkud Aug 8, 2024

Choose a reason for hiding this comment

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

@mattrobball What's your opinion here?

@mattrobball
Copy link
Copy Markdown
Contributor

mattrobball commented Aug 8, 2024

If you want to implement #15474 (which I certainly do), you just need to remove some simp theorems that really should not be simp theorems to begin with #15591. Then other changes can be evaluated on their own.

@urkud
Copy link
Copy Markdown
Member

urkud commented Aug 8, 2024

I sent #15591 to bors.

@mattrobball
Copy link
Copy Markdown
Contributor

mattrobball commented Aug 8, 2024

The fixes to to_additive should build with master shortly then

@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 Aug 10, 2024
@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Apr 15, 2025

Coming here from PR triage: do the changes still apply in principle? If so, can you merge master, please?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@urkud urkud urkud left review comments

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

Assignees

No one assigned

Labels

merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@astrainfinita @leanprover-bot @mattrobball @urkud @grunweg @eric-wieser