Zulip Chat Archive

Stream: new members

Topic: circular dependency problem

view this post on Zulip Moritz Firsching (Mar 13 2021 at 13:18):

When simplifying some bernoulli power series lemmas, I run into a dependency problem.
The pr is #6641. I have file bernoulli_polynomial.lean depending on bernoulli.lean. Some lemmas I moved from bernoulli to bernoulli_polynomial, because the new proof depends on stuff from bernoulli_polynomial. However there are some other lemmas in bernoulli, which depend on the lemmas that I moved to bernoulli_polynomial. Should I then just move all the stuff that depends on the moved lemmas to bernoulli_polynomialas well or is there a better way of doing it?

view this post on Zulip Bryan Gin-ge Chen (Mar 13 2021 at 15:24):

Yes, it looks like you'll have to move everything that depends on the moved declarations. If you anticipate that we may add a lot more to bernoulli_polynomial.lean, it may make sense to create a 3rd file specific to Bernoulli power series and stuff that depends on those definitions, and at that point we may want to create a directory number_theory/bernoulli/ and rename bernoulli.lean to bernoulli/basic.lean, etc.

view this post on Zulip Heather Macbeth (Mar 13 2021 at 18:02):

I am not an expert here, but is there a reason it's in number theory, anyway? Many kinds of polynomials get their own file in ring_theory/polynomial, see chebyshev, dickson, symmetric, soon pochhammer and bernstein. Wouldn't it make sense to put bernoulli there too?

view this post on Zulip Heather Macbeth (Mar 13 2021 at 18:03):

And the power series material could move to ring_theory/power_series.

view this post on Zulip Alex J. Best (Mar 13 2021 at 18:35):

Certainly Mazur would put them in math/bernoulli :grinning: http://people.math.harvard.edu/~mazur/papers/slides.Bartlett.pdf

view this post on Zulip Moritz Firsching (Mar 14 2021 at 12:55):

Thanks for all the hints! When trying to fix this, I noticed that I actually have a circular dependency in the proof, and this won't be resolve shifting stuff around between files..
I closed the pull request for now. When trying to simplify it I simply didn't realize that bernoulli'_odd_eq_zero (written by @Ashvni Narayanan ) actually uses the power series we were trying to simplify...

Last updated: May 06 2021 at 22:13 UTC