Best way to reason on distribution of solutions?

Stream: general

[Shi Zhengyu]

Hi all,

What is the best way to reason about the distribution of real roots of a polynomial? I was trying to prove two polynomials' solutions are interlaced. Below is a definition of interlace I wrote for two lists.

mutual def Interlace, Interlace' {num_t: Type} [linear_order num_t]
with Interlace: list num_t -> list num_t -> Prop
| (x :: xs) (y :: ys) := (x <= y) ∧ Interlace' xs (y :: ys)
| (x :: xs) nil := true
| _ _ := false
with Interlace': list num_t -> list num_t -> Prop
| (x :: xs) (y :: ys) := (y <= x) ∧ Interlace (x :: xs) ys
| _ _ := false

Then I need to define

def solution (A: polynomial ℂ): list ℂ := sorry

Is it good practice to use above definition, and treat solutions as elements of a list? If so, how should I fill in the sorry above?

Thanks!

[Kevin Buzzard]

I don't know much about inductive types but if I were thinking about formalising this I would have just written the predicate directly; one doesn't need inductive types to do it: just write that the n'th term of one list is in between the n'th and the n+1st term of the other one. As for solution this is going to be there already -- at least as a finset -- let's try docs#polynomial.roots ? And then take the reals ones and sort them.