refactor(*): saturating fin addition

[pechersky]

The fin ops will be removed from core in leanprover-community/lean#527. This allows for redefining fin addition as saturating, as well as removing the extra unwanted operations.

To do so, some small changes are needed scattered around the library. The most dependent files: data/matrix/notation.lean and data/zmod/basic.lean, and tactic/norm_fin.lean required larger refactoring.

Once this is merged, further improvement of the fin API is possible.

---

• depends on: [Merged by Bors] - feat(algebra/ordered_monoid): min_*_distrib #6144
• depends on: [Merged by Bors] - feat(data/nat/basic): le_of_add_le_* #6145

To test this branch, I built the lean#527 branch locally and overrode the toolchain with the newly built dev lean.

The only files which currently have wrong proofs are data/matrix/notation.lean and data/zmod/basic.lean, with about 4 lemmas each. In general, some refactoring is needed for the notation simp lemmas that deal with numerals.

This PR is likely to bitrot quickly if not kept up with master.

[Vierkantor]

Since this is still a WIP/RFC, I'll just quickly note that I approve of the idea of saturating addition on fin. I will take a closer look at the code when the dependencies and holes are resolved.

[jcommelin]

I'm also happy with changing the defn of addition on fin.

[pechersky]

Since this is still a WIP/RFC, I'll just quickly note that I approve of the idea of saturating addition on fin. I will take a closer look at the code when the dependencies and holes are resolved.

Since you're the point person for the data/matrix/notation.lean file, is there any chance you could look at the lemmas in there? Or should we call on @jsm28 since he developed the simp technology for arbitrary numerals?

[Vierkantor]

I'm almost finished with some other work, then I'll take a look.

[jsm28]

The data/matrix/notation.lean simp lemmas deal with arbitrary numerals, rather than just those that are in range, for completeness rather than because out-of-range numerals are expected to be useful there.

On the other hand, the notation there seems appropriate in any case where fin n is being used as a generic index type for some vector of n things. And I've frequently seen indices used in informal mathematics where out-of-range indices are said to be taken mod n, and I don't think I've ever seen indices used with a convention where out-of-range indices are said to saturate. Is the expectation with saturating operations that anything using the convention of indices mod n should do all its arithmetic on nat (or int) and explicitly reduce mod n before converting back to fin n, rather than doing fin n arithmetic directly?

[Vierkantor]

There should be no problem with indexing your matrix over zmod n if you want wraparound. No conversion between index types needed.

[pechersky]

Is the expectation with saturating operations that anything using the convention of indices mod n should do all its arithmetic on nat (or int) and explicitly reduce mod n before converting back to fin n, rather than doing fin n arithmetic directly?

I think the consensus on Zulip was that there should be no arithmetic done on fin indices at all. We do need to have some form of addition to make numerals work. So the consensus on that was that modular arithmetic on numerals is counterintuitive, and a saturating numeral 10 : fin 3 would be equal to 2 : fin 3.

[Vierkantor]

OK, I worked on the notation for a bit, but it's not as simple as fixing a few lemmas: vec_alt0 (v : fin n → α) should now look like the even-indexed entries of v, followed by the same amount of repetitions of the final element of v. But then we want n to be positive to talk about "the final element". I'll return to it in a couple of hours, after I have dinner.

[Vierkantor]

Sorry, I'm not really feeling ready for a lot of thinking tonight. In about 12 hours I'll be back again, feel free to attempt the fix before then.

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - feat(algebra/ordered_monoid): min_*_distrib #6144
• [Merged by Bors] - feat(data/nat/basic): le_of_add_le_* #6145

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[gebner]

Can you link to the Zulip discussion about saturating addition on fin? I searched for saturating and modular, but couldn't find anything relevant.

To be honest, I think that this change is a bad idea. Or at the very least insufficiently motivated. What concrete problem does saturating addition solve? Or does it at least have nicer properties than modular arithmetic? Does the definition of addition even matter if we want to avoid arithmetic on fin n?

I find saturating arithmetic to be extremely surprising in mathematics. Also in indices, since you often have periodic extensions.

So the consensus on that was that modular arithmetic on numerals is counterintuitive, and a saturating numeral 10 : fin 3 would be equal to 2 : fin 3

Both are equally counterintuitive if you expect an error instead. I don't see how saturating addition improves anything here.

[pechersky]

Some discussions are at
https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F.20tactics/topic/Fetching.20all.20types.20with.20instances
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/fin.20simp.20normal.20form

I understand the concern that this isn't strongly motivated. Do we want to be able to provide numerical syntax for fin? How about supporting the (undesired) coercion from nat to fin? Should we, if not redefining add for fin, at least remove the other "arithmetic" definitions placed on it?

The saturating addition, in my mind, is a rephrasing of the complete total order that is on fin, where + 1 is just the directly larger element (a canonically_linear_ordered_add_monoid). The fact that we use + as the notation is unfortunate, where instead x ⊕ y = min x y; x ⊗ y = x + y are the operations involved. The current addition we have does not respect the lattice structure of fin.

Differentiating fin and zmod would also help avoiding use of one for the other, or abusing defeq of one for the other.

[jsm28]

A coercion from nat is useful even if you don't care whether it's modulo or saturating because all the values you coerce are in range; in that case, it allows doing arithmetic on nat before coercing and postponing the proof obligations (that the coerced value is in range and the so result is meaningful) until a more convenient point (rather than needing to include proof terms in the definition of a function that uses such coercions, for example).

[jcommelin]

I don't have a very strong opinion. As long as zmod stays the way it is, I don't really care how fin behaves arithmetically. It might make sense to have saturating addition, because we already have zmod for the modular one...