Polynomials over a field are not quite Euclidean in lean

Stream: maths

[Chris Hughes]

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?

[Johannes Hölzl]

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)"

[Chris Hughes]

Why 2^d?

[Johan Commelin]

I actually think that valuation_remainder_lt is not what mathematicians want

[Johan Commelin]

It is a lot stronger than the usual condition

[Johan Commelin]

They swapped two quantifiers, so to speak

[Mario Carneiro]

what do you mean?

[Johan Commelin]

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).

[Johannes Hölzl]

Why 2^d?

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johannes Hölzl]

(where E = euclidean_size_field_poly)

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

it's the absorbing element of multiplication...

[Mario Carneiro]

there is also with_bot, which has no algebraic interpretation

[Mario Carneiro]

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

[Chris Hughes]

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

[Chris Hughes]

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.

[Mario Carneiro]

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