Zulip Chat Archive

floor_semiring would readily extend nat_ceil (and the yet inexistent nat_floor) and maybe we could set up an inference from floor_ring to floor_semiring using int.to_nat?

Kevin Buzzard (Jun 04 2021 at 16:56):

I can't really imagine a nat-valued floor function on the reals, this is what's confusing me.

Kevin Buzzard (Jun 04 2021 at 16:57):

If you want to define semiring_floor of (-1 : real) to be 0 then it doesn't satisfy the Galois connection property: (0 : nat) <= floor(-1) but 0 isn't <= -1 in the reals.

Yaël Dillies (Jun 04 2021 at 18:05):

I'm now writing the API. Shall I mention directly the gc in the class definition?

Yaël Dillies (Jun 04 2021 at 18:21):

And here I hit a problem. I have two conflicting notions of floor. Is there any way to give them the same name, but allow Lean to get the best one regarding the situation? (it sounds prone to creating bugs...) That is, it gets the ring floor when dealing with a floor_ring and the semiring floor when dealing with afloor_semiring.

Yaël Dillies (Jun 04 2021 at 18:32):

Actually, the name is not too bad because we can define notation. But what about notation then?

Yakov Pechersky (Jun 04 2021 at 18:57):

This is what typeclasses are for. Except what happens if something is both a floor_ring and a floor_semiring?

Yaël Dillies (Jun 04 2021 at 19:17):

I don't think that happens because a floor_ring is bounded below and a floor_semiringis unbounded.

Yaël Dillies (Jun 04 2021 at 19:18):

Of course, you can take different ordering of the same type, but that surely doesn't come up in practice when using floors and ceils.

Yaël Dillies (Jun 04 2021 at 20:22):

It's actually not that trivial to generalise that stuff... For example, how can you define the fractional part without referring to substraction?

Yaël Dillies (Jun 04 2021 at 20:24):

Is there something like a partial substraction where a - b + b = a if b ≤ a, as for ℕ?

Eric Wieser (Jun 04 2021 at 21:42):

"monus" has been used for that before I think. Pi-like types with nat in their codomain would inherit such a structure

Yaël Dillies (Jun 05 2021 at 17:18):

Where do I find that? The docs search is inconclusive.

Eric Wieser (Jun 05 2021 at 17:58):

monus only exists in zulip threads

Kevin Buzzard (Jun 05 2021 at 18:00):

Isn't it basically equivalent to some cancellative assumption? a+b=a+c -> b=c?

Kevin Buzzard (Jun 05 2021 at 18:01):

Oh maybe it's equivalent to this "canonical order" assumption as in canonically_ordered_monoid

Yaël Dillies (Jun 05 2021 at 18:01):

Not really. The cancellative assumption asserts that this monus is unique. What I want is the existence

Kevin Buzzard (Jun 05 2021 at 18:01):

Then canonical order I think

Kevin Buzzard (Jun 05 2021 at 18:02):

Wait, maybe you just want half of that implication. The integers are not canonically ordered, for example

Yaël Dillies (Jun 05 2021 at 18:03):

Aren't they?

Mario Carneiro (Jun 05 2021 at 18:03):

the reverse implication fails

Mario Carneiro (Jun 05 2021 at 18:04):

a - b + b = a does not imply b <= a

Mario Carneiro (Jun 05 2021 at 18:04):

I don't think we have a version of canonically ordered with just one side of the implication

Yaël Dillies (Jun 05 2021 at 18:05):

And I guess linear_ordered isn't enough?

Mario Carneiro (Jun 05 2021 at 18:05):

No, it's off the beaten path of algebraic classes since negatives make it fail

Yaël Dillies (Jun 05 2021 at 18:06):

Argh

Yaël Dillies (Jun 05 2021 at 18:06):

And what about ceil?

Yaël Dillies (Jun 05 2021 at 18:07):

Isn't N conditionnally complete?

Yaël Dillies (Jun 05 2021 at 18:09):

Ah wait, that's bad. I want to match floor. So maybe I can define ceil x := ite (floor x = x) x (floor x + 1)? Sounds a bit tricky to prove stuff about.

Yaël Dillies (Jun 05 2021 at 18:10):

If a linear_ordered_semiring really is the positive half of a linear_ordered_ring, how come it be that hard

