Refactoring multiplicity

Stream: mathlib4

[Daniel Weber]

Would refactoring docs#multiplicity to be noncomputable and return values in ℕ∞ instead of PartENat be good?

[Edward van de Meent]

i seem to recall that removing PartENat in favour of ℕ∞ is somewhere on the list of todos, but i could be wrong.

[Geoffrey Irving]

Why would ℕ∞ make it noncomputable?

[Yaël Dillies]

because you can't know whether a finite value satisfying the predicate exists, and PartENat nicely avoids that issue by making equality with ∞ be noncomputable instead

[Antoine Chambert-Loir]

What is the gain in this modification ?

[Daniel Weber]

PartENat is really annoying to work with

[Daniel Weber]

Another option is to have it return values in Nat, with a junk value when it's infinite

[Michael Stoll]

See also here.

[Riccardo Brasca]

I am not 100% the junk value solution will work well, since (for example) having multiplicity 0 is a meaningful concept. But it also true that working with multiplicity now is a little pain.

[Daniel Weber]

Perhaps we could have both versions, like with dist and edist and degree and natDegree?

[Ruben Van de Velde]

In the unix style, we could use Int and return -1 as a junk value

[Riccardo Brasca]

Ruben Van de Velde said:

In the unix style, we could use Int and return -1 as a junk value

I would really like to be able to write p^(multiplicity p n)...

[Daniel Weber]

Perhaps 1 makes more sense as a junk value? This keeps multiplicity p n = 0 ↔ ¬p ∣ n

[Daniel Weber]

Although it breaks multiplicity a 1 = 0

[Johan Commelin]

I think it's fine to have two versions. We could rename the current version to eMultiplicity to free up multiplicity. Or we could have a new concept called natMultiplicity.

[Johan Commelin]

Riccardo Brasca said:

I would really like to be able to write p^(multiplicity p n)...

I agree, and right now you can't do that either, right? Because you can't raise something to the power k : partEnat.

[Johan Commelin]

Maybe we should have a Part.get! and a partEnat.get! that return junk (read: default) values. If we do that, we're sorta forced to use 0` as junk value.

[Daniel Weber]

I'm trying to create a natMultiplicity, but I'm unsure how general stuff should be. docs#le_multiplicity_map, for instance - should it take Finite (f a) (f b), or the weaker Finite a b → Finite (f a) (f b)?

[Kevin Buzzard]

Surely it should just be exactly as general as the corresponding multiplicity stuff?

[Daniel Weber]

Yes, but this creates a problem in theorems like docs#multiplicity_eq_multiplicity_iff - I need to take an assumption like Finite a b ↔ Finite c d.

[Kevin Buzzard]

Oh I see -- the corresponding theorem really isn't true. I get your point now.

[Kevin Buzzard]

The problem with the weaker assumption is that probably in practice I'll have h1 : Finite a b and h2 : Finite c d and I don't really want to be faced with a proof obligation that they're logically equivalent. My instinct is just to assume basic finiteness assumptions needed to make the theorems true i.e. Finite a b and Finite c d. If people want more general versions then they can add them later.

[Edward van de Meent]

import Mathlib
variable (A B : Prop)

example (a:A) (b:B) : A ↔ B := by tauto

besides the point, but proving that they're equivalent is easy?

[Edward van de Meent]

(assuming you do indeed have proofs of both)

[Daniel Weber]

Yes, but doing it every time it you're doing a bunch of rewrites can be annoying

[Edward van de Meent]

fair

[Daniel Weber]

What's docs#has_dvd.dvd.multiplicity_pos ? Is this something that was missed in the port?

[Daniel Weber]

docs3#has_dvd.dvd.multiplicity_pos

[Kevin Buzzard]

I see -- it's enabling dot notation for a terms of a type which was since renamed :-/

[Filippo A. E. Nuccio]

I remember discussing this with @Sébastien Gouëzel who agreed that this PartENat is painful. I would be very much in favour of having multiplicity valued in ℕ∞ as the default, and if needed to keep both verisons.

[Riccardo Brasca]

Johan Commelin said:

Riccardo Brasca said:

I would really like to be able to write p^(multiplicity p n)...

I agree, and right now you can't do that either, right? Because you can't raise something to the power k : partEnat.

