types with 0 = bot

Stream: general

[Johan Commelin]

Should we have a typeclass for things where 0 = \bot? There are quite a number of examples:

• nat,
• nnreal,
• with_zero G (for G a linearly ordered comm monoid),
• X → Y, whenever Y is an instance of the class under discussion
• finsupp X Y, idem dito

[Johan Commelin]

Question is inspired by: https://github.com/leanprover-community/mathlib/pull/3094/files#diff-b49cdf1ee39a90ada5463a413001d526R97

[Mario Carneiro]

zero_le is a theorem of canonically_ordered_monoid but we could generalize it

[Johan Commelin]

I see, because I guess that X →\0 nat is not a canonically ordered monoid, right?

[Mario Carneiro]

I think it is?

[Johan Commelin]

Are canonically ordered monoids totally ordered?

[Mario Carneiro]

no

[Johan Commelin]

I see

[Mario Carneiro]

multiset is a good example too

[Johan Commelin]

So only with_zero G in the above list is not canonically ordered. The others are.

[Kevin Buzzard]

The ideals of a Dedekind domain are canonically ordered, the elements of a UFD aren't, but they only form a pre-order

[Kevin Buzzard]

Wait they are canonically ordered

[Kevin Buzzard]

Preordered

[Johan Commelin]

Kevin Buzzard said:

The ideals of a Dedekind domain are canonically ordered

But multiplicative... sorry, we don't support that.

[Johan Commelin]

So, should this be

class zero_eq_bot (X : Type*) [has_zero X] [has_bot X] :=
(zero_eq_bot : (0 : X) = \bot)

Or should this use a different setup?

[Johan Commelin]

I guess zero_eq_bot is a bad name for the class, because we want to reserve that name for the lemma...

[Kevin Buzzard]

We had zero_ne_one_class but look what happened to that

[Johan Commelin]

That was different.. it extended has_one and has_zero

[Kevin Buzzard]

I'm just saying that the name changed later

[Johan Commelin]

Aha, ok

[Kenny Lau]

Johan Commelin said:

So, should this be

class zero_eq_bot (X : Type*) [has_zero X] [has_bot X] :=
(zero_eq_bot : (0 : X) = \bot)

Or should this use a different setup?

I don't know why Lean doesn't know that this is a Prop, it should, but alright this is Prop

[Kevin Buzzard]

Zero_eq_bot_class is just asking to be renamed

[Kevin Buzzard]

Kenny it's a bug in structure

[Kevin Buzzard]

T2 spaces were types for a long time for this reason

[Mario Carneiro]

I don't like that class because it says nothing other than literally 0 = bot

[Mario Carneiro]

at the very least I want 0 and bot to have some algebraic meaning

[Mario Carneiro]

like it should extend order_bot or something so that you can prove zero_le

[Mario Carneiro]

Also, what about preorders satisfying zero_le but not 0 = bot?

[Johan Commelin]

Those are ugly

[Kevin Buzzard]

With_top int is used in valuations

[Kevin Buzzard]

But not with_bot int

[Mario Carneiro]

with_bot int wouldn't be one of these, right?

[Kevin Buzzard]

This whole thing is so weird. Mathematicians use different kinds of structures with + and *, and different kinds of structures with bot and top

[Mario Carneiro]

I think I would rather have this be a zero_le_class that doesn't say anything about bot

[Kevin Buzzard]

With_bot int has 0 ne bot but it's clearly an ugly class

[Kevin Buzzard]

You would never need it, you'd instead use eint

[Mario Carneiro]

I'm not really sure what the motivation for the question is TBH

[Kevin Buzzard]

Which also has zero ne bot and is a bit more respectable

[Kevin Buzzard]

If you think in this kind of way you end up isolating structures such as a group with 0, something which I consider rather a clever insight

[Mario Carneiro]

group with zero has some respectable axioms though

[Mario Carneiro]

this has just one equality

[Kevin Buzzard]

UFD should be a predicate on monoid with 0

[Mario Carneiro]

why with zero? It doesn't talk about zero at all

[Kevin Buzzard]

Because rings have 0 and you're stuck with them

[Mario Carneiro]

"all elements that are not zero-like have a unique factorization"

[Kevin Buzzard]

Eg nat

[Johan Commelin]

Mario Carneiro said:

I'm not really sure what the motivation for the question is TBH

See the second post of the thread

[Mario Carneiro]

I don't think this is a general class. nat.bot_eq_zero simply calculates the value of bot : nat according to the definition. I would call it nat.bot_eq

[Mario Carneiro]

This looks more like a definition unfolding simp lemma, and we generally don't make those into classes

[Johan Commelin]

@Mario Carneiro Let me #xy my question: What should the statement of finsupp.has_inf look like?

[Mario Carneiro]

well you can state it over a canonically ordered monoid and still cover all your targets

[Johan Commelin]

@Aaron Anderson :up:

[Mario Carneiro]

Actually that class doesn't have an inf

[Mario Carneiro]

you could define it, but there is also decidable_linear_ordered_cancel_add_comm_monoid which is not the lub of those classes but is an ub below nat

[Aaron Anderson]

In my code, I just defined the lattice structure on finsupps to nat, because I only really care about finsupps representing factorizations. It occurs to me that it might be nice to be able to define such factorizations with enats, so that we can prime-factorize 0, in which case canonically_ordered_add_monoid would also suffice. Thus I think canonically_ordered_add_monoid would work for all applications I can imagine at the moment

