Zulip Chat Archive

Stream: new members

Topic: Playing with polynomials


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Sep 20 2020 at 06:43):

"If you want to calculate, use Python"

view this post on Zulip Kenny Lau (Sep 20 2020 at 06:44):

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

view this post on Zulip Kenny Lau (Sep 20 2020 at 06:44):

probably some version in 2018

view this post on Zulip Lucas Allen (Sep 20 2020 at 06:57):

Ok.

view this post on Zulip Reid Barton (Sep 20 2020 at 10:51):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Sep 20 2020 at 11:52):

I need a telephone booth emoji

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Sep 20 2020 at 12:08):

yes

view this post on Zulip Mario Carneiro (Sep 20 2020 at 12:08):

just like norm_num but for polynomials

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Sep 20 2020 at 14:48):

It really works with exprs that represent reals

view this post on Zulip Kevin Buzzard (Sep 20 2020 at 14:48):

Aah!

view this post on Zulip Kevin Buzzard (Sep 20 2020 at 14:49):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 20 2020 at 14:54):

Thanks!

view this post on Zulip Kevin Buzzard (Sep 20 2020 at 14:55):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 20 2020 at 14:57):

along with perhaps a lack of specific applications at the moment

view this post on Zulip Kevin Buzzard (Sep 20 2020 at 14:58):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Sep 20 2020 at 14:59):

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

view this post on Zulip 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).

view this post on Zulip Reid Barton (Sep 20 2020 at 14:59):

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

view this post on Zulip Kevin Buzzard (Sep 20 2020 at 15:00):

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

view this post on Zulip Reid Barton (Sep 20 2020 at 15:00):

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

view this post on Zulip Kevin Buzzard (Sep 20 2020 at 15:00):

Nobody can prove the algorithm terminates, for starters

view this post on Zulip Reid Barton (Sep 20 2020 at 15:01):

Well that's not actually a problem

view this post on Zulip Kevin Buzzard (Sep 20 2020 at 15:03):

Try telling that to the equation compiler

view this post on Zulip Kevin Buzzard (Sep 20 2020 at 15:03):

Of course I see what you mean, tactics are meta

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Kevin Buzzard (Sep 20 2020 at 15:10):

which is good because that's an open problem

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 20 2020 at 20:27):

aha!

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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 []

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Sep 21 2020 at 04:48):

Aah, I guess you do

view this post on Zulip 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?

view this post on Zulip Lucas Allen (Sep 21 2020 at 04:49):

Yes!

view this post on Zulip 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

view this post on Zulip Lucas Allen (Sep 21 2020 at 04:59):

Adding @[simp] gives a red squiggle.

view this post on Zulip Johan Commelin (Sep 21 2020 at 05:29):

@Lucas Allen because the statement doesn't use m

view this post on Zulip Lucas Allen (Sep 21 2020 at 05:33):

Oh no.

view this post on Zulip Lucas Allen (Sep 21 2020 at 05:33):

sorry.

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Sep 21 2020 at 05:42):

What happens if you rw instead of apply?

view this post on Zulip Johan Commelin (Sep 21 2020 at 05:43):

I would have expected the apply to work though.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Lucas Allen (Sep 21 2020 at 05:54):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 21 2020 at 05:57):

Try (3 : \Z) instead

view this post on Zulip Johan Commelin (Sep 21 2020 at 05:57):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 21 2020 at 05:58):

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

view this post on Zulip Lucas Allen (Sep 21 2020 at 06:00):

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

view this post on Zulip 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