Modeq name

Stream: mathlib4

[Henrik Böving]

What would you want the name of modeq to be in Lean 4? Modeq or ModEq? I think the latter makes more since

Furthermore I'm having a little issue with the definition:

def Modeq (n a b : ℕ) :=
  a % n = b % n deriving Decidable

It cannot derive Decidable do we want to treat this as a bug and fix it upstream in the compiler or shall I write a manual instance?

[Mario Carneiro]

delta deriving is still todo, it needs some upstream changes

[Mario Carneiro]

the workaround is to write the instances manually (with a Porting note), you probably can't just skip them since later things will need those instances

[Mario Carneiro]

ModEq seems like a fine name to me

[Henrik Böving]

Oh I also have to write a manual Trans instance. Could it be that we want a abbrev ModEq instead of a def ModEq?

[Heather Macbeth]

In mathlib3, for teaching, I actually used attribute [irreducible] on the def for modeq, because the definition is so unintuitive that I wanted to prevent the students from ever accidentally encountering it.

[Henrik Böving]

The definition is unintuitive? This is the only definition i have ever been taught and can think of to be honest :D How would you go about defining this?

[Heather Macbeth]

So that's a vote in the opposite direction from abbrev -- I don't think we have any policy of taking teaching preferences into account for mathlib, though.

[Heather Macbeth]

Henrik Böving said:

The definition is unintuitive? This is the only definition i have ever been taught and can think of to be honest :D How would you go about defining this?

I'm thinking of int.modeq rather than nat.modeq, but the definition I teach in class is

def int.modeq (n a b : ℤ) := n ∣ (a - b)

[Heather Macbeth]

It's easier to reason about -- no case splits in proofs.

[Henrik Böving]

Interesting. As a programmer I think of modeq as "the remainders are equivalent" which is exactly what the mathlib definition mirrors and when I explain students for example the RSA algorithm I can explain a \equiv b \pmod n as "This is just notation for putting the modulo on both sides" but I guess if you are building the mathematics up instead of just using all the nice modulo properties your approach might be easier.

[Heather Macbeth]

Indeed, I think in many mathematical theories there's a difference between what's easy when building the theory and what's easy when using it.

[Heather Macbeth]

Incidentally, there's no analogue of attribute [irreducible] in Lean 4, right? Is there any other way to hide a definition post-facto? (Maybe someone can point me to a previous discussion of this design decision?)

[Henrik Böving]

attribute [irreducible] ModEq would work out without any issues.

[Heather Macbeth]

Oh, great! I wonder what I was thinking of? I thought I had heard that it was no longer possible to mark definitions as irreducible after the fact.

[Henrik Böving]

From what I have seen in this stream it seems like the attribute feature in Lean 4 is either equivalent or actually a teeny bit better than in Lean 3 in what it allows you to do. There are a few syntax changes but in general everything I've seen from Lean 3 with attribute so far should work in Lean 4 as well.

[Heather Macbeth]

Hmm ... do you know what Mario was referring to here?

Mario Carneiro said:

Like I said in the meeting, attribute [irreducible] is just plain not supported in lean 4

[Henrik Böving]

Hm no, when i applied attribute [irreducible] just now I actually saw some proofs failing such as the fact that the Trans instance of Eq can be trivially used to prove one for ModEq and so on. So it does work and have an effect as well.

[Kevin Buzzard]

@Mario Carneiro explained in the meeting that allowing declarations to become irreducible after the fact meant that some dsimp lemmas about the declarations would...now no longer typecheck...or something? So it was a bad idea?

[Patrick Massot]

Henrik Böving said:

What would you want the name of modeq to be in Lean 4? Modeq or ModEq? I think the latter makes more since

Furthermore I'm having a little issue with the definition:

def Modeq (n a b : ℕ) :=
  a % n = b % n deriving Decidable

It cannot derive Decidable do we want to treat this as a bug and fix it upstream in the compiler or shall I write a manual instance?

