[Merged by Bors] - refactor(ring_theory/unique_factorization_domain): completes the refactor of `unique_factorization_domain` #4156

awainverse · 2020-09-15T00:32:00Z

Refactors unique_factorization_domain to unique_factorization_monoid
unique_factorization_monoid is a predicate
unique_factorization_monoid now requires no additive/subtractive structure

jcommelin

I haven't looked at the big file yet... will do that later.
Thanks for doing this!

src/ring_theory/discrete_valuation_ring.lean

src/ring_theory/principal_ideal_domain.lean

Vierkantor

I only looked at the big file, I will do the rest later :)

src/ring_theory/unique_factorization_domain.lean

Vierkantor · 2020-09-15T09:23:08Z

src/ring_theory/unique_factorization_domain.lean

+multiset.induction_on f
+  (λ h, (ha.1 (associated_one_iff_is_unit.1 h)).elim)
+  (λ p s _ hp hs, let ⟨u, hu⟩ := hp in ⟨p,
+    have hs0 : s = 0, from classical.by_contradiction
+      (λ hs0, let ⟨q, hq⟩ := multiset.exists_mem_of_ne_zero hs0 in
+       (hs q (by simp [hq])).2.1 $
+        (ha.2 ((p * ↑(u⁻¹)) * (s.erase q).prod) _
+          (by {rw [mul_right_comm _ _ q, mul_assoc, ← multiset.prod_cons, multiset.cons_erase hq,
+            mul_comm p _, mul_assoc, ← multiset.prod_cons, hu.symm, mul_comm, mul_assoc],
+            simp, })).resolve_left $
+              mt is_unit_of_mul_is_unit_left $ mt is_unit_of_mul_is_unit_left
+                (hs p (multiset.mem_cons_self _ _)).2.1),
+    ⟨(by {clear _let_match; simp * at *}), hs0 ▸ rfl⟩⟩)
+  (pfa.2) (pfa.1)


I expect this proof would be more readable if it's formatted in tactic-style. For example, the pfa.2 pfa.1 arguments at the end can stay with the function call if we make them the arguments to a refine call at the start.

While the proof is fresh in your mind you could even add a couple of comments saying what's going on. Christian Szegedy told me today that the machine learning people are desperate for comments in code.

I've made this a tactic proof, but I can't really say it's "fresh in my mind", because I didn't write the original and don't particularly understand it. I've added a docstring to the top because it took me a moment even to understand the statement.

src/ring_theory/unique_factorization_domain.lean

Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>

kbuzzard

This looks absolutely great to me. Many thanks for doing it!

kbuzzard · 2020-09-15T20:11:04Z

src/ring_theory/unique_factorization_domain.lean

+multiset.induction_on f
+  (λ h, (ha.1 (associated_one_iff_is_unit.1 h)).elim)
+  (λ p s _ hp hs, let ⟨u, hu⟩ := hp in ⟨p,
+    have hs0 : s = 0, from classical.by_contradiction
+      (λ hs0, let ⟨q, hq⟩ := multiset.exists_mem_of_ne_zero hs0 in
+       (hs q (by simp [hq])).2.1 $
+        (ha.2 ((p * ↑(u⁻¹)) * (s.erase q).prod) _
+          (by {rw [mul_right_comm _ _ q, mul_assoc, ← multiset.prod_cons, multiset.cons_erase hq,
+            mul_comm p _, mul_assoc, ← multiset.prod_cons, hu.symm, mul_comm, mul_assoc],
+            simp, })).resolve_left $
+              mt is_unit_of_mul_is_unit_left $ mt is_unit_of_mul_is_unit_left
+                (hs p (multiset.mem_cons_self _ _)).2.1),
+    ⟨(by {clear _let_match; simp * at *}), hs0 ▸ rfl⟩⟩)
+  (pfa.2) (pfa.1)


While the proof is fresh in your mind you could even add a couple of comments saying what's going on. Christian Szegedy told me today that the machine learning people are desperate for comments in code.

kbuzzard · 2020-09-15T20:19:14Z

Just to mention that there's this funny finiteness result polynomial.wf_dvd_monoid [integral_domain α] [wf_dvd_monoid α] : wf_dvd_monoid (polynomial α) in the UFD file. Is this also true for mv_polynomial? I think it might be.

Hey yeah I guess it's also true that if R is a UFD then so is mv_polynomial's over R with variables in an arbitrary type.

awainverse · 2020-09-16T01:55:38Z

Just to mention that there's this funny finiteness result polynomial.wf_dvd_monoid [integral_domain α] [wf_dvd_monoid α] : wf_dvd_monoid (polynomial α) in the UFD file. Is this also true for mv_polynomial? I think it might be.

Hey yeah I guess it's also true that if R is a UFD then so is mv_polynomial's over R with variables in an arbitrary type.

Yeah, this is all that's needed other than Gauss's Lemma for showing that a polynomial ring over a UFD is a UFD.
I could try making it work for mv_polynomial, but I might want to wait for another PR

Vierkantor

Thank you so much for the changes! Just a few stylistic issues and it looks good to me.

src/ring_theory/discrete_valuation_ring.lean

src/ring_theory/unique_factorization_domain.lean

Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>

scripts/nolints.txt

jcommelin

lgtm

