constant polynomial tactic

Stream: metaprogramming / tactics

[Jack J Garzella]

I'm hoping to get my feet wet with metaprogramming in lean by writing a degree_constant_poly tactic. The idea is for it to prove statements like degree (C 2 * X ^ 3 - X + 2) = 3 and degree (X ^ 5) = 5.
After skimming Kevin's post and Mario's Tutorial, I think I have an idea of what the pseudocode should be, but I have no experience so I'm not sure if I'm falling into a trap:

Let f be the constant polynomial expression (which should have degree n)

1. Reflect the f to a list-based representation (sort of like in Kevin's post)

2. Express the reflected f as a sum of the highest nonzero term and the rest
   --> the highest nonzero degree term has degree n by degree_monomial
   --> the rest has degree less than n by recursing

3. Use degree_add_eq_of_degree_lt to finish the proof

Does this seem like a sane way to do this? Also are there implementation details I should worry about, i.e. would it be important for this to be tail recursive in the actual implementation?

[Kevin Buzzard]

I think that's Patrick's tutorial, but very much inspired by earlier comments of Mario (as was my blog post :D)

[Kevin Buzzard]

This is a great idea by the way; note that you'll need to assume your ring is non-zero, otherwise the degree of X^5 is not 5 :-/

[Jack J Garzella]

Oops! Sorry Patrick! Should be fixed now

[Patrick Massot]

Kevin Buzzard said:

I think that's Patrick's tutorial, but very much inspired by earlier comments of Mario (as was my blog post :D)

For the record, most of what is in that tutorial was taught to me by Simon, not Mario (but of course without Mario I would have stopped learning Lean after one day of suffering, long long before Simon got the opportunity to teach me anything).

[Alex J. Best]

An (alternative?) approach could use ring as a preprocessing step to get the polynomial into SOP or horner form, then repeatedly apply lemmas to compute the degree based on that normal form.

[Jack J Garzella]

Alex J. Best said:

An (alternative?) approach could use ring as a preprocessing step to get the polynomial into SOP or horner form, then repeatedly apply lemmas to compute the degree based on that normal form.

This is probably what I really want to do. I think SOP form might be the best, because I really want to look at the individual monomials. This means I'll have to implement some sort of degree or multidegree, then implement lemmas like degree_monomial and degree_ad_eq_of_degree_lt for the normal form.

[Jack J Garzella]

Is there a more detailed exposition of SOP somewhere? In the ring code it seems to be mentioned more offhand

[Mario Carneiro]

There is no formal definition, but it basically produces terms like 3 * x * y^2 + y^2 * z - 9

[Alex J. Best]

I was thinking horner would be nicer actually, but I didn't try it all! Assuming it gives you (X + 1)* X + 1 you could have a lemma like degree f*X + C a = degree f + 1 and compute from out to in 1 + 1 + 1 + ...., the problem is the side condition for this lemma that f \ne 0 which might be a bit annoying.

[Jack J Garzella]

Hmm, would it ever be possible that an expression in horner normal form for f to be zero in that case?

[Jack J Garzella]

Another thought is, how hard would it be to break into cases based on whether something is zero?

[Alex J. Best]

Right, with horner form it shouldn't happen, its just a matter of proving from the innermost term to the outermost that the degree is increasing by one each time?

[Alex J. Best]

I guess you'll need some decision procedure for the coefficients of the polynomial, which could be just using decidable_eq for the base ring, but may be more complicated, e.g. for reals there isn't decidable equality, so the leading term could be something with cannot be decided to not equal zero which would stymie the tactic, but in most cases people aren't going to end up in that situation, instead some situation where norm_num can prove the coefficient nonzero.