## Stream: new members

### Topic: Eval of constant polynomial

#### Patrick Lutz (Jul 12 2020 at 01:29):

For some reason, I'm having a hard time figuring out how to evaluate a constant polynomial. I can do it in some situations, e.g. the following works

import data.polynomial data.real.basic
example : eval 5 (C 2 : polynomial ℝ) = 2 :=
begin
rw eval_C,
end


but the following does not

example : eval 5 (2 : polynomial ℝ) = 2 :=
begin
rw eval_C,
end


Instead, Lean complains that it didn't find an instance of the pattern eval ?m_3 (C ?m_4). Also, things like change (2 : polynomial ℝ) with (C 2 : polynomial ℝ), don't work and hint and library_search have no suggestions. Also,

#eval eval 5 (2 : polynomial ℚ)


doesn't work and, to my surprise, tells me that code generation failed, VM does not have code for 'classical.choice'. What is going on here? Does (2 : polynomial ℝ) not mean what I think it does?

#### Mario Carneiro (Jul 12 2020 at 01:45):

Does simp work?

#### Mario Carneiro (Jul 12 2020 at 01:45):

There should be enough rules to prove C 2 = 2

#### Patrick Lutz (Jul 12 2020 at 01:47):

no, simp doesn't work

#### Patrick Lutz (Jul 12 2020 at 01:48):

For reference, simp also can't prove this

example : eval 5 (2 : polynomial ℝ) = eval 5 (C 2 : polynomial ℝ) := sorry


#### Mario Carneiro (Jul 12 2020 at 01:56):

import data.polynomial data.real.basic

namespace polynomial
variables {R : Type*} [semiring R] {a : R}

@[simp] lemma C_bit0 : C (bit0 a) = bit0 (C a) := C_add
@[simp] lemma C_bit1 : C (bit1 a) = bit1 (C a) := by simp [bit1, C_bit0]

end polynomial

open polynomial
example : eval 5 (2 : polynomial ℝ) = 2 :=
by rw [← show C (2 : ℝ) = 2, by simp, eval_C]


#### Scott Morrison (Jul 12 2020 at 02:02):

@Patrick Lutz, feel like making a PR to add those two simp lemmas to data.polynomial? :-)

#### Patrick Lutz (Jul 12 2020 at 02:04):

@Mario Carneiro Okay, that works (after changing semiring R to comm_semiring R). Is this what's going on: (2 : polynomial \R) is really something like C 1 + C 1 which is not definitionally equal to C (1 + 1)?

#### Patrick Lutz (Jul 12 2020 at 02:04):

Scott Morrison said:

Patrick Lutz, feel like making a PR to add those two simp lemmas to data.polynomial? :-)

Sure, I can do that.

#### Scott Morrison (Jul 12 2020 at 02:06):

Huh, why did you need to change to comm_semiring? Surely those bitX lemmas are true generally.

#### Patrick Lutz (Jul 12 2020 at 02:07):

I don't know, but when it was just what Mario wrote I got this error message:

failed to synthesize type class instance for
R : Type u_1,
_inst_1 : semiring R,
a : R
⊢ comm_semiring R


#### Patrick Lutz (Jul 12 2020 at 02:07):

and the error appeared everywhere C was written

#### Mario Carneiro (Jul 12 2020 at 02:09):

Maybe you have an old mathlib?

#### Patrick Lutz (Jul 12 2020 at 02:11):

I just tried running leanproject up and the error is still there when I use semiring instead of comm_semiring

#### Patrick Lutz (Jul 12 2020 at 02:13):

Oh wait, nevermind. It went away after I restarted VSCode

#### Patrick Lutz (Jul 12 2020 at 03:07):

Scott Morrison said:

Patrick Lutz, feel like making a PR to add those two simp lemmas to data.polynomial? :-)

Should I ask for write access to mathlib to push to a branch and pull request from there or should I fork the mathlib repo?

#### Scott Morrison (Jul 12 2020 at 03:48):

I'll count that as asking for write access; I've sent you an invitation. (to your berkeley email)

#### Yury G. Kudryashov (Jul 12 2020 at 05:51):

We should also have lemmas like eval x (bit0 p) = bit0 (eval x p), and similarly for bit1, 0, and 1.

#### Yury G. Kudryashov (Jul 12 2020 at 05:51):

These lemmas would simp the original goal.

#### Patrick Lutz (Jul 12 2020 at 08:29):

Yury G. Kudryashov said:

We should also have lemmas like eval x (bit0 p) = bit0 (eval x p), and similarly for bit1, 0, and 1.

I added the first two of those, but it looks like eval_one and eval_zero already exist.

#### Patrick Lutz (Jul 12 2020 at 08:29):

@Scott Morrison I've now made the PR.

#### Scott Morrison (Jul 12 2020 at 08:52):

I'll have a look!

#### Scott Morrison (Jul 12 2020 at 08:53):

there are some strange rules about titles of PRs (because these become the commit message in our git history when we squash all the commits from the PR into a single commit)

#### Scott Morrison (Jul 12 2020 at 08:54):

this one should probably be feat(data/polynomial): simp lemmas for bit0 / bit1

#### Scott Morrison (Jul 12 2020 at 08:57):

Other than that, looks great! For bigger PRs, it's good to add the label request-review once you've seen that the CI checks have succeeded, to get someone's attention. (They'll then mark it changes-requested after making comments, you'll change it back, etc. etc..)

#### Scott Morrison (Jul 12 2020 at 08:57):

For this one, I think we're good to go!

Last updated: Dec 20 2023 at 11:08 UTC