# Zulip Chat Archive

## Stream: maths

### Topic: constructive real algebraic numbers

#### Reid Barton (Nov 13 2019 at 12:06):

Not really a Lean question but the real algebraic numbers form a real closed field constructively, right? What's the easiest way to see this?

#### Reid Barton (Nov 13 2019 at 12:07):

I'm supposed to represent a real algebraic number by a polynomial together with an interval of rationals on which it has a unique root, or something?

#### Ulrik Buchholtz (Nov 13 2019 at 12:10):

I think the original reference is Madison 1970, but there may have been some improvements since.

#### Ulrik Buchholtz (Nov 13 2019 at 12:11):

Madison just pairs a polynomial together with the number of roots left of the desired root.

#### Reid Barton (Nov 13 2019 at 12:13):

Oh thanks. Let's suppose I already believe in quantifier elimination for real closed fields. Then it's easy to see how to decide the ordering on such descriptions. Let's suppose I also believe that given polynomials f and g I can find a polynomial whose roots are the sums of the roots of f and g. Is it easy to see how to pick out the index of the correct root?

#### Reid Barton (Nov 13 2019 at 12:14):

And same for products

#### Reid Barton (Nov 13 2019 at 12:14):

I guess this is probably in this 3-page paper, which I can't conveniently download at the moment

#### Ulrik Buchholtz (Nov 13 2019 at 12:27):

I guess this is probably in this 3-page paper, which I can't conveniently download at the moment

Actually, it's not, since he just shows that the relations $x + y = z$ and $xy = z$ are decidable. (Check you mail for the paper.) I don't see immediately how compute the representations of $x + y$ and $xy$ from those of $x$ and $y$.

#### Johan Commelin (Nov 13 2019 at 12:27):

Is his proof constructive?

#### Johan Commelin (Nov 13 2019 at 12:28):

I think there are methods using resultants and such, to go from `x`

and `y`

to `x + y`

and `xy`

.

#### Johan Commelin (Nov 13 2019 at 12:28):

I don't remember the details, but I think it can be done quite constructively

#### Ulrik Buchholtz (Nov 13 2019 at 12:30):

Yes, I think it's constructive. There are bunch of other representations where you pair a polynomial with either an interval, a Cauchy sequence, or something else. (I see *Thom representations* and *sign representations* and what-not…)

#### Reid Barton (Nov 13 2019 at 12:39):

The algorithms for arithmetic in the Madison paper are of the form "try every representation until you find one that works" (tested by quantifier elimination). I guess those won't satisfy a constructivist.

#### Reid Barton (Nov 13 2019 at 12:41):

I feel like this is the sort of thing someone would definitely have already formalized in Coq

#### Johan Commelin (Nov 13 2019 at 12:41):

Why? :see_no_evil: It would only have doubly-exponential running time...

#### Reid Barton (Nov 13 2019 at 12:43):

Because you don't know that the search will actually succeed unless you already proved (meaning constructively) that a solution exists

#### Johan Commelin (Nov 13 2019 at 12:43):

How about you combine the two representations: both small intervals around the roots and a pointer to the interval you care about.

#### Reid Barton (Nov 13 2019 at 12:43):

in which case you don't need the search

#### Johan Commelin (Nov 13 2019 at 12:43):

That might lead to rather efficient add/mul ?

#### Reid Barton (Nov 13 2019 at 12:45):

Aha, https://hal.inria.fr/hal-00671809v2

#### Johan Commelin (Nov 13 2019 at 12:46):

@Cyril Cohen We are watching you :grinning_face_with_smiling_eyes: :wink:

#### Patrick Massot (Nov 13 2019 at 12:49):

Why are we loosing Reid? What happened? He used to be doing mathematics!

#### Chris Hughes (Nov 13 2019 at 13:22):

I remember talking to Cyril about this. This is one place where Lean wins over Coq, because of quotients. In order to remain constructive in Coq, he had to reduce each number to a canonical, but I think he said most computer implementations actually don't reduce each number to a canonical form.

#### Reid Barton (Nov 13 2019 at 13:38):

Interesting.

I was going to ask @Mario Carneiro to automatically export the construction from Coq and import it into Lean (while remaining constructive of course) but I guess he's off the hook

#### Wojciech Nawrocki (Nov 29 2019 at 22:25):

Out of curiosity @Reid Barton what's your usecase for real algebraics? Wenda Li has been doing some great work on using them for efficiently deciding certain kinds of univariate polynomial inequalities in Isabelle: paper1 paper2

Last updated: May 19 2021 at 02:10 UTC