Kevin Buzzard (Jun 05 2021 at 18:25):

If you really want the integers to not be a floor semiring then you can use canonically ordered. The issue is whether the floor is int valued or nat valued. If it's nat valued then the key floor axiom implies that everything in the ring is >= 0 and then you're fine to use canonically ordered additive monoids. Maybe they should not be called floor semirings though, maybe semifloor semirings or something?

Kevin Buzzard (Jun 05 2021 at 18:26):

My instinct about a floor semiring is that it should just be a floor ring without the - and in particular the floor will be int valued.

Yaël Dillies (Jun 05 2021 at 18:47):

Yes, I have the same instinct. But then the floor_ring ceil is defined as -floor (-x) and that's not really usable as a definition anymore.

Kevin Buzzard (Jun 05 2021 at 19:04):

That's interesting, because $\R_{\geq0}$ has a perfectly good notion of ceil.

Yaël Dillies (Jun 05 2021 at 19:06):

Yes absolutely. But I think this is related to $\R_{\ge 0}$ being archimedean.

Yaël Dillies (Jun 05 2021 at 19:06):

But don't forget that we get to specify the floor function. So the ceil function has to stem from floor somehow.

Kevin Buzzard (Jun 05 2021 at 19:06):

The commutative additive monoids satisfying this cancellation law a+b=a+c -> b=c are precisely the commutative additive monoids which are submonoids of commutative additive groups. So one could then ask the same question: if you have a semiring with an int-valued floor and it satisfies additive cancellation, does the associated ring that you get by "formally adding negatives" also get a floor ring structure? This is just the same ceil question in disguise.

Yaël Dillies (Jun 05 2021 at 19:25):

I'm tempted to say yes but this sounds a bit tricky because negating floor makes it into a ceil (I guess that was your point). So maybe using ceil x = floor x or floor x + 1 is an alternative?

Yaël Dillies (Jun 05 2021 at 19:25):

Tangent question does floor_ring imply archimedean?

Mario Carneiro (Jun 05 2021 at 20:12):

perhaps not directly but they are closely related (in the same file, even)

Kevin Buzzard (Jun 05 2021 at 20:13):

@Calle Sönne thought about this sort of thing. What started off as a simple-looking project to define decimal expansions of real numbers in lean (something which might still not be done!) turned into a rabbit hole of trying to figure out precisely which rings had some kind of notion of expansion of this kind and ultimately I think we came up with some pretty weird examples of floor rings but I can no longer remember them. Maybe Calle still can

Mario Carneiro (Jun 05 2021 at 20:14):

actually they aren't in the same file anymore. docs#archimedean.floor_ring shows that an archimedean ring is a floor ring but I don't see the converse in the library

Kevin Buzzard (Jun 05 2021 at 20:16):

I'm pretty sure that if it's not there then we knew an example where it wasn't true

Mario Carneiro (Jun 05 2021 at 20:18):

I think it should be true, although the proof might rely on an additional assumption like being a field so that you get the simplified characterization of archimedean

Mario Carneiro (Jun 05 2021 at 20:20):

it follows pretty directly from archimedean_iff_rat_le and le_ceil

Kevin Buzzard (Jun 05 2021 at 20:20):

I think Calle and I spent some time thinking about noncommutative floor rings, eg add two non-commuting polynomial variables to the integers and make them infinitesimally small

Kevin Buzzard (Jun 05 2021 at 20:20):

We definitely weren't restricting to fields

Kevin Buzzard (Jun 05 2021 at 20:21):

We had examples where the decimal expansion of a number didn't converge to the number etc

Mario Carneiro (Jun 05 2021 at 20:21):

It might not be an instance because you need to say something like floor_ring + field that would be a diamond

Floris van Doorn (Jun 06 2021 at 07:56):

This thread is relevant:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/subtraction.20in.20canonically_ordered_add_monoid
I wanted to define truncated subtraction ("monus") for all canonically ordered monoids.
I started on it, but at that time it was very hard, since I needed a lot more classes to prove specific properties about this subtraction (in a good amount of generality). I am planning to retry with all the new ordered-monoid classes we recently got.

Yaël Dillies (Jun 06 2021 at 08:46):

Ah great!

Last updated: Dec 20 2023 at 11:08 UTC