int.mod_by_nat

Stream: Is there code for X?

[Bolton Bailey]

I was a bit surprised to see the type signature of docs#int.nat_mod is Z -> Z -> N. Do we have an int/nat modulus operation of the form Z -> N -> N?

[Junyan Xu]

Maybe just do

import data.zmod.basic
variables (a : ℤ) (b : ℕ)
#check (a : zmod b).val

If b = 0 it would give you the absolute value of a.

[Adam Topaz]

what would you expect (-3) % 0 to be?

[Adam Topaz]

python gives me a division by zero error, but lean is happy to say that (-3) % 0 is -3 (which is the only reasonable answer IMO)

[Bolton Bailey]

I would expect (-3) % 0 to be 0 probably, but I wouldn't really care. What would you expect (-3).nat_mod 0 to be?

[Adam Topaz]

I don't think nat_mod should exist in the first place :rofl:

[Bolton Bailey]

Well, it's used a few times in mathlib. As far as I can tell each time the second argument is a nat cast to an int.

[Bolton Bailey]

Seems perfectly normal to me, I just want to extend % on naturals to also work when the first argument is an integer.

[Adam Topaz]

But % does work on ints

[Bolton Bailey]

I don't want to see a bunch of casts when my second argument is a nat, but fair enough.

[Bolton Bailey]

Actually wait no, it's important to me that the return type is a nat too.

[Adam Topaz]

So you can compose with docs#int.nat_abs

[Adam Topaz]

Or with docs#int.to_nat

[Adam Topaz]

Depending on the behavior you want for negative integers

[Adam Topaz]

docs#int.has_mod (since I'm on mobile)

[Bolton Bailey]

This is exactly what docs#int.nat_mod does

[Adam Topaz]

Aha okay. Well hopefully one little cast in the second variable isn't that bad?

[Bolton Bailey]

I guess not. I agree that nat_mod shouldn't exist, but I think if only one of nat_mod and mod_by_nat were to exist, it should be the latter.

[Bolton Bailey]

The point is that the % of int calls nat_abs on its second argument anyway, so better to write x.mod_by_nat |y| less often than x.nat_mod (y : \Z) more often. But also nat_mod is in core, so I can't get rid of the old way.

[Bolton Bailey]

docs#int.mod