## Stream: new members

### Topic: Playing with polynomials

#### Lucas Allen (Sep 20 2020 at 06:26):

Hello, in an effort to play with polynomials in Lean I came up with the following,

import data.polynomial

open polynomial

noncomputable def P : polynomial ℤ := 3 * X^2 + 1
noncomputable def Q : polynomial ℤ := 4 * X^2 + 7 * X + 6

#check P + Q
#check P - Q
#check P * Q
#check P /ₘ Q

#eval P + Q
#eval P - Q
#eval P * Q
#eval P /ₘ Q


The #eval lines give the error "code generation failed, VM does not have code for 'classical.choice'", and the definitions of P and Q demand the noncomputable. Is there some way around the noncomputability of polynomials, so that #eval P + Q gives 7 * X^2 + 7 * X + 7?

#### Kenny Lau (Sep 20 2020 at 06:43):

"If you want to calculate, use Python"

#### Kenny Lau (Sep 20 2020 at 06:44):

(or use an older version of Lean/mathlib before we decided to make everything noncomputable)

#### Kenny Lau (Sep 20 2020 at 06:44):

probably some version in 2018

Ok.

#### Reid Barton (Sep 20 2020 at 10:51):

Or use a future version of Lean/mathlib with the norm_poly tactic

#### Kevin Buzzard (Sep 20 2020 at 11:44):

@Lucas Allen can you please leave 2020, you've come to the wrong year. Please recalibrate a couple of years in either direction.

#### Mario Carneiro (Sep 20 2020 at 11:52):

I need a telephone booth emoji

#### Kevin Buzzard (Sep 20 2020 at 12:06):

Polynomials used to be computable but this caused trouble with reasoning. Now they're noncomputable but apparently this causes problems with computation. Is Reid right that this can be fixed with a tactic?

yes

#### Mario Carneiro (Sep 20 2020 at 12:08):

just like norm_num but for polynomials

#### Reid Barton (Sep 20 2020 at 12:09):

The trick is the kind of "computation" you want is not the same as the noncomputable kind. For example, norm_num works on the reals too

#### Kenny Lau (Sep 20 2020 at 12:58):

that there are two meanings of "computation": the Lean meaning, which is that you write a program that does it; the mathematical meaning, which is that you reduce something to a normal form.

#### Kevin Buzzard (Sep 20 2020 at 14:38):

There's some trickery involved though, isn't there? Because norm_num doesn't _really_ work with reals, right? It can only make progress if all the reals are rational.

#### Reid Barton (Sep 20 2020 at 14:48):

It really works with exprs that represent reals

Aah!

#### Kevin Buzzard (Sep 20 2020 at 14:49):

So why don't we teach it that sqrt(x)*sqrt(x)=x :-)

#### Reid Barton (Sep 20 2020 at 14:51):

Like this?

import data.real.basic
import tactic.norm_num

example : real.sqrt 5 * real.sqrt 5 = 5 := by norm_num


Thanks!

#### Kevin Buzzard (Sep 20 2020 at 14:55):

(I never knew it did that -- I had the wrong mental model)

#### Reid Barton (Sep 20 2020 at 14:57):

I think the main obstruction to turning norm_num into something more like a computer algebra system is that it's not obvious (at least to me) what kind of organizational framework is appropriate

#### Reid Barton (Sep 20 2020 at 14:57):

along with perhaps a lack of specific applications at the moment

#### Kevin Buzzard (Sep 20 2020 at 14:58):

I want to prove that $x^2-4$ is not irreduible without doing any work.

#### Reid Barton (Sep 20 2020 at 14:58):

but for any computation you can do in a CAS, provided you can give a proof that the computation is correct (when it succeeds), there's no reason that something like norm_num couldn't be extended to do it

#### Kevin Buzzard (Sep 20 2020 at 14:59):

Actually I don't really want to prove this at all, I just want to prove stuff about DVRs etc. I don't have a specific application.

#### Reid Barton (Sep 20 2020 at 14:59):

This example is pretty trivial because ring can already do the correctness proof

#### Kevin Buzzard (Sep 20 2020 at 14:59):

I guess sometimes I want to prove that y^2=x^3-4x has rank 0 (or 1 or whatever).

#### Reid Barton (Sep 20 2020 at 14:59):

so you can "just" do the factorization in an untrusted program

#### Kevin Buzzard (Sep 20 2020 at 15:00):

and Cremona's software is not spitting out a formally verifiable thing here

#### Reid Barton (Sep 20 2020 at 15:00):

Right, I think you skipped over a large range of difficulties there :upside_down:

#### Kevin Buzzard (Sep 20 2020 at 15:00):

Nobody can prove the algorithm terminates, for starters

#### Reid Barton (Sep 20 2020 at 15:01):

Well that's not actually a problem

#### Kevin Buzzard (Sep 20 2020 at 15:03):

Try telling that to the equation compiler

#### Kevin Buzzard (Sep 20 2020 at 15:03):

Of course I see what you mean, tactics are meta

#### Reid Barton (Sep 20 2020 at 15:06):

For a procedure like this, there are two relevant outcomes:

• the procedure succeeds in producing an answer along with a correct proof
• all other behavior: nontermination, answer but no certificate, certificate but it doesn't type check somehow

#### Reid Barton (Sep 20 2020 at 15:08):

If you can build a procedure which provably always has the first behavior then great, but in practice it's fine to have tactics that can fail, as long as they work when you need them to

#### Reid Barton (Sep 20 2020 at 15:09):

