Zulip Chat Archive

Stream: general

Topic: nonzero_ring?


Kenny Lau (May 27 2020 at 08:51):

We have nonzero_comm_ring and nonzero_comm_semiring and nonzero_semiring but not nonzero_ring. Is this deliberate?

Johan Commelin (May 27 2020 at 08:53):

Probably not

Kenny Lau (May 27 2020 at 08:57):

https://github.com/leanprover-community/mathlib/blob/2792c93ac5ad99a82945caad1110e6e284fd6ff7/src/algebra/ring.lean#L669-L676

/-- Predicate for semirings in which zero does not equal one. -/
class nonzero_semiring (α : Type*) extends semiring α, zero_ne_one_class α

/-- Predicate for commutative semirings in which zero does not equal one. -/
class nonzero_comm_semiring (α : Type*) extends comm_semiring α, zero_ne_one_class α

/-- Predicate for commutative rings in which zero does not equal one. -/
class nonzero_comm_ring (α : Type*) extends comm_ring α, zero_ne_one_class α

Kenny Lau (May 27 2020 at 09:00):

https://github.com/leanprover-community/mathlib/pull/2595/files#diff-997c56fe87e1352880681d783e610a7f

Kenny Lau (May 27 2020 at 09:00):

#2595 created nonzero_semiring but not nonzero_ring

Kenny Lau (May 27 2020 at 09:17):

#2839

Chris Hughes (May 27 2020 at 10:43):

The point of the commutative versions was to deal with polynomials. Nobody's found a point of the non commutative versions yet.

Chris Hughes (May 27 2020 at 10:44):

Is this related to codewars? I wanted this class for a Kata.

Kenny Lau (May 27 2020 at 10:47):

no, I want to refactor linear_algebra.basic

Kenny Lau (May 27 2020 at 10:47):

there are a lot of theorems with rings and 0 ne 1 assumption

Johan Commelin (May 27 2020 at 10:48):

Shouldn't zero_ne_one_class be a prop?

Johan Commelin (May 27 2020 at 10:49):

We could have a class [nonzero R], and then we can get rid of nonzero_* for all versions of *.

Mario Carneiro (May 27 2020 at 10:49):

zero_ne_one_class is one of the things we need to delete

Mario Carneiro (May 27 2020 at 10:50):

it makes sense for an algebraic hierarchy that isn't mathlib's

Mario Carneiro (May 27 2020 at 10:51):

If you use mixins for making classes, a la the mathcomp hierarchy, it makes sense

Kevin Buzzard (May 27 2020 at 10:54):

We want a non_subsingleton class :-)

Mario Carneiro (May 27 2020 at 10:55):

are those always the same thing in all classes where zero_ne_one makes sense?

Mario Carneiro (May 27 2020 at 10:56):

I guess it's true as long as 0 * x = 0 and 1 * x = x

Mario Carneiro (May 27 2020 at 10:57):

which seem like pretty safe bets in an algebraic class with a thing called 0

Johan Commelin (May 27 2020 at 10:57):

Is it true in with_zero \a if \a is an ordered_add_comm_monoid?

Johan Commelin (May 27 2020 at 10:57):

To bad... we don't have a 1 there :sad:

Kevin Buzzard (May 27 2020 at 10:58):

so 1 is definitely not 0, because we have two of those!

Mario Carneiro (May 27 2020 at 10:58):

It's not true in a add_monoid has_one, which is the context where nat.cast is stated

Kevin Buzzard (May 27 2020 at 10:58):

Johan's class should be an instance of zero_ne_zero_class

Reid Barton (May 27 2020 at 11:00):

that's the to_additive of zero_ne_one_class right?

Mario Carneiro (May 27 2020 at 11:01):

I feel like it should be possible to to_additive a semiring and get a tropical ring

Johan Commelin (May 27 2020 at 11:02):

Back on topic: what do we do with nonzero_*?

Johan Commelin (May 27 2020 at 11:02):

I wouldn't want to waste Kenny's refactor energy

Mario Carneiro (May 27 2020 at 11:02):