Yes, it is already a pain. I think that having two versions is a good idea. Maybe a typeclass saying that the multiplicity of all nonunits (or whatever it is needed) is always finite.

[Daniel Weber]

I refactored to an ℕ-valued version at branch#CM_multiplic, if anybody wants to take a look

[Daniel Weber]

#16881

[Daniel Weber]

hmm, this makes docs#padicValNat noncomputable

[Daniel Weber]

I'm uncertain what to do with the results in Data.Nat.Multiplicity - should they use emultiplicity or multiplicity?

[Riccardo Brasca]

I would say multiplicity, but which one requires less dependencies?

[Daniel Weber]

They are in the same file

[Matthew Ballard]

Daniel Weber said:

hmm, this makes docs#padicValNat noncomputable

The csimp on docs#padicValNat.padicValNat_eq_maxPowDiv restores code generation

[Eric Wieser]

There was a suggestion elsewhere to just implement padicValNat from scratch to be kernel reducible, which could make it computable at the same time.

[Daniel Weber]

#16881 passes CI now! If anybody is able to review it that'd be great

[Kevin Buzzard]

That's quite a large diff! However perhaps this is inevitable, and changes like

padic.png

make me feel like it's making mathlib more readable. Also the removal of random [@DecidableRel R[X] (· ∣ ·)]s makes me happy too, although I'm very much on the noncomputable side of things when it comes to mathlib decisions.

[Riccardo Brasca]

I think that the way to go is the following: do we agree we want both version? I personally do. If this is the case you can split the PR in at least two: first of all just rename multiplicity to emultiplicity, without adding anything else, and in a following PR add the new multiplicity.

[Michael Stoll]

I agree that it makes sense to have both emultiplicity (ENat-valued) and a Nat-valued multiplicity. Getting tid of docs#PartENat is definitely a good thing!

[Kevin Buzzard]

Do we need to split the PR into two? A lot of the diff is just renaming lemma names. I've just ploughed through all of it because like Michael I have always found it hard to work with PartENat.

[Riccardo Brasca]

Maybe not, I was just suggesting a way of making the diff smaller.

[Daniel Weber]

Riccardo Brasca said:

I think that the way to go is the following: do we agree we want both version? I personally do. If this is the case you can split the PR in at least two: first of all just rename multiplicity to emultiplicity, without adding anything else, and in a following PR add the new multiplicity.

You mean while keeping PartENat?

[Riccardo Brasca]

I forgot there is also this change. Making several PRs makes the review process easier, but it means more work for you, so a trade-off of probably the way to go. But anyway I think we should decide this (having both versions) is the solution we want.

[Daniel Weber]

Another option is to use multiplicity and natMultiplicity instead of emultiplicity and mutliplicity, and then less renames are needed

[Daniel Weber]

Another thing of note in the PR is moving many results outside of the multiplicity namespace, as they all had to be renamed anyway to have either multiplicity or emultiplicity to disambiguate, so the namespace was redundant

[Yaël Dillies]

Daniel Weber said:

Another option is to use multiplicity and natMultiplicity instead of emultiplicity and mutliplicity, and then less renames are needed

Yes but I think this goes against the principle of making the main things have shorter names

[Yaël Dillies]

Daniel Weber said:

Another thing of note in the PR is moving many results outside of the multiplicity namespace, as they all had to be renamed anyway to have either multiplicity or natMultiplicity to disambiguate, so the namespace was redundant

I always hated that namespace. It's not a type! Happy to see it go

[Daniel Weber]

There are still some remains, mostly multiplicity.Finite and a few other lemmas

[Daniel Weber]

@Yaël Dillies said:

Daniel Weber said:

Another thing of note in the PR is moving many results outside of the multiplicity namespace, as they all had to be renamed anyway to have either multiplicity or natMultiplicity to disambiguate, so the namespace was redundant

I always hated that namespace. It's not a type! Happy to see it go

#19623 eliminates that namespace completely (up to deprecated aliases), renaming multiplicity.Finite to FiniteMultiplicity

[Johan Commelin]

I think this is a good move. But I do find FiniteMultiplicity a rather long name. We also have things like fincard, so how about FinMultiplicity? Or possibly NatMultiplicity?