Stream: PR reviews

Topic: polynomial.eval2_smul

Bolton Bailey (Feb 01 2021 at 04:40):

Looking at the code for polynomial.eval2_smul

@[simp] lemma eval₂_smul (g : R →+* S) (p : polynomial R) (x : S) {s : R} :
eval₂ g x (s • p) = g s • eval₂ g x p :=
begin
simp only [eval₂, sum_smul_index, forall_const, zero_mul, g.map_zero, g.map_mul, mul_assoc],
-- Why doesn't rw [←finsupp.mul_sum] work?
convert (@finsupp.mul_sum _ _ _ _ _ (g s) p (λ i a, (g a * x ^ i))).symm,
end


Shouldn't the lemma be

@[simp] lemma eval₂_smul (g : R →+* S) (p : polynomial R) (x : S) {s : R} :
eval₂ g x (s • p) = g s * eval₂ g x p :=
...


As both g s and eval₂ g x p are in S

Bolton Bailey (Feb 01 2021 at 04:51):

Similar thing with polynomial.eval_smul

Johan Commelin (Feb 01 2021 at 05:49):

@Bolton Bailey (Aside: is this part of an existing PR? If so, you can write #1234 in the title of the thread, and it will create a link to PR 1234.)

I think the reason for using \bu in both places is for some sort of "regularity" in the operations on both sides. But maybe in practice using * on the RHS would be better. I don't have a strong opinion.

Bolton Bailey (Feb 01 2021 at 05:57):

It's not part of an existing PR, I was going to test the air here before writing one.
After wondering for a few days why the Infoview in my project was showing a coercion operation when I didn't think there should be one it seems like this is the reason. With that in mind, I think that the * is more natural, but I'll try to figure out if changing it fixes the issue.

Johan Commelin (Feb 01 2021 at 06:03):

Aha, but then you should probably use a different stream. (Not too big of an issue.) We try to use this stream only for discussion about explicit PRs. (See the other thread titles, they all have the format #1234 pr name.

Johan Commelin (Feb 01 2021 at 06:03):

But where is the coercion? Because there shouldn't be a coercion either.

Bolton Bailey (Feb 01 2021 at 08:42):

Thanks, in the future I'll open a PR before posting, and I'll make a PR for this as soon as I have time.

Here's a MWE of my case, where I am trying to reason about a polynomial that has been converted to a mv_polynomial using eval_2.

import data.polynomial.basic
import data.mv_polynomial.basic

section

universe u

parameter {S : Type}
parameter {F : Type u}
parameter [field F]

lemma foo (s : S) (i : F) (p : polynomial F) : polynomial.eval₂ mv_polynomial.C (mv_polynomial.X s) (i • p) = i • polynomial.eval₂ mv_polynomial.C (mv_polynomial.X s) (p) :=
begin
rw polynomial.eval₂_smul,
-- ⇑mv_polynomial.C i • polynomial.eval₂ mv_polynomial.C (mv_polynomial.X s) p =
-- i • polynomial.eval₂ mv_polynomial.C (mv_polynomial.X s) p
end

end


Eric Wieser (Feb 01 2021 at 08:44):

Where's the coercion?

Johan Commelin (Feb 01 2021 at 08:44):

Well, we enjoy discussions before PRs as well (-; But we put them in #general or #maths . (But no worries... it's not a big deal. I was just confused about whether I missed a PR that you were talking about.)

Eric Wieser (Feb 01 2021 at 08:45):

Are you talking about the function coercion right at the start? That's just how bundled functions work, and nothing to do with this lemma

Eric Wieser (Feb 01 2021 at 08:45):

Presumably a zulip admin can move this thread

Bolton Bailey (Feb 01 2021 at 09:03):

If that's how bundled functions look that's fine, but it's a bit surprising since nowhere in the code I write myself do I have to put ⇑ before mv_polynomial.C when calling it as a function.

It still seems to me that it should be * in the lemma - the \smul is on the left hand side because it has to be, but an smul on the right hand side is not what I expected. You can see the original author was confused as to why they couldn't use rw [←finsupp.mul_sum] - this indeed closes the lemma in the * version.

Last updated: May 06 2021 at 11:23 UTC