## Stream: maths

### Topic: polynomial refactor

#### 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
• find homes for the last 200 lines of code in data/polynomial/misc.lean

#### 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

#### Scott Morrison (Jul 15 2020 at 14:55):

great. small files are good

#### Scott Morrison (Jul 15 2020 at 15:03):

is that the current branch?

#### Jalex Stark (Jul 15 2020 at 15:03):

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

#### 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


#### 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

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

#### 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

oops

#### 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

#### 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}

#### 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

#### Johan Commelin (Jul 15 2020 at 17:14):

Thank you so much for doing this

#### 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

#### Jalex Stark (Jul 15 2020 at 17:41):

is rec_on_hornera programming thing? docs#polynomial.rec_on_horner

#### Johan Commelin (Jul 15 2020 at 17:42):

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

#### 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

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

oh okay

#### Jalex Stark (Jul 15 2020 at 17:44):

it is a Sort-valued induction

#### 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

#### 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

#### Jalex Stark (Jul 15 2020 at 17:47):

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

#### Johan Commelin (Jul 15 2020 at 17:47):

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

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

#### Kyle Miller (Jul 15 2020 at 18:03):

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

#### Johan Commelin (Jul 15 2020 at 18:10):

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

#### Johan Commelin (Jul 15 2020 at 18:10):

After tomorrow I would be able to help

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

#### 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

#### Johan Commelin (Jul 15 2020 at 18:32):

Oooh, that shouldn't happen

#### Johan Commelin (Jul 15 2020 at 18:32):

Please use coeff n p instead of p.to_fun n

#### Jalex Stark (Jul 15 2020 at 18:42):

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

Ouch

it builds

#### Jalex Stark (Jul 15 2020 at 21:01):

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

#### Johan Commelin (Jul 16 2020 at 03:04):

Thank you so so much!

#### Johan Commelin (Jul 16 2020 at 03:04):

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

#### Jalex Stark (Jul 16 2020 at 03:13):

what do we need to check before merging?

#### 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.

#### 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.

#### Johan Commelin (Jul 16 2020 at 03:18):

Monday it would be top of my list.

#### 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

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

#### Jalex Stark (Jul 16 2020 at 03:41):

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

#### Jalex Stark (Jul 16 2020 at 03:43):

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

#### Johan Commelin (Jul 16 2020 at 03:46):

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

#### Johan Commelin (Jul 16 2020 at 03:46):

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

#### Jalex Stark (Jul 16 2020 at 03:47):

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

#### Jalex Stark (Jul 16 2020 at 03:47):

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

#### Jalex Stark (Jul 16 2020 at 03:49):

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

#### Jalex Stark (Jul 16 2020 at 03:49):

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

#### 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

#### Jalex Stark (Jul 16 2020 at 03:54):

ah, i just figured it out

#### Jalex Stark (Jul 16 2020 at 03:54):

i was using too small numbers

#### Johan Commelin (Jul 16 2020 at 03:54):

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

#### Jalex Stark (Jul 16 2020 at 03:54):

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

#### Johan Commelin (Jul 16 2020 at 03:54):

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

#### Johan Commelin (Jul 16 2020 at 03:54):

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

oh i see

#### Johan Commelin (Jul 16 2020 at 03:55):

Is it Kenny's commit I linked above?

#### 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.

#### Scott Morrison (Jul 16 2020 at 03:55):

We definitely don't want that.

#### 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.

#### Scott Morrison (Jul 16 2020 at 03:56):

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

#### 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

#### Jalex Stark (Jul 16 2020 at 03:57):

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

#### Jalex Stark (Jul 16 2020 at 03:58):

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

#### Jalex Stark (Jul 16 2020 at 04:05):

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

#### 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