Zulip Chat Archive

Stream: general

Topic: normalize


view this post on Zulip Kenny Lau (Feb 01 2019 at 12:21):

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.

view this post on Zulip Kenny Lau (Feb 01 2019 at 12:21):

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

view this post on Zulip Kenny Lau (Feb 01 2019 at 12:21):

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

view this post on Zulip Mario Carneiro (Feb 01 2019 at 12:23):

why does int.gcd use algebra.normalization_domain?

view this post on Zulip Kenny Lau (Feb 01 2019 at 12:24):

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

view this post on Zulip Kenny Lau (Feb 01 2019 at 12:24):

And that uses that because the whole file is about gcd

view this post on Zulip Mario Carneiro (Feb 01 2019 at 12:24):

nat.gcd doesn't

view this post on Zulip Kenny Lau (Feb 01 2019 at 12:24):

because nat isn't a gcd_domain

view this post on Zulip Kenny Lau (Feb 01 2019 at 12:27):

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?

view this post on Zulip Kenny Lau (Feb 01 2019 at 12:27):

What do you think?

view this post on Zulip Kenny Lau (Feb 01 2019 at 12:27):

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

view this post on Zulip Mario Carneiro (Feb 01 2019 at 12:28):

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

view this post on Zulip Kenny Lau (Feb 01 2019 at 12:29):

Ok I'll experiment on a branch

view this post on Zulip Mario Carneiro (Feb 01 2019 at 12:30):

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

view this post on Zulip Kenny Lau (Feb 01 2019 at 12:31):

I agree

view this post on Zulip Kenny Lau (Feb 01 2019 at 13:08):

@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 )   :=

view this post on Zulip Kenny Lau (Feb 01 2019 at 13:12):

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

view this post on Zulip Kevin Buzzard (Feb 01 2019 at 14:59):

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?

view this post on Zulip Kenny Lau (Feb 09 2019 at 21:55):

@Mario Carneiro what do you think about #668?

view this post on Zulip Mario Carneiro (Feb 09 2019 at 21:57):

what chris said - summary?

view this post on Zulip Kenny Lau (Feb 09 2019 at 22:02):

it's in this zulip thread

view this post on Zulip Mario Carneiro (Feb 09 2019 at 22:03):

some definitions changed?

view this post on Zulip Simon Hudon (Feb 09 2019 at 22:17):

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

view this post on Zulip Kenny Lau (Feb 09 2019 at 22:17):

done @Mario Carneiro

view this post on Zulip Chris Hughes (Feb 09 2019 at 22:46):

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.

view this post on Zulip Kenny Lau (Feb 09 2019 at 22:47):

agreed

view this post on Zulip Kenny Lau (Feb 09 2019 at 22:47):

I'll be careful about that in the future


Last updated: May 18 2021 at 17:44 UTC