Zulip Chat Archive
Stream: metaprogramming / tactics
Topic: constant polynomial tactic
Jack J Garzella (Jun 17 2020 at 18:08):
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)
 Reflect the f to a listbased representation (sort of like in Kevin's post)

Express the reflected f as a sum of the highest nonzero term and the rest
> the highest nonzero degree term has degree n bydegree_monomial
> the rest has degree less than n by recursing 
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 (Jun 17 2020 at 18:08):
I think that's Patrick's tutorial, but very much inspired by earlier comments of Mario (as was my blog post :D)
Kevin Buzzard (Jun 17 2020 at 18:09):
This is a great idea by the way; note that you'll need to assume your ring is nonzero, otherwise the degree of X^5 is not 5 :/
Jack J Garzella (Jun 17 2020 at 19:06):
Oops! Sorry Patrick! Should be fixed now
Patrick Massot (Jun 17 2020 at 19:52):
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 (Jun 18 2020 at 11:26):
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 (Jun 19 2020 at 16:54):
Alex J. Best said:
An (alternative?) approach could use
ring
as a preprocessing step to get the polynomial intoSOP
orhorner
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 (Jun 19 2020 at 16:54):
Is there a more detailed exposition of SOP
somewhere? In the ring
code it seems to be mentioned more offhand
Mario Carneiro (Jun 19 2020 at 17:46):
There is no formal definition, but it basically produces terms like 3 * x * y^2 + y^2 * z  9
Alex J. Best (Jun 19 2020 at 18:38):
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 (Jun 21 2020 at 00:19):
Hmm, would it ever be possible that an expression in horner normal form for f
to be zero in that case?
Jack J Garzella (Jun 21 2020 at 00:19):
Another thought is, how hard would it be to break into cases based on whether something is zero?
Alex J. Best (Jun 21 2020 at 01:27):
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 (Jun 21 2020 at 01:30):
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.
Last updated: May 09 2021 at 21:10 UTC