This definition is really crazy. Why on earth would anyone want to make this so complicated when the mathematical definition is so nice?

[Kevin Buzzard]

Re modeq -- why not just prove int.modeq_def (n a b : ℤ) : int.modeq n a b : ℤ <-> n ∣ (a - b) := ... and tell them to rewrite the definition?

[Henrik Böving]

Patrick Massot said:

Henrik Böving said:

What would you want the name of modeq to be in Lean 4? Modeq or ModEq? I think the latter makes more since

Furthermore I'm having a little issue with the definition:

def Modeq (n a b : ℕ) :=
  a % n = b % n deriving Decidable

It cannot derive Decidable do we want to treat this as a bug and fix it upstream in the compiler or shall I write a manual instance?

This definition is really crazy. Why on earth would anyone want to make this so complicated when the mathematical definition is so nice?

As explained above I would say the exact same to your definition :sweat_smile:

[Patrick Massot]

Seriously, we can't take the remainder thing as the definition. The fact that this definition works for natural number is a completely meaningless accident.

[Henrik Böving]

Also another question, is there a particular reason that Nat.mod_zero is not @[simp] anymore?

[Henrik Böving]

Oh I'm seeing it's a built-in theorem so I probably better ask the person that wrote it.

[Patrick Massot]

Henrik, who did that to you? We need a name. Who inflicted that definition on you?

[Kevin Buzzard]

The reason the computer scientists like the definition is that they constantly think of things as subsets, they have a fear of quotients because of implementation issues. They are just choosing a fixed "representative" element in each equivalence class and defining a pathological function taking each element to the representative of the equivalence class. Mathematicians find these functions weird because they are not at all canonical, they don't have natural properties like f(a+b)=f(a)+f(b) and we'd rather use quotients than these ugly representatives.

[Patrick Massot]

I understand that fear, but it isn't relevant here. When defining the relation you don't need anything like a quotient.

[Henrik Böving]

Patrick Massot said:

Henrik, who did that to you? We need a name. Who inflicted that definition on you?

That would be Professor Eich-Soellner. This nice looking lady: image.png

[Kevin Buzzard]

A relation on a type can be defined by a function from the type (two things are related if their images are equal), and they choose to define the relation this way via a "non-canonical" map from nat to nat sending each element in the equivalence class to the representative. This makes the non-canonical map kind of embedded in the definition, making it much more difficult to work with.

[Matthew Ballard]

Isn't $\mathbb{Z}$ (really) a quotient of $\mathbb{N} \times \mathbb{N}$?

[Patrick Massot]

I do not dare asking whether she defines divisibility using the remainder operation.

[Henrik Böving]

My lecture notes say no!
image.png

[Kevin Buzzard]

I've worked through the definition of Int as a quotient of Nat \times Nat in Lean 3 and there is a terrifying 8-variable Grobner basis roblem in ring theory you need to do when proving something about multiplication, and nlinarith does it. But if you look at the term it generates, it uses mathlib's inbuilt Int which is presumably still the non-canonical definition. If the CS guys are happy to write the API and battle through the non-canonical functions like of_neg_of_nat then surely they can have any implementation they want?

[Patrick Massot]

That's a relief.

[Patrick Massot]

At least you'll be able to bring that bit to other rings.

[Henrik Böving]

Kevin Buzzard said:

I've worked through the definition of Int as a quotient of Nat \times Nat in Lean 3 and there is a terrifying 8-variable Grobner basis roblem in ring theory you need to do when proving something about multiplication, and nlinarith does it. But if you look at the term it generates, it uses mathlib's inbuilt Int which is presumably still the non-canonical definition. If the CS guys are happy to write the API and battle through the non-canonical functions like of_neg_of_nat then surely they can have any implementation they want?

As a cs guy that does not know what a Grobner basis is I would like to avoid that if possible maybe :P

