well-founded recursion on polynomials

Stream: general

[Eric Rodriguez]

I'd really like to be able to make this definition:

def derivative_seq : R[X] → list R[X]
| 0 := []
| p := p :: derivative_seq (p.derivative)

but Lean shouts at me in many ways, and I guess understandably so. There's many things wrong with this - firstly, I don't think Lean likes me using 0 as a pattern (and I'm not too sure that .(0) helps - if I do that and turn it into a meta_def, it just turns the whole function into λ p, []). Furthermore, I'd like to use well-founded recursion here - for p ≠ 0, we clearly have that degree (p.derivative) < degree p, but how do I get that p ≠ 0 apart from that if it was, we'd have gone down the first path?

I guess essentially I'm really misunderstanding the equation compiler and maybe forcing it to do things it doesn't want to. Is the correct way to use wf.fix?

[Eric Rodriguez]

is this the correct way to do this?

noncomputable def derivative_seq [decidable_eq R[X]] : R[X] → list R[X]
| p := if p ≠ 0 then p :: derivative_seq (p.derivative) else []

[Eric Wieser]

Another option would be to directly recurse on p.degree

[Eric Rodriguez]

hmm, that doesn't seem to well-found properly, this throws an error:

noncomputable def derivative_seq [decidable_eq R[X]] : R[X] → list R[X]
| p := if h : p = 0 then [] else have _ := polynomial.degree_derivative_lt h,
                                 p :: derivative_seq (p.derivative)

[Eric Rodriguez]

Eric Wieser said:

Another option would be to directly recurse on p.degree

with a match, you mean?

[Eric Wieser]

Probably an auxiliary def

[Eric Wieser]

def aux : ℕ → polynomial R → list (polynomial R)
| 0 p := []
| (n+1) p := p :: aux n p.derivative

Then use aux p.degree p or similar

[Reid Barton]

Why do you need a list?

[Eric Rodriguez]

What do you suggest, Reid? I'm trying to implement Budan-Fourier like the Isabelle implementation

[Eric Rodriguez]

https://arxiv.org/abs/1811.11093

[Eric Wieser]

polynomial.derivative^[n] maybe?

[Eric Rodriguez]

I can also just stick that in a list.map, I don't get p :: derivative_seq p' = derivative_seq p automatically but that's ok

[Johan Commelin]

But even then, why would you need a list?

[Eric Rodriguez]

My understanding of the theorem is that I take the sequence of derivatives, evaluate them at a point, and the sign differences in this sequence are meaningful. The way I calculate sign differences is using a list representation, although also a finsupp could work just as well, thinking about it.

[Eric Rodriguez]

It's also far more idiomatic; I've made a function that turns a polynomial into a list and even proving that a monomial's representation was if r = 0 then [0] else r :: list.repeat 0 n was hell

[Eric Rodriguez]

I think in Isabelle (or at least from what I got from the paper) they represent polynomials directly as lists, so they don't have to think about all this

[Eric Rodriguez]

oh, maybe not:

typedef (overloaded) 'a poly = "{f :: nat ⇒ 'a::zero. ∀⇩∞ n. f n = 0}"

[Johan Commelin]

I think you can just work with nat -> R given by n \mapsto (polynomial.derivative^[n] p).eval x.

[Johan Commelin]

That sequence will eventually be zero

[Johan Commelin]

But you can still count the number of sign differences on the image of finset.range (p.nat_degree + 1).