I think your idea is a good one

Mario Carneiro (May 27 2020 at 11:04):

although I think that we should still have things like domain and field containing nonzero as part of the structure

Johan Commelin (May 27 2020 at 20:46):

@Mario Carneiro what do you think of just using [fact (0:R) ≠ 1] whenever we need it, and adding an instance for this fact for [domain R]?

Johan Commelin (May 27 2020 at 20:46):

Then we can remove all the nonzero_* classes completely

Mario Carneiro (May 27 2020 at 20:56):

You can do this kind of encoding for anything. The big downside is that all facts end up in a single class, which means that typeclass inference is going to have to sort through all facts in all contexts when trying to prove this. So no, I think we should try to not have any instances of fact other than local instances and hypotheses

Kenny Lau (May 27 2020 at 21:11):

so what should we do?

Mario Carneiro (May 27 2020 at 21:11):

have a nonzero R class, which was Johan's original suggestion

Kenny Lau (May 27 2020 at 21:12):

for semiring?

Mario Carneiro (May 27 2020 at 21:13):

class nonzero (R) [has_zero R] [has_one R] := (zero_ne_one : 0 != 1)

Mario Carneiro (May 27 2020 at 21:13):

it could also be class nonzero (R) [semiring R]

Mario Carneiro (May 27 2020 at 21:14):

do we have monoid_with_zero?

Johan Commelin (May 27 2020 at 21:14):

Yes we do

Mario Carneiro (May 27 2020 at 21:15):

ah, I should get in the habit of using that for stuff with 0 and 1

Johan Commelin (May 27 2020 at 21:15):

But a monoid_with_zero is always nonzero

Johan Commelin (May 27 2020 at 21:15):

So I vote for your first option

Mario Carneiro (May 27 2020 at 21:15):

say what?

Mario Carneiro (May 27 2020 at 21:15):

that's definitely the wrong choice

Johan Commelin (May 27 2020 at 21:16):

Well, it worked for my one application...

Mario Carneiro (May 27 2020 at 21:16):

If monoid_with_zero is to group_with_zero as ring is to division_ring then it shouldn't have nonzero

Mario Carneiro (May 27 2020 at 21:17):

In particular I would like semirings to be monoid_with_zero

Johan Commelin (May 27 2020 at 21:17):

Yup, but I'm not sure that analogy should hold

Johan Commelin (May 27 2020 at 21:17):

Apparently in tropical geometry people study monoid_with_zero Ms and they are all nonzero by assumption.

Johan Commelin (May 27 2020 at 21:17):

That's why I included that assumption.

Johan Commelin (May 27 2020 at 21:17):

But it's probably a 2-line refactor to drop that assumption from mathlib

Mario Carneiro (May 27 2020 at 21:17):

luckily we now have a way to say this :)

Johan Commelin (May 27 2020 at 21:18):

s/now/almost/

Johan Commelin (May 27 2020 at 21:18):

I need to refill my 'refactor-mathlib' battery. So I would like to take a pass on this one.

Mario Carneiro (May 27 2020 at 21:18):

It seems awkward that group_with_zero and semiring currently have no greatest lower bound

Kevin Buzzard (May 27 2020 at 21:19):

The mathematical world is still reeling from the introduction of this new group_with_zero concept

Johan Commelin (May 27 2020 at 21:19):

But a complete refactor of the algebraic hierarchy... I wouldn't want to do that without more supporting tools

Kevin Buzzard (May 27 2020 at 21:19):

we haven't yet decided how much further it goes

Mario Carneiro (May 27 2020 at 21:20):

Johan Commelin said:

But a complete refactor of the algebraic hierarchy... I wouldn't want to do that without more supporting tools

It's not a complete refactor, just one new class

Mario Carneiro (May 27 2020 at 21:20):

some theorems will transfer to the weaker assumption, other stuff won't

Mario Carneiro (May 27 2020 at 21:20):

since it's a GLB class there will be no conflicts

Kenny Lau (May 28 2020 at 07:32):

