fin n with saturating addition

Stream: Is there code for X?

[Johan Commelin]

There has been talk about having a version of fin n with saturating addition. Do we actually have this somewhere? cc @Gabriel Ebner

#12485 needs it in the case n = 2. cc @Jujian Zhang

[Gabriel Ebner]

I don't think we have a saturating version of fin yet, but it would of course be nice.

[Yaël Dillies]

cc @Yakov Pechersky

[Gabriel Ebner]

We already have the special case n=2 though, it's called with_zero unit:

import algebra.punit_instances
example : (1 + 1 : with_zero unit) = 1 := rfl

[Kevin Buzzard]

We could of course use saturating addition as the default addition on fin given that zmod covers the mod n case :-)

[Gabriel Ebner]

We've had this discussion before, it's not going to happen because core Lean 4 uses modular arithmetic in Fin. We're going to have to find a new name for the saturating version.

[Yaël Dillies]

But why can't core Lean use zmod instead?

[Johan Commelin]

Gabriel Ebner said:

We already have the special case n=2 though, it's called with_zero unit:

import algebra.punit_instances
example : (1 + 1 : with_zero unit) = 1 := rfl

Thanks!
@Jujian Zhang I think you can probably use this to golf the first 70 lines from your PR.

[Vincent Beffara]

I thought the n=2 case was

instance : has_zero bool := ⟨ff⟩
instance : has_one bool := ⟨tt⟩
instance : has_add bool := ⟨(||)⟩

:grinning:

[Gabriel Ebner]

I think it would be a bit confusing if bool was not a Boolean ring.

[Yaël Dillies]

( bool.boolean_ring is something I'm working on btw)

[Yakov Pechersky]

#6149

[Yakov Pechersky]

You could probably also use "additive (tropical (fin n))" for your purposes at this point, that pr is old

[Gabriel Ebner]

The additive gets you back the original modular addition. Just tropical (fin 2) alone is enough to get saturating addition (but you'll have 0*0=1).

[Yakov Pechersky]

Ah, yes.

[Yakov Pechersky]

Wait why would 0*0=1 in tropical fin 2?

[Gabriel Ebner]

Because 0=1 and 1=0 and *=+ and 1+1=0 in fin 2. :smile:

[Yakov Pechersky]

Ah, one has to launder via (trop 0) and (trop 1), right

[Yakov Pechersky]

Well just tropical fin n, 2 < n won't work in general either for the sat addition because untrop ((trop 2) + (trop 3)) = 3, not 5 (in fin 7 let's say)