[Merged by Bors] - chore(*): add a `div`/`sub` field to (`add_`)`group`(`_with_zero`) by Vierkantor · Pull Request #5303 · leanprover-community/mathlib3

Vierkantor · 2020-12-10T11:06:00Z

This PR is intended to fix the following kind of diamonds:
Let foo X be a type with a ∀ X, has_div (foo X) instance but no ∀ X, has_inv (foo X), e.g. when foo X is a euclidean_domain. Suppose we also have an instance ∀ X [cromulent X], group_with_zero (foo X). Then the (/) coming from group_with_zero_has_div cannot be defeq to the (/) coming from foo.has_div.

As a consequence of making the has_div instances defeq, we can no longer assume that (div_eq_mul_inv a b : a / b = a * b⁻¹) = rfl for all groups. The previous preparation PR #5302 should have changed all places in mathlib that assumed defeqness, to rewrite explicitly instead.

depends on: [Merged by Bors] - chore(*): don't assume sub_eq_add_neg and div_eq_mul_inv are defeq #5302

#5302) This PR prepares for a follow-up PR (#5303) that adds `div` and `sub` fields to (`add_`)`group`(`_with_zero`). That follow-up PR is intended to fix the following kind of diamonds: Let `foo X` be a type with a `∀ X, has_div (foo X)` instance but no `∀ X, has_inv (foo X)`, e.g. when `foo X` is a `euclidean_domain`. Suppose we also have an instance `∀ X [cromulent X], group_with_zero (foo X)`. Then the `(/)` coming from `group_with_zero_has_div` cannot be defeq to the `(/)` coming from `foo.has_div`. As a consequence of making the `has_div` instances defeq, we can no longer assume that `(div_eq_mul_inv a b : a / b = a * b⁻¹) = rfl` for all groups. This preparation PR should have changed all places in mathlib that assumed defeqness, to rewrite explicitly instead. Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60div.60.20as.20a.20field.20in.20.60group(_with_zero).60 Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

github-actions · 2020-12-11T16:48:10Z

🎉 Great news! Looks like all the dependencies have been resolved:

~~[Merged by Bors] - chore(*): don't assume sub_eq_add_neg and div_eq_mul_inv are defeq #5302~~

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

Vierkantor · 2020-12-11T22:51:51Z

There seem to be no obvious breakages in the low-level files, so let's see what CI thinks of the whole of mathlib...

sgouezel · 2020-12-14T07:58:23Z

Does not build yet

Vierkantor · 2020-12-14T11:53:37Z

Now it compiles successfully on my machine.

sgouezel

It would be worth adding somehwere a comment explaining why you choose to have fields sub and div instead of using x + - y or x * y^{-1}, by mentioning the example that is a motivation for the PR.

Vierkantor · 2020-12-14T16:52:26Z

It would be worth adding somehwere a comment explaining why you choose to have fields sub and div instead of using x + - y or x * y^{-1}, by mentioning the example that is a motivation for the PR.

I have added this as a comment on the declarations of div_inv_monoid/sub_neg_monoid.

This PR is intended to fix the following kind of diamonds: Let `foo X` be a type with a `∀ X, has_div (foo X)` instance but no `∀ X, has_inv (foo X)`, e.g. when `foo X` is a `euclidean_domain`. Suppose we also have an instance `∀ X [cromulent X], group_with_zero (foo X)`. Then the `(/)` coming from `group_with_zero_has_div` cannot be defeq to the `(/)` coming from `foo.has_div`. As a consequence of making the `has_div` instances defeq, we can no longer assume that `(div_eq_mul_inv a b : a / b = a * b⁻¹) = rfl` for all groups. The previous preparation commit should have changed all places in mathlib that assumed defeqness, to rewrite explicitly instead.

…riables

(I could have sworn the line was just short enough; I cannot count apparently)

The elaborator managed to apply it by itself in a really messed-up way, so it looked like `norm_num` was unfolding stuff badly when really it was the elaborator a few lines previously

jcommelin · 2020-12-16T14:29:46Z

That was an epic refactor. Thanks a lot! 🎉

bors merge

…5303) This PR is intended to fix the following kind of diamonds: Let `foo X` be a type with a `∀ X, has_div (foo X)` instance but no `∀ X, has_inv (foo X)`, e.g. when `foo X` is a `euclidean_domain`. Suppose we also have an instance `∀ X [cromulent X], group_with_zero (foo X)`. Then the `(/)` coming from `group_with_zero_has_div` cannot be defeq to the `(/)` coming from `foo.has_div`. As a consequence of making the `has_div` instances defeq, we can no longer assume that `(div_eq_mul_inv a b : a / b = a * b⁻¹) = rfl` for all groups. The previous preparation PR #5302 should have changed all places in mathlib that assumed defeqness, to rewrite explicitly instead. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