Mario Carneiro said:

class nonzero (R) [has_zero R] [has_one R] := (zero_ne_one : 0 != 1)

https://github.com/leanprover-community/mathlib/commit/d1df1780ff89b8c023847b97119411601448f74c
https://github.com/leanprover-community/mathlib/tree/nonzero

Johan Commelin (May 28 2020 at 07:34):

Every sentence a verb

Johan Commelin (May 28 2020 at 07:35):

In other words: what the point?

Kenny Lau (May 28 2020 at 07:35):

I have started this refactor on the nonzero branch

Kenny Lau (May 28 2020 at 07:42):

[nonzero_semiring α] becomes [semiring α] [nonzero α]
[nonzero_comm_semiring α] becomes [comm_semiring α] [nonzero α]
[nonzero_comm_ring α] becomes [comm_ring α] [nonzero α]

Kenny Lau (May 28 2020 at 07:42):

(is there a place where I can put information like this?)

Johan Commelin (May 28 2020 at 07:43):

The commit message?

Bryan Gin-ge Chen (May 28 2020 at 07:45):

Note that when you make a PR, the contents of the first post become the commit message of the final squashed and merged commit.

Kenny Lau (May 28 2020 at 07:46):

along with the title?

Johan Commelin (May 28 2020 at 07:47):

When you create the PR it suggests a title, but it's usually crappy. It might also suggest a message, but you might want to change it.

Kenny Lau (May 28 2020 at 07:48):

I'm just asking whether the title also becomes the commit message

Kenny Lau (May 28 2020 at 07:48):

i.e. whether #2847 is correct

Johan Commelin (May 28 2020 at 07:48):

The title becomes the first line of the message, and will afterwards typically be formatted as a title.

Johan Commelin (May 28 2020 at 07:49):

Kenny Lau said:

i.e. whether #2847 is correct

Yup, looks fine to me

Kenny Lau (May 28 2020 at 07:50):

@[ancestor has_mul has_zero]
class no_zero_divisors (α : Type u) extends has_mul α, has_zero α :=
(eq_zero_or_eq_zero_of_mul_eq_zero :  a b : α, a * b = 0  a = 0  b = 0)

Kenny Lau (May 28 2020 at 07:50):

can we make this a Prop?

Kenny Lau (May 28 2020 at 07:50):

(by moving has_mul and has_zero before extends)

Kenny Lau (May 28 2020 at 07:50):

class domain (α : Type u) extends ring α, no_zero_divisors α, nonzero α

Kenny Lau (May 28 2020 at 07:51):

because the nonzero is problematic in "old_str_cmd true" and the no_zero_divisors is problematic in "false"

Johan Commelin (May 28 2020 at 07:51):

Yup, I would like that one to become a prop as well

Mario Carneiro (May 28 2020 at 07:51):

no_zero_divisors looks about as useful as zero_ne_one_class and distrib

Johan Commelin (May 28 2020 at 07:52):

Unbundling FTW!

Mario Carneiro (May 28 2020 at 07:52):

I think it should just be deleted (and merged into domain)

Johan Commelin (May 28 2020 at 07:52):

But group_with_zero!

Mario Carneiro (May 28 2020 at 07:53):

aha, is that a thing?

Johan Commelin (May 28 2020 at 07:53):

Never heard of them before

Mario Carneiro (May 28 2020 at 07:53):

pre-domain

Johan Commelin (May 28 2020 at 07:54):

quasi-pseudo-demi-domain

Mario Carneiro (May 28 2020 at 07:54):

splitting semimonoid

Mario Carneiro (May 28 2020 at 07:54):

gotta keep them guessing

Kenny Lau (May 30 2020 at 06:55):

rss-bot said:

chore(algebra): displace zero_ne_one_class with nonzero and make no_z…
chore(algebra): displace zero_ne_one_class with nonzero and make no_zero_divisors a Prop (#2847)

Johan Commelin (May 30 2020 at 07:12):

Thanks @Kenny Lau


Last updated: Dec 20 2023 at 11:08 UTC