polynomial refactor

Stream: maths

[Jalex Stark]

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

[Jalex Stark]

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

[Scott Morrison]

great. small files are good

[Jalex Stark]

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

[Scott Morrison]

is that the current branch?

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Scott Morrison]

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

[Jalex Stark]

oops

[Jalex Stark]

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

[Jalex Stark]

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}

[Jalex Stark]

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

[Johan Commelin]

Thank you so much for doing this

[Jalex Stark]

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

[Jalex Stark]

is rec_on_hornera programming thing? docs#polynomial.rec_on_horner

[Johan Commelin]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

oh okay

[Jalex Stark]

it is a Sort-valued induction

[Jalex Stark]

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

[Johan Commelin]

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

[Jalex Stark]

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

[Johan Commelin]

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

[Jalex Stark]

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

[Kyle Miller]

I didn't know it was called that, but I remember learning about the $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.

[Jalex Stark]

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

[Johan Commelin]

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

[Johan Commelin]

After tomorrow I would be able to help

[Jalex Stark]

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

[Jalex Stark]

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

[Johan Commelin]

Oooh, that shouldn't happen

[Johan Commelin]

Please use coeff n p instead of p.to_fun n

[Jalex Stark]

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

[Johan Commelin]

Ouch

[Jalex Stark]

it builds

[Jalex Stark]

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

[Johan Commelin]

Thank you so so much!

[Johan Commelin]

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

[Jalex Stark]

what do we need to check before merging?

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

Monday it would be top of my list.

[Jalex Stark]

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

[Johan Commelin]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Johan Commelin]

Jalex Stark said:

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

Sounds like you are not on the master branch

[Jalex Stark]

ah, i just figured it out

[Jalex Stark]

i was using too small numbers

[Johan Commelin]

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

[Jalex Stark]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Jalex Stark]

oh i see

[Johan Commelin]

Is it Kenny's commit I linked above?

[Scott Morrison]

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.

[Scott Morrison]

We definitely don't want that.

[Scott Morrison]

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.

[Scott Morrison]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Patrick Stevens]

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