# Zulip Chat Archive

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

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

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?

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

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 `expr`

s that represent reals

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

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

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

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

#### Reid Barton (Sep 20 2020 at 20:27):

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?

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

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
exact (add_mul ↑a ↑b X).symm,
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`

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

Oh no.

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

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
exact (add_mul ↑a ↑b X).symm,
end
lemma test : (3 * X : polynomial ℤ) + (5 * X) = 8 * X :=
begin
apply X_add,
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
exact (add_smul a b X).symm
end
lemma xxx : (3 : ℤ) • (X : polynomial ℤ) + (5 : ℤ) • (X) = (8 : ℤ) • X :=
begin
apply X_add,
end
#simp [X_add] (3 : ℤ) • (X : polynomial ℤ) + (5 : ℤ) • (X) --(3 + 5) • X
```

Last updated: May 06 2021 at 20:13 UTC