Zulip Chat Archive

Stream: maths

Topic: polynomial refactor


view this post on Zulip Jalex Stark (Jul 15 2020 at 14:50):

I split data/polynomial.lean into several files on the branch mathlib:polynomial_refactor. I'm currently working on

  • fix some proofs that broke during the shuffle
  • add module docstrings
  • find homes for the last 200 lines of code in data/polynomial/misc.lean

view this post on Zulip Jalex Stark (Jul 15 2020 at 14:52):

currently several means, uh, 15. one optimization i'm not yet attempting is to reduce the height of the import DAG. i think some of the content will end up in ring_theory and/or field_theory, though I think most of it should go to algebra/polynomial

view this post on Zulip Scott Morrison (Jul 15 2020 at 14:55):

great. small files are good

view this post on Zulip Jalex Stark (Jul 15 2020 at 15:02):

i am very confused about this broken proof:
https://github.com/leanprover-community/mathlib/compare/polynomial_refactor#diff-ad4dee56670fd030e11668e3244f9379R123-R126

view this post on Zulip Scott Morrison (Jul 15 2020 at 15:03):

is that the current branch?

view this post on Zulip Jalex Stark (Jul 15 2020 at 15:03):

oh i guess that link doesn't do what I thought it did

view this post on Zulip Jalex Stark (Jul 15 2020 at 15:04):

lemma eval₂_comp [comm_semiring S] (f : R →+* S) {x : S} :
  (p.comp q).eval₂ f x = p.eval₂ f (q.eval₂ f x) := sorry
--   show (p.sum (λ e a, C a * q ^ e)).eval₂ f x = p.eval₂ f (eval₂ f x q),
-- by simp only [eval₂_mul, eval₂_C, eval₂_pow, eval₂_sum]; refl

view this post on Zulip Jalex Stark (Jul 15 2020 at 15:05):

the old proof is commented out. all of the lemmas used in the simp only have been proven and their statements haven't changed, but now it doesn't close the goal

view this post on Zulip Jalex Stark (Jul 15 2020 at 15:07):

oh I maybe have the wrong set of comm_semiring hypotheses (nope, I have them for both R and S)

view this post on Zulip Scott Morrison (Jul 15 2020 at 15:12):

gah, I have a local branch also called polynomial_refactor, which I'll have to move before I can check out yours

view this post on Zulip Jalex Stark (Jul 15 2020 at 15:13):

oops

view this post on Zulip Jalex Stark (Jul 15 2020 at 15:26):

i'm going to open it as a WIP PR; that will make it easier to discuss specific pieces of code

view this post on Zulip Jalex Stark (Jul 15 2020 at 16:16):

aha! there are some places where I proved something about {p q : polynomial R} when they used to be proven for {q : polynomial R} {q : polynomial S}

view this post on Zulip Jalex Stark (Jul 15 2020 at 17:13):

fixed all the sorries. thinking about docstrings, while waiting for CI to tell me which things I broke outside of data/poynomial with my changes

view this post on Zulip Johan Commelin (Jul 15 2020 at 17:14):

Thank you so much for doing this

view this post on Zulip Jalex Stark (Jul 15 2020 at 17:15):

I'm glad I have this community to teach me how to contribute to a large software project

view this post on Zulip Jalex Stark (Jul 15 2020 at 17:41):

is rec_on_hornera programming thing? docs#polynomial.rec_on_horner

view this post on Zulip Johan Commelin (Jul 15 2020 at 17:42):