src/ring_theory/unique_factorization_domain.lean

Co-authored-by: Johan Commelin <johan@commelin.net>

awainverse · 2020-09-21T21:23:08Z

Hopefully fixing this merge conflict doesn't break anything.

jcommelin · 2020-09-22T06:16:25Z

Thanks 🎉

bors merge

…ctor of `unique_factorization_domain` (#4156) Refactors `unique_factorization_domain` to `unique_factorization_monoid` `unique_factorization_monoid` is a predicate `unique_factorization_monoid` now requires no additive/subtractive structure Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>

bors · 2020-09-22T08:04:22Z

Pull request successfully merged into master.

Build succeeded:

awainverse added 4 commits September 7, 2020 21:23

init

23776cd

Moving through factor_set

5d52442

Whew

a50c45d

Linting

86625b9

awainverse added the awaiting-review The author would like community review of the PR label Sep 15, 2020

jcommelin requested review from Vierkantor and kbuzzard September 15, 2020 05:46

jcommelin reviewed Sep 15, 2020

View reviewed changes

src/ring_theory/discrete_valuation_ring.lean Show resolved Hide resolved

src/ring_theory/principal_ideal_domain.lean Outdated Show resolved Hide resolved

Vierkantor requested changes Sep 15, 2020

View reviewed changes

awainverse and others added 2 commits September 15, 2020 12:32

Easy reviews

36a845f

Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>

typo fix

cacbd20

kbuzzard reviewed Sep 15, 2020

View reviewed changes

More reviews

272344d

awainverse 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 Sep 15, 2020

prime_of_factor etc.

6d9aee3

awainverse 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 Sep 16, 2020

Flipping exists_factors

d76b165

Vierkantor approved these changes Sep 16, 2020

View reviewed changes

Stylistic Reviews

465dd16

Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>

bryangingechen reviewed Sep 16, 2020

View reviewed changes

scripts/nolints.txt Outdated Show resolved Hide resolved

nolint reversion

682dda6

Vierkantor requested a review from jcommelin September 18, 2020 11:51

jcommelin reviewed Sep 19, 2020

View reviewed changes

src/ring_theory/unique_factorization_domain.lean Outdated Show resolved Hide resolved

Update src/ring_theory/unique_factorization_domain.lean

69b9636

Co-authored-by: Johan Commelin <johan@commelin.net>

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

Merge remote-tracking branch 'origin/master' into ufmonoid

fc11998

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

awainverse added 2 commits September 21, 2020 15:56

Fixing merge fix

c6ebb18

Liiiiiiiiiiiiiiiiiiint

22529cf

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 Sep 22, 2020

bors bot changed the title ~~refactor(ring_theory/unique_factorization_domain): completes the refactor of unique_factorization_domain~~ [Merged by Bors] - refactor(ring_theory/unique_factorization_domain): completes the refactor of unique_factorization_domain Sep 22, 2020

bors bot closed this Sep 22, 2020

bors bot deleted the ufmonoid branch September 22, 2020 08:04

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(ring_theory/unique_factorization_domain): completes the refactor of `unique_factorization_domain` #4156

[Merged by Bors] - refactor(ring_theory/unique_factorization_domain): completes the refactor of `unique_factorization_domain` #4156

awainverse commented Sep 15, 2020

jcommelin left a comment

Vierkantor left a comment

Vierkantor Sep 15, 2020

kbuzzard Sep 15, 2020

awainverse Sep 15, 2020

kbuzzard left a comment

kbuzzard Sep 15, 2020

kbuzzard commented Sep 15, 2020 •

edited

Loading

awainverse commented Sep 16, 2020

Vierkantor left a comment

jcommelin left a comment

awainverse commented Sep 21, 2020

jcommelin commented Sep 22, 2020

bors bot commented Sep 22, 2020

[Merged by Bors] - refactor(ring_theory/unique_factorization_domain): completes the refactor of unique_factorization_domain #4156

[Merged by Bors] - refactor(ring_theory/unique_factorization_domain): completes the refactor of unique_factorization_domain #4156

Conversation

awainverse commented Sep 15, 2020

jcommelin left a comment

Choose a reason for hiding this comment

Vierkantor left a comment

Choose a reason for hiding this comment

Vierkantor Sep 15, 2020

Choose a reason for hiding this comment

kbuzzard Sep 15, 2020

Choose a reason for hiding this comment

awainverse Sep 15, 2020

Choose a reason for hiding this comment

kbuzzard left a comment

Choose a reason for hiding this comment

kbuzzard Sep 15, 2020

Choose a reason for hiding this comment

kbuzzard commented Sep 15, 2020 • edited Loading

awainverse commented Sep 16, 2020

Vierkantor left a comment

Choose a reason for hiding this comment

jcommelin left a comment

Choose a reason for hiding this comment

awainverse commented Sep 21, 2020

jcommelin commented Sep 22, 2020

bors bot commented Sep 22, 2020

[Merged by Bors] - refactor(ring_theory/unique_factorization_domain): completes the refactor of `unique_factorization_domain` #4156

[Merged by Bors] - refactor(ring_theory/unique_factorization_domain): completes the refactor of `unique_factorization_domain` #4156

kbuzzard commented Sep 15, 2020 •

edited

Loading