bors · 2020-12-16T18:35:08Z

Pull request successfully merged into master.

Build succeeded:

Vierkantor added WIP Work in progress blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Dec 10, 2020

Vierkantor force-pushed the sub_div_monoid branch 2 times, most recently from 0f9f524 to fcaa620 Compare December 10, 2020 12:40

bryangingechen mentioned this pull request Dec 10, 2020

[Merged by Bors] - chore(*): don't assume sub_eq_add_neg and div_eq_mul_inv are defeq #5302

Closed

github-actions Bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Dec 10, 2020

github-actions Bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Dec 11, 2020

Vierkantor force-pushed the sub_div_monoid branch from fcaa620 to 459c4a8 Compare December 11, 2020 22:50

github-actions Bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Dec 11, 2020

Vierkantor added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Dec 11, 2020

sgouezel 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 14, 2020

Vierkantor force-pushed the sub_div_monoid branch from 1c3a0da to cf9f89b Compare December 14, 2020 11:53

Vierkantor 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 Dec 14, 2020

eric-wieser reviewed Dec 14, 2020

View reviewed changes

Comment thread src/algebra/group/defs.lean Outdated

eric-wieser reviewed Dec 14, 2020

View reviewed changes

Comment thread src/algebra/group/defs.lean Outdated

sgouezel reviewed Dec 14, 2020

View reviewed changes

Comment thread src/algebra/group_with_zero/basic.lean Outdated

Vierkantor added 5 commits December 16, 2020 09:34

Fix overlong lines

7df1479

More sub_eq_add_neg rewriting

3a79f71

Fill in missing field so the elaborator doesn't complain about metava…

5f2ed7d

…riables

Fix analysis/hofer.lean

cbc4958

Vierkantor and others added 6 commits December 16, 2020 09:34

Fix remaining issues

93bffdf

Lint fix (missing docstring)

435345a

This line is probably not needed?

aec4b3c

Update src/algebra/group_with_zero/basic.lean

ddd7702

Explain the motivation behind div_inv_monoid

4be36ec

Fix congruence.lean

6ea8c8a

Vierkantor force-pushed the sub_div_monoid branch from 64b594f to a58e124 Compare December 16, 2020 10:32

Vierkantor added 4 commits December 16, 2020 10:32

Rename div_sub_tac -> try_refl_tac

a58e124

Fix overlong line

a21f7a1

(I could have sworn the line was just short enough; I cannot count apparently)

Can we delete the int_sub_hack?

8d83d1d

Fix missing div_eq_mul_inv

d56f39e

The elaborator managed to apply it by itself in a really messed-up way, so it looked like `norm_num` was unfolding stuff badly when really it was the elaborator a few lines previously

github-actions Bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Dec 16, 2020

bors Bot changed the title ~~chore(*): add a div/sub field to (add_)group(_with_zero)~~ [Merged by Bors] - chore(*): add a div/sub field to (add_)group(_with_zero) Dec 16, 2020

bors Bot closed this Dec 16, 2020

bors Bot deleted the sub_div_monoid branch December 16, 2020 18:35

bryangingechen mentioned this pull request Jan 2, 2021

[Merged by Bors] - feat(ring_theory/fractional_ideal): move inv to dedekind_domain #5053

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore(*): add a `div`/`sub` field to (`add_`)`group`(`_with_zero`)#5303

[Merged by Bors] - chore(*): add a `div`/`sub` field to (`add_`)`group`(`_with_zero`)#5303
Vierkantor wants to merge 15 commits into
masterfrom
sub_div_monoid

Vierkantor commented Dec 10, 2020 •

edited by bryangingechen

Loading

Uh oh!

github-actions Bot commented Dec 11, 2020

Uh oh!

Vierkantor commented Dec 11, 2020

Uh oh!

sgouezel commented Dec 14, 2020

Uh oh!

Vierkantor commented Dec 14, 2020

Uh oh!

Uh oh!

Uh oh!

sgouezel left a comment

Uh oh!

Uh oh!

Vierkantor commented Dec 14, 2020

Uh oh!

jcommelin commented Dec 16, 2020

Uh oh!

bors Bot commented Dec 16, 2020

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Conversation

Vierkantor commented Dec 10, 2020 • edited by bryangingechen Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Dec 11, 2020

Uh oh!

Vierkantor commented Dec 11, 2020

Uh oh!

sgouezel commented Dec 14, 2020

Uh oh!

Vierkantor commented Dec 14, 2020

Uh oh!

Uh oh!

Uh oh!

sgouezel left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Vierkantor commented Dec 14, 2020

Uh oh!

jcommelin commented Dec 16, 2020

Uh oh!

bors Bot commented Dec 16, 2020

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Vierkantor commented Dec 10, 2020 •

edited by bryangingechen

Loading