Zulip Chat Archive

Stream: maths

Topic: euclidean domains


view this post on Zulip Johan Commelin (Jul 20 2018 at 07:25):

Currently, the definition of a Euclidean domain has the field

(val_remainder_lt :  a {b}, b  0  valuation (remainder a b) < valuation b)

I think it should read

(val_remainder_lt :  a {b}, b  0  (remainder a b = 0  valuation (remainder a b) < valuation b))

or something like that. What is best in these cases:
(i) the change as I suggest, or
(ii) move the claim remainder a b = 0 to a condition, so b \ne 0 \and remainder a b \ne 0 \to ...

view this post on Zulip Chris Hughes (Jul 20 2018 at 07:35):

My plan when I wrote polynomials, was that it should take a well founded relation instead of a valuation. mod_lt would be r (remainder a b) b and val_me_mul_left would be not r (a * b) a I think. degree now returns with_bot nat so it meets this definition.

view this post on Zulip Chris Hughes (Jul 20 2018 at 07:44):

The trouble with your definition is it makes every proof and definition longer. For example gcd needs an extra else if.

def gcd : α  α  α
| a := λ b, if a0 : a = 0 then b
 else if hba : remainder b a = 0 then a
 else
  have h:_ := or.resolve_left (val_mod_lt' b a0) hba,
  gcd (b%a) a
using_well_founded {rel_tac :=
  λ _ _, `[exact ⟨_, measure_wf valuation]}

view this post on Zulip Johan Commelin (Jul 20 2018 at 08:02):

On the other hand, it is the definition that every mathematician is used to...

view this post on Zulip Johan Commelin (Jul 20 2018 at 08:02):

@Chris Hughes Do you think the valuation of an ED should also take values in with_bot nat? And then require that valuation a = bot \iff a = 0?

view this post on Zulip Chris Hughes (Jul 20 2018 at 08:04):

That might be also be an idea, but without valuation a = bot \iff a = 0, because that will be annoying with integers.

view this post on Zulip Chris Hughes (Jul 20 2018 at 08:05):

But even so, I think arbitrary well founded is better, because then people dealing with integers can use the relation x.nat_abs < y.nat_abs where the use of with_bot would just be annoying.

view this post on Zulip Johan Commelin (Jul 20 2018 at 09:54):

So, what do you suggest as definition of ED?

view this post on Zulip Johan Commelin (Jul 20 2018 at 09:54):

Then we can try to use that, and also prove that it is equivalent to the "usual" definition. And possibly build a 2nd constructor that mimics the "usual" one.

view this post on Zulip Chris Hughes (Jul 20 2018 at 11:54):

I just made a PR with my suggested solution. https://github.com/leanprover/mathlib/pull/211

view this post on Zulip Johan Commelin (Jul 20 2018 at 12:04):

Nice! I like your speed!

view this post on Zulip Johan Commelin (Jul 20 2018 at 13:14):

Cool, you add an instance for int!


Last updated: May 10 2021 at 08:14 UTC