Eval of constant polynomial

Stream: new members

[Patrick Lutz]

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]

Does simp work?

[Mario Carneiro]

There should be enough rules to prove C 2 = 2

[Patrick Lutz]

no, simp doesn't work

[Patrick Lutz]

For reference, simp also can't prove this

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

[Mario Carneiro]

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]

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

[Patrick Lutz]

@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]

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]

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

[Patrick Lutz]

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]

and the error appeared everywhere C was written

[Mario Carneiro]

Maybe you have an old mathlib?

[Patrick Lutz]

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

[Patrick Lutz]

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

[Patrick Lutz]

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]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

These lemmas would simp the original goal.

[Patrick Lutz]

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]

@Scott Morrison I've now made the PR.

[Scott Morrison]

You can add links from zulip just by writing: #3376

[Scott Morrison]

I'll have a look!

[Scott Morrison]

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]

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

[Scott Morrison]

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]

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