normalize

Stream: general

[Kenny Lau]

Ok this situation is quite complicated here and I'm not sure I understand the whole situation (an import graph would be quite beneficial).

So I look at algebra/gcd_domain.lean and think to myself: I should define normalize x to replace x * norm_unit x since that expression is used a lot and should have a name and is actually the whole point of normalization_domain (we don't really care about the unit it multiplies by, right?).

But this would require lemmas from ring_theory/associated.lean about units and dvd.

Unfortunately, it imports data/int/gcd.lean which imports algebra.gcd_domain, and this is an essential import in the sense that a majority of the file is based on this import.

However, data/int/gcd.lean is not an essential import of ring_theory/associated.lean, in the sense that < 10% of the file breaks when I remove that import. Things that break include three theorems which is essentially examples about int and nat, and also a section below about normalization domain.

[Kenny Lau]

So my proposal is:

1. remove the import data/int/gcd.lean from ring_theory/associated.lean
2. move ring_theory/associated.lean to algebra/associated.lean
3. add the import algebra/associated.lean to algebra/gcd_domain.lean
4. add normalize in algebra/gcd_domain.lean
5. move the three theorems that break to data/int/gcd.lean
6. move the section that breaks to algebra/gcd_domain.lean

[Kenny Lau]

@Mario Carneiro do you think this is a good idea? did I miss anything?

[Mario Carneiro]

why does int.gcd use algebra.normalization_domain?

[Kenny Lau]

There is no algebra.normalization_domain: it is just algebra.gcd_domain.

[Kenny Lau]

And that uses that because the whole file is about gcd

[Mario Carneiro]

nat.gcd doesn't

[Kenny Lau]

because nat isn't a gcd_domain

[Kenny Lau]

I suppose we can remove the normalization_domain and gcd_domain sections of data/int/gcd.lean and move them to algebra/gcd_domain.lean?

[Kenny Lau]

What do you think?

[Kenny Lau]

afterall there's a proof that int is euclidean_domain in algebra/euclidean_domain.lean anyway, so this wouldn't be unprecedented

[Mario Carneiro]

my guess is that you can do integer gcd by reference to nat gcd, without bringing in the abstract algebra. But setting that aside, I think that moving ring_theory.associated to algebra is okay for much of it, but not all; you will probably need to split the file

[Kenny Lau]

Ok I'll experiment on a branch

[Mario Carneiro]

I think that data.int.gcd shouldn't bring in anything from ring_theory

[Kenny Lau]

I agree

[Kenny Lau]

@Mario Carneiro so where should these theorems go?

theorem irreducible_iff_nat_prime : ∀(a : ℕ), irreducible a ↔ nat.prime a
lemma nat.prime_iff_prime {p : ℕ} : p.prime ↔ _root_.prime (p : ℕ) :=
lemma nat.prime_iff_prime_int {p : ℕ} : p.prime ↔ _root_.prime (p : ℤ) :=
def associates_int_equiv_nat : (associates ℤ) ≃ ℕ :=

[Kenny Lau]

https://github.com/leanprover-community/mathlib/blob/normalize/src/pending/default.lean

[Kevin Buzzard]

Can one break up file X.lean into X_part_1.lean and X_part_2.lean and then just change X.lean into import X_part_1.lean import X_part_2.lean, and then you have more breathing space to fiddle with imports?

[Kenny Lau]

@Mario Carneiro what do you think about #668?

[Mario Carneiro]

what chris said - summary?

[Kenny Lau]

it's in this zulip thread

[Mario Carneiro]

some definitions changed?

[Simon Hudon]

I would chime in and say a Zulip thread is not a summary. It's useful for reference but you should be able to get the gist of the PR without looking at Zulip

[Kenny Lau]

done @Mario Carneiro

[Chris Hughes]

I think a good rule in future might be that moving stuff around should be in a separate PR from adding any new code, to make review easier.

[Kenny Lau]

agreed

[Kenny Lau]

I'll be careful about that in the future