Zulip Chat Archive

Stream: maths

Topic: Polynomials over a field are not quite Euclidean in lean


view this post on Zulip Chris Hughes (May 28 2018 at 09:16):

I've been trying to prove polynomials over a field are a Euclidean domain. The only trouble is, they do not meet the axioms if I use degree as valuation since for two constant polynomials, degree (a % b) = degree b. Does anyone have experience doing this in any other theorem prover and can recommend a sensible solution. The most obvious is to definenew_degree 0 = 0, and new_degree p = degree p + 1 for p ≠ 0. Is this the best option?

view this post on Zulip Johannes Hölzl (May 28 2018 at 09:23):

In Isabelle the size is not degree d itself but 2^d, and 0 for the 0 polynomial. See http://isabelle.in.tum.de/dist/library/HOL/HOL-Computational_Algebra/Polynomial_Factorial.html :

definition euclidean_size_field_poly :: "'a :: field poly ⇒ nat" where
  "euclidean_size_field_poly p = (if p = 0 then 0 else 2 ^ degree p)"

view this post on Zulip Chris Hughes (May 28 2018 at 09:24):

Why 2^d?

view this post on Zulip Johan Commelin (May 28 2018 at 09:26):

I actually think that valuation_remainder_lt is not what mathematicians want

view this post on Zulip Johan Commelin (May 28 2018 at 09:27):

It is a lot stronger than the usual condition

view this post on Zulip Johan Commelin (May 28 2018 at 09:27):

They swapped two quantifiers, so to speak

view this post on Zulip Mario Carneiro (May 28 2018 at 09:28):

what do you mean?

view this post on Zulip Johan Commelin (May 28 2018 at 09:28):

Quote from wiki: (EF1) If a and b are in R and b is nonzero, then there are q and r in R such that a = bq + r and either r = 0 or f(r) < f(b).

view this post on Zulip Johannes Hölzl (May 28 2018 at 09:28):

Why 2^d?

I guess you get the nice rule: E(p * q) = E(p) * E (q)

view this post on Zulip Mario Carneiro (May 28 2018 at 09:29):

oh, you need a % b != 0 also as a precondition

view this post on Zulip Johan Commelin (May 28 2018 at 09:29):

So it is about the existence of q and r, but this somehow requires it for all q and r

view this post on Zulip Johannes Hölzl (May 28 2018 at 09:29):

(where E = euclidean_size_field_poly)

view this post on Zulip Johan Commelin (May 28 2018 at 09:29):

Mario, I think that would also fix it, yes.

view this post on Zulip Mario Carneiro (May 28 2018 at 09:30):

that's basically what wiki is saying, or you can have a disjunction at the end

view this post on Zulip Johan Commelin (May 28 2018 at 09:30):

After all, the valuation of 0 is 37 according to @Kevin Buzzard

view this post on Zulip Mario Carneiro (May 28 2018 at 09:30):

hey, with the new with_zero class you can now just say that valuation takes values in with_zero nat

view this post on Zulip Johan Commelin (May 28 2018 at 09:31):

Nooo! with_zero nat looks horrible... can we please have with_bot or something

view this post on Zulip Mario Carneiro (May 28 2018 at 09:32):

it's the absorbing element of multiplication...

view this post on Zulip Mario Carneiro (May 28 2018 at 09:32):

there is also with_bot, which has no algebraic interpretation

view this post on Zulip Mario Carneiro (May 28 2018 at 09:33):

actually valuation looks like it doesn't need any algebraic interpretation, so I guess with_bot is fine

view this post on Zulip Chris Hughes (May 28 2018 at 09:34):

It could just be generalised to take any well founded relation, instead of a valuation

view this post on Zulip Chris Hughes (May 28 2018 at 17:58):

hey, with the new with_zero class you can now just say that valuation takes values in with_zero nat

Where is this class defined? I definitely prefer the idea of option nat over 2^degree.

view this post on Zulip Mario Carneiro (May 28 2018 at 19:30):

with_bot is in lattice.bounded_lattice, with_zero is in algebra.group. Basically it should already be available if you have the basic mathlib lemmas


Last updated: May 09 2021 at 09:11 UTC