Not really... just a "programming name" (-;

view this post on Zulip Jalex Stark (Jul 15 2020 at 17:42):

i think i've heard "horner normal form" before, maybe if i stare at this anothe rminute i'll see why it's a normal form

view this post on Zulip Jalex Stark (Jul 15 2020 at 17:43):

(it is a def without a docstring. i'm not sure why it's not a lemma instead)

view this post on Zulip Jalex Stark (Jul 15 2020 at 17:44):

oh okay

view this post on Zulip Jalex Stark (Jul 15 2020 at 17:44):

it is a Sort-valued induction

view this post on Zulip Jalex Stark (Jul 15 2020 at 17:44):

i don't know why you need that other than for programming, but I will now try to write a dosctring

view this post on Zulip Johan Commelin (Jul 15 2020 at 17:45):

It could be that for a particular proof this is the kind of induction strategy that works well

view this post on Zulip Jalex Stark (Jul 15 2020 at 17:47):

but if you're just proving something then you wouldn't mind being Prop-valued?

view this post on Zulip Johan Commelin (Jul 15 2020 at 17:47):

Sure... but it also works for definitions. Although I can't think of a use-case...

view this post on Zulip Jalex Stark (Jul 15 2020 at 17:48):

(to be clear, I'm not definitely not arguing to change the definition; i'm just trying to understand what its docstring should be)

view this post on Zulip Kyle Miller (Jul 15 2020 at 18:03):

I didn't know it was called that, but I remember learning about the a0+X(a1+X(a2+X()))a_0+X(a_1+X(a_2+X(\dots))) form for polynomials in high school algebra. As far as I know, it's mostly useful for computation, since it saves you from calculating all those powers. Though, I guess rec_on_horner is essentially induction on the coefficient list with two operations: insert 0 at the beginning, or replace a 0 at the beginning with a non-zero constant, which seems relatively easy to work with.

view this post on Zulip Jalex Stark (Jul 15 2020 at 18:08):

oof, I broke a proof in polynomial_algebra.lean, which suggests that I've changed the behavior of the polynomial simp set :(

view this post on Zulip Johan Commelin (Jul 15 2020 at 18:10):

Ooo.oo... I'm sorry for you

view this post on Zulip Johan Commelin (Jul 15 2020 at 18:10):

After tomorrow I would be able to help

view this post on Zulip Jalex Stark (Jul 15 2020 at 18:11):

I'm feeling good about pushing forward and trying to get to the bottom of things myself; hopefully by the time you have time to think about it the remaining questions will be big-picture design stuff :)

view this post on Zulip Jalex Stark (Jul 15 2020 at 18:22):

i think my problems are with apply_eq_coeff in particular. I've had to write p.to_fun a lot

view this post on Zulip Johan Commelin (Jul 15 2020 at 18:32):

Oooh, that shouldn't happen

view this post on Zulip Johan Commelin (Jul 15 2020 at 18:32):

Please use coeff n p instead of p.to_fun n

view this post on Zulip Jalex Stark (Jul 15 2020 at 18:42):

in at least one case, the to_fun is coming from finsupp.mem_support_iff

view this post on Zulip Johan Commelin (Jul 15 2020 at 18:45):

Ouch

view this post on Zulip Jalex Stark (Jul 15 2020 at 20:59):

it builds

view this post on Zulip Jalex Stark (Jul 15 2020 at 21:01):

there are a lot of module docstrings which want to be elaborated

view this post on Zulip Johan Commelin (Jul 16 2020 at 03:04):

Thank you so so much!

view this post on Zulip Johan Commelin (Jul 16 2020 at 03:04):

I think you shouldn't feel burdened by more documentation. That can be done later.

view this post on Zulip Jalex Stark (Jul 16 2020 at 03:13):

what do we need to check before merging?

view this post on Zulip Johan Commelin (Jul 16 2020 at 03:17):

Did you fix the conflict already? Otherwise we have to wait a bit for someone to do that.

view this post on Zulip Johan Commelin (Jul 16 2020 at 03:18):

I don't think I can review this today, maybe tomorrow. And this weekend I'll take a healthy break away from my screen.

view this post on Zulip Johan Commelin (Jul 16 2020 at 03:18):

Monday it would be top of my list.

view this post on Zulip Jalex Stark (Jul 16 2020 at 03:30):

i think i need to figure out what changed in data/polynomial.lean in master and then distribute those changes into the current file structure

view this post on Zulip Johan Commelin (Jul 16 2020 at 03:31):

Maybe git diff HEAD~5 HEAD -- src/data/polynomial.lean can help (and tweak the 5 a bit)

view this post on Zulip Jalex Stark (Jul 16 2020 at 03:41):

running that command gives me no output, including with 5 \to 1 and 5 \to 10

view this post on Zulip Jalex Stark (Jul 16 2020 at 03:43):

i'll try using the github ui to look at commits

view this post on Zulip Johan Commelin (Jul 16 2020 at 03:46):

@Jalex Stark Did you git pull on the master branch?

view this post on Zulip Johan Commelin (Jul 16 2020 at 03:46):

Maybe you didn't have the conflicting changes yet, since they are probably quite new

view this post on Zulip Jalex Stark (Jul 16 2020 at 03:47):

I did git fetch and git merge origin master and have not made a merge commit

view this post on Zulip Jalex Stark (Jul 16 2020 at 03:47):

i guess if i make a merge commit that keeps the file, your method will work

view this post on Zulip Jalex Stark (Jul 16 2020 at 03:49):

agh i just get the trivial diff of adding the whole file

view this post on Zulip Jalex Stark (Jul 16 2020 at 03:49):

but now I guess both files live on my machine and I could diff them manually

view this post on Zulip Johan Commelin (Jul 16 2020 at 03:53):

Jalex Stark said:

agh i just get the trivial diff of adding the whole file

Sounds like you are not on the master branch

view this post on Zulip Jalex Stark (Jul 16 2020 at 03:54):

ah, i just figured it out

view this post on Zulip Jalex Stark (Jul 16 2020 at 03:54):

i was using too small numbers

view this post on Zulip Johan Commelin (Jul 16 2020 at 03:54):

https://github.com/leanprover-community/mathlib/commit/58dde5b8fe3778d11b8e4d936a7b98fb790ea085

view this post on Zulip Jalex Stark (Jul 16 2020 at 03:54):

if i go back 50 commits, then that's before I deleted the file

view this post on Zulip Johan Commelin (Jul 16 2020 at 03:54):

Right, but master doesn't know about those 50 commits

view this post on Zulip Johan Commelin (Jul 16 2020 at 03:54):

Hence, on the master branch, I guess you could use small numbers

view this post on Zulip Jalex Stark (Jul 16 2020 at 03:55):

oh i see

view this post on Zulip Johan Commelin (Jul 16 2020 at 03:55):

Is it Kenny's commit I linked above?

view this post on Zulip Scott Morrison (Jul 16 2020 at 03:55):

I won't be able to look at this until at least tomorrow, but I did see this thing above about having to use p.to_fun in places.

view this post on Zulip Scott Morrison (Jul 16 2020 at 03:55):

We definitely don't want that.

view this post on Zulip Scott Morrison (Jul 16 2020 at 03:55):

In fact, a thorough refactor of polynomial is probably going to want to make polynomial @[irreducible] as early as possible, so it's not even possible to convert it to a function.

view this post on Zulip Scott Morrison (Jul 16 2020 at 03:56):

(i.e. coeff will be the only option)

view this post on Zulip Jalex Stark (Jul 16 2020 at 03:56):

yes, the problem was that we accidentally went the other direction, making a global instance of coe_to_fn

view this post on Zulip Jalex Stark (Jul 16 2020 at 03:57):

once we got rid of the bad instance we stopped having the problem

view this post on Zulip Jalex Stark (Jul 16 2020 at 03:58):

i'll work on merging kenny's tensor product commit

view this post on Zulip Jalex Stark (Jul 16 2020 at 04:05):

ah, great, the only change to polynomial.lean was a deletion of one instance

view this post on Zulip Patrick Stevens (Jul 16 2020 at 05:43):

git log -p filename will give you the complete history of a file, expressed as a series of patches - sounds like it might have been helpful


Last updated: May 11 2021 at 15:12 UTC