[Aaron Anderson]

Actually, no, this won't work right. I need canonically_ordered_add_monoids that are also (semi-)lattices

[Aaron Anderson]

In order to define (semi-)lattice operations

[Aaron Anderson]

And the other property I need is zero_le

[Mario Carneiro]

Does decidable_linear_ordered_cancel_add_comm_monoid work on enat?

[Mario Carneiro]

I guess it's not cancellative

[Johan Commelin]

We really need to rename that class to dlocacm

[Mario Carneiro]

I want to popularize more acronymy

[Simon Hudon]

Acronyms really make the code inscrutable. I think the cost to readability often exceeds any benefit

[Mario Carneiro]

Then we should use less words

[Mario Carneiro]

I want a character limit on concept names

[Mario Carneiro]

something like DLO_cancel_add_comm_monoid would work for me as well

[Mario Carneiro]

plus you can put the expansion in the docstring

[Aaron Anderson]

So I think if I was in a vacuum, I'd use something like [semilattice_inf_bot] [fact zero_eq_bot] and then feel icky about using fact ([semilattice_inf] [fact zero_le] would work, but such a thing is provably an instance of the other thing already!)

[Simon Hudon]

Mario Carneiro said:

I want a character limit on concept names

Why? How much do each character cost you?

Because concepts can be phrases, maybe the documentation should treat them as a series of words rather than one huge word.

[Mario Carneiro]

I think readability is significantly hampered in theorems like decidable_linear_ordered_cancel_add_comm_monoid.to_decidable_linear_ordered_add_comm_monoid

[Mario Carneiro]

At a certain point we should say "okay this sequence of words is a unit now, let's acronym and continue"

[Mario Carneiro]

that way we can keep recursively acronyming to keep the size bounded

[Aaron Anderson]

Kevin Buzzard said:

UFD should be a predicate on monoid with 0

I have half-baked ideas on this now, which you can see at https://github.com/leanprover-community/mathlib/blob/freek-70/roadmap/divisibility_lattice.lean if you want. I think that we could have a series of divisibility typeclasses on monoids, ranging from "reasonably defined dvd" to gcd_domain minus [integral_domain] to UFD minus [integral_domain].

[Aaron Anderson]

In the case of UFD, unfortunately, the only way to unify the case of monoids with zero and without zero that occurs to me is to use a finsupp primes enat definition of factorization, but enats are messy, and the zero and nonzero cases have different ways of reducing to regular nats

[Aaron Anderson]

Aaron Anderson said:

So I think if I was in a vacuum, I'd use something like [semilattice_inf_bot] [fact zero_eq_bot] and then feel icky about using fact ([semilattice_inf] [fact zero_le] would work, but such a thing is provably an instance of the other thing already!)

Actually, because [semilattice_inf] has inf_idem, the inf of two finsupps is still a finsupp even without zero_le. It's just that I'd have to use filter or something to define the supports of infs and sups, although I could prove lemmas to simplify those in some cases.

[Aaron Anderson]

(of course a bot instance still requires zero_le)

[Aaron Anderson]

I've made some progress at #3335, but there's still some awkward assumptions where there should be typeclass inference

[Aaron Anderson]

I think everything I want to do really applies to finsupps with values in nat, enat, nnreal, or ennreal.

[Johan Commelin]

Right, so we need to have a typeclass that applies to all those cases

[Aaron Anderson]

It would be enough to assume that I'm working with a canonically_ordered_add_monoid which is also compatibly a decidable_linear_order

[Aaron Anderson]

I think this is a job for tactic.pi_instances?

[Johan Commelin]

Well... it's not really a pi type

[Johan Commelin]

So... I'm not so sure

[Aaron Anderson]

Well, I'm just wondering what in this file https://github.com/leanprover-community/mathlib/blob/6c1ae3b/src/order/bounded_lattice.lean#L21 allows typeclasses like semilattice_inf_bot to extend semilattice_inf and order_bot simultaneously with the same le

[Johan Commelin]

set_option old_structure_cmd true

[Johan Commelin]

That's the magic bit that makes them share fields that they have in common

[Aaron Anderson]

Is there a way to do this when you have a lemma that wants to use two typeclass instances that have fields in common, or do you just need to make a new typeclass extending both, with that command?

[Johan Commelin]

I think you need a new class

[Johan Commelin]

So you mentioned two classes... are they sufficient to prove 0 \le x for all x?

[Aaron Anderson]

Just canonically_ordered_add_monoid is enough for zero_eq_bot

[Johan Commelin]

So what do you need the DLO for?

[Johan Commelin]

Or rather, what is the kind of statement for which you need both?

[Aaron Anderson]

To show that (inf f g).support is the intersection of f.support and g.support

[Johan Commelin]

Aha, I see

[Aaron Anderson]

I need the fact that inf x y = 0 iff x = 0 or y = 0

[Johan Commelin]

I guess we need a linearly canon.ord.add.mon in that case

[Aaron Anderson]

And if I want to put an instance of canonically_ordered_add_monoid on finsupp, then some things also break, which I'm fairly sure can be fixed under the DLO assumption

[Aaron Anderson]

I'll make that extra class and try everything out later today. Should the extra class be defined in the same file as canonically_ordered_add_monoid?

[Johan Commelin]

Ok, so wherever canon.ord.add.mon is defined, you can add another type that is a linear version