since our goal is to compute the ranks of elliptic curves (or whatever), not prove an internal theorem "there exists an algorithm which computes the rank of every elliptic curve"

#### Kevin Buzzard (Sep 20 2020 at 15:10):

which is good because that's an open problem

#### Mario Carneiro (Sep 20 2020 at 20:24):

FYI, this was a surprise to me as well. norm_num doesn't know anything about square roots, that's all simp's work

aha!

#### Bryan Gin-ge Chen (Sep 20 2020 at 20:42):

Returning to the initial question, right now #simp [P,Q] P + Q just returns 3 * X ^ 2 + 1 + (4 * X ^ 2 + 7 * X + 6), but maybe it's possible to add some simp lemmas (or make a simp set?) to make it more "useful".

#### Lucas Allen (Sep 21 2020 at 04:40):

Kevin Buzzard said:

Lucas Allen can you please leave 2020, you've come to the wrong year. Please recalibrate a couple of years in either direction.

I think practicing the art of impeccable timing is starting to pay off.

#### Lucas Allen (Sep 21 2020 at 04:42):

Bryan Gin-ge Chen said:

Returning to the initial question, right now #simp [P,Q] P + Q just returns 3 * X ^ 2 + 1 + (4 * X ^ 2 + 7 * X + 6), but maybe it's possible to add some simp lemmas (or make a simp set?) to make it more "useful".

I had a go at adding a simp lemma to see if it worked,

@[simp] lemma X_add : (X : polynomial ℤ) + X = 2 * X := sorry

#simp [X] X + X


It gives "monomial 1 1 + monomial 1 1", but I want "2 * X". I also tried #simp [(X : polynomial ℤ)] X + X but this gives "simplify tactic failed to simplify." Is there some way to get this to work?

#### Johan Commelin (Sep 21 2020 at 04:43):

Ooh, you don't want to put X in the simpset, rather put X_add between the []

#### Lucas Allen (Sep 21 2020 at 04:47):

#simp [X_add] X + X gives "simplify tactic failed to simplify". Do I need to say something about it being a ℤ polynomial?

#### Johan Commelin (Sep 21 2020 at 04:48):

Aah, I guess you do

#### Johan Commelin (Sep 21 2020 at 04:48):

@[simp] lemma X_add : (X : polynomial ℤ) + X = 2 * X := sorry

#simp [X_add] (X : polynomial ℤ) + X


does this work?

Yes!

#### Lucas Allen (Sep 21 2020 at 04:58):

Why is this an invalid simp lemma?

lemma X_add (m : ℕ) (a b : ℤ) : (a * X : polynomial ℤ) + (b * X) = (a + b) * X :=
begin
end


#### Lucas Allen (Sep 21 2020 at 04:59):

Adding @[simp] gives a red squiggle.

#### Johan Commelin (Sep 21 2020 at 05:29):

@Lucas Allen because the statement doesn't use m

Oh no.

sorry.

#### Lucas Allen (Sep 21 2020 at 05:39):

I get a deterministic timeout with the following

@[simp] lemma X_add (a b : ℤ) : (a * X : polynomial ℤ) + (b * X) = (a + b) * X :=
begin
end

lemma test : (3 * X : polynomial ℤ) + (5 * X) = 8 * X :=
begin
end


I don't know why, and I hope it's not obvious again...

#### Johan Commelin (Sep 21 2020 at 05:42):

What happens if you rw instead of apply?

#### Johan Commelin (Sep 21 2020 at 05:43):

I would have expected the apply to work though.

#### Lucas Allen (Sep 21 2020 at 05:52):

"rewrite tactic failed, did not find instance of the pattern in the target expression
↑?m_1 * X + ↑?m_2 * X
state:
⊢ 3 * X + 5 * X = 8 * X"

no deterministic timeout though.

#### Lucas Allen (Sep 21 2020 at 05:54):

I'm wondering if it has something to do with the fact that a * X has type polynomial ℤ, and it's not (a : ℤ) * X.

#### Lucas Allen (Sep 21 2020 at 05:54):

But (a : ℤ) * X doesn't work.

#### Lucas Allen (Sep 21 2020 at 05:57):

lemma X_add (a b : ℤ) : a * (X : polynomial ℤ) + b * X = (a + b) * X :=gives red squiggles under the *'s. It likes lemma test : 3 * (X : polynomial ℤ) + 5 * (X) = 8 * X :=  however.

#### Johan Commelin (Sep 21 2020 at 05:57):

Try (3 : \Z) instead

#### Johan Commelin (Sep 21 2020 at 05:57):

but rather, I think you should use C to create constant polynomials

#### Johan Commelin (Sep 21 2020 at 05:58):

Arguably, we should consider making a \bu X the standard way of multiplying by scalars, instead of C a * X.

#### Lucas Allen (Sep 21 2020 at 05:58):

lemma xxx : (3 : ℤ) * (X : polynomial ℤ) + (5 : ℤ) * (X) = (8 : ℤ) * X := gives red squiggles under the *'s type mismatch error.

#### Johan Commelin (Sep 21 2020 at 05:58):

((3 : \Z) * X : ...) ?

#### Lucas Allen (Sep 21 2020 at 06:00):

I think it was (3 : \Z) * (X : ...)

#### Lucas Allen (Sep 21 2020 at 06:01):

It likes the \bu. Everything works now.

@[simp] lemma X_add (a b : ℤ) : a • (X : polynomial ℤ) + b • X = (a + b) • X :=
begin