[Kevin Buzzard]

It was a problem of the form "a,b,c,d,e,f,g,h are nats, and a+b=c+d and e+f=g+h and a*b+c*d+blah blah blah = c * f + d * e + ..., and other polynomial identities are also true, and the goal is some other random equality of polynomials"

[Kyle Miller]

@Henrik Böving One of the issues with using a remainder-after-division to define modulo-equality is that you need to choose which remainder to use for normalization. For nat/int this is relatively clear what to use, but modulo congruence still is meaningful for other rings where you don't have a good way to normalize your div/mod.

Even in CS there are confusions about div/mod, since there are two main conventions: is division from rounding toward zero or toward negative infinity? The Lean % operator uses the second convention, but C uses the first. Haskell has functions for both.

[Henrik Böving]

Kyle Miller said:

Henrik Böving One of the issues with using a remainder-after-division to define modulo-equality is that you need to choose which remainder to use for normalization. For nat/int this is relatively clear what to use, but modulo congruence still is meaningful for other rings where you don't have a good way to normalize your div/mod.

Even in CS there are confusions about div/mod, since there are two main conventions: is division from rounding toward zero or toward negative infinity? The Lean % operator uses the second convention, but C uses the first. Haskell has functions for both.

My math classes trivially solve this issue by not telling us that a ring is a thing even :(

[Kyle Miller]

It would be great if eventually the modeq for Int was just n ∣ (a - b) (that's practically better two -- just one division rather than two to implement!)

When I've thought about this before (and I think this is what Heather is referring to), for Nat you can't get much better than a % n = b % n since we have truncating subtraction. You could do n ∣ (max a b - min a b) at least...

[Kevin Buzzard]

natural and integer division are also pathological functions (they don't satisfy nice theorems because of rounding errors) and the identity is not a pathological function, and neither is multplication, therefore the remainder function must also be pathological because a=(a/b)*b+a%b

[Kevin Buzzard]

They're implementation issues and shouldn't be exposed ;-)

[Kyle Miller]

@Henrik Böving That doesn't solve the issue since you still have to choose your division rounding convention for normalization :wink:

At least they all satisfy a = div a b * b + mod a b for whatever choices of div and mod. (Given the div, you define mod this way)

[Henrik Böving]

I can't remember ever choosing a rounding convention even, we kinda just...went with it?

[Kevin Buzzard]

The definition should be (n : \Z) | a - b ;-)

[Kyle Miller]

When you assert that 0 <= mod a b < abs b you've said you're rounding to negative infinity since that means a >= div a b * b

[Kevin Buzzard]

Henrik Böving said:

I can't remember ever choosing a rounding convention even, we kinda just...went with it?

Henrik do you know about the issue where a random change in convention for integer division from Lean 3 to Lean 4 caused problems for mathlib4?

[Henrik Böving]

Yes I did see the chats about it.

[Yury G. Kudryashov]

So, do you suggest that we define int.modeq first, then define nat.modeq using int.modeq?

[Henrik Böving]

I'm not denying all of this is an issue or saying that you are wrong with your ideas of how to do things don't get me wrong^^ I'm just explaining the way I was taught. I'm very much aware that most of the mathematics I'm being taught in the style they are by my university is far far away from anything close to the rigor you would expect.

[Henrik Böving]

Which is part of the reason I'm doing mathlib porting work in the first place to be honest.

[Kevin Buzzard]

To be honest I have only recently started paying attention to the way logic and mathematics are taught to computer scientists, and I was really surprised by some of the things I saw.

[Kyle Miller]

@Henrik Böving I first learned about the modulo operator in QBasic and then used that intuition when learning about modulo congruence, which gave me the same sort of operational understanding, where int.modeq n a b is something you evaluate by modulo reducing a and b then checking equality. It took awhile before I really got that in math it's fine having relations that don't need to have computational content, which moving toward n ∣ (a - b) (or "there exists a k such that a = b + k * n") helped me with.

[Kyle Miller]

The latter point of view also makes it more obvious that the "point" of congruence is that it's that you're wanting to work with numbers ignoring differences by multiples of the modulus, which the operational point of view obscures.

[Henrik Böving]

Oh I'm perfectly content with these types of definitions. I can actually remember kind of intuitively using the 2nd one a couple of times while writing proofs.

[Kyle Miller]

@Kevin Buzzard Your idea about defining nat.modeq in terms of int.modeq made me wonder if we need nat.modeq at all. I can't immediately think of a reason for it that can't be served by just writing Nat-specialized lemmas for int.modeq.

[Kevin Buzzard]

Ha ha yeah that would be an interesting refactor! That's kind of weird that the way which seems to me to be more natural involves doing int before nat. It wouldn't surprise me if it ended up cleaner, a non-pathological subtraction makes proofs much easier.

[Henrik Böving]

https://github.com/leanprover-community/mathlib4/pull/1274

[Yury G. Kudryashov]

Kevin Buzzard said:

Ha ha yeah that would be an interesting refactor! That's kind of weird that the way which seems to me to be more natural involves doing int before nat. It wouldn't surprise me if it ended up cleaner, a non-pathological subtraction makes proofs much easier.

Especially if we reuse general theory about, e.g., docs#con.

[Reid Barton]

Kevin Buzzard said:

Henrik Böving said:

I can't remember ever choosing a rounding convention even, we kinda just...went with it?

Henrik do you know about the issue where a random change in convention for integer division from Lean 3 to Lean 4 caused problems for mathlib4?

In fact, if the % definition is used for int.modeq with the Lean 4 core definition of %, then the definition is simply wrong (positive and negative numbers won't be modeq modulo anything).

[Reid Barton]

Oh unless they happen to be divisible by the modulus.

[Yury G. Kudryashov]

So, a % n is incompatible between Lean 3 and Lean 4?

[Yury G. Kudryashov]

(for integer a n)

[Reid Barton]

Yes but mathlib4 fixes this by overriding the appropriate instance (and the hope is to merge the change into Lean 4 eventually).

[Yaël Dillies]

I would be happy with a refactor wiping nat.modeq out of existence in favor of int.modeq, but isn't there a more general ideal.modeq to be had?

[Yaël Dillies]

Or are we deciding to draw the line between theory building and simplicity of definition there?

[Yury G. Kudryashov]

We don't have subgroup.modeq...

[Heather Macbeth]

For the record, defining int.modeq in terms of subgroups is far worse for teaching than defining it in terms of % ...

[Reid Barton]

Subgroups? you probably won't be so lucky...

[Kevin Buzzard]

I want to define it in terms of divisibility and I've taught it like that and it worked out great.

[Kyle Miller]

Reid Barton said:

(and the hope is to merge the change into Lean 4 eventually).

I hope so! I didn't realize Lean 4 switched from the "Python convention" to the "C convention." The Python convention is (in just my opinion) the correct one, in that it always gives a modulus in the range 0, 1, ..., n-1 when n is positive, so you can for example write a[i % len(a)] no matter what the integer i is.

#eval (-5) % 3
-- -2

Of course this also means that division is rounding toward zero rather than negative infinity:

#eval (-5) / 3
--- -1

I believe we should have both div/mod conventions in some capacity. It's just a question of what convention the operators / and % use.

[Kyle Miller]

As a case study, Haskell chose to have two pairs of functions for integers: div/mod for the "Python convention", and quot/rem for the "C convention." It doesn't supply operators for these, but Haskell also has a feature for using two-argument functions as binary operators, for example 5 `div` 3 for div 5 3.

[Reid Barton]

https://leanprover.zulipchat.com/#narrow/stream/341532-lean4-dev/topic/.5BRFC.5D.20Int.2Ediv.20convention/near/296956937