Submonoid of elements smaller than one

Stream: mathlib4

[Albus Dompeldorius]

Should the submonoid of elements smaller than one be added to mathlib? There is already Submonoid.oneLE, which is the submonoid of elements greater than one.

Here is a straight-forward adaption:

/-- The submonoid of elements that are at most `1`. -/
@[to_additive (attr := simps) "The submonoid of nonpositive elements."]
def le_one : Submonoid M where
  carrier := Set.Iic 1
  mul_mem' := mul_le_one'
  one_mem' := le_rfl

variable {M}

@[to_additive (attr := simp)] lemma mem_le_one : a ∈ le_one M ↔ a ≤ 1 := Iff.rfl

[Eric Wieser]

It should be called leOne, but this otherwise seems reasonable

[Albus Dompeldorius]

In that case, to_additive generates the name leZero instead of nonpos (the corresponding oneLE generates nonneg). I could force to_additive to generate nonpos, making it consistent with the existing code, like this:

/-- The submonoid of elements that are at most `1`. -/
@[to_additive (attr := simps) nonpos "The submonoid of nonpositive elements."]
def leOne : Submonoid M where
  carrier := Set.Iic 1
  mul_mem' := mul_le_one'
  one_mem' := le_rfl

variable {M}

@[to_additive (attr := simp) mem_nonpos] lemma mem_leOne : a ∈ leOne M ↔ a ≤ 1 := Iff.rfl

Does this look good?

[Eric Wieser]

Yes, that looks good to me

[Floris van Doorn]

You can also teach to_additive to automatically suggest the correct name by modifying this definition and adding a line

  | "le" :: "Zero" :: s        => "nonpos" :: fixAbbreviation s

[Albus Dompeldorius]

Floris van Doorn said:

You can also teach to_additive to automatically suggest the correct name...

Yeah, I was thinking that this could be done. That is probably the best approach. Thanks for providing the appropriate rule.

[Albus Dompeldorius]

Floris van Doorn said:

  | "le" :: "Zero" :: s        => "nonpos" :: fixAbbreviation s

Unfortunately, this causes a collision with the following rule:

  | "le" :: "Zero" :: "Part" :: s         => "negPart" :: fixAbbreviation s

Perhaps I should just hardcode nonpos after all.

[Eric Wieser]

That won't be a collision as long as you put your case after that one

[Albus Dompeldorius]

BTW, shouldn't leZeroPart become nonposPart, and so on anyway, for consistency? I guess there is a tradeoff between consistency and simplicity here.

[Floris van Doorn]

I don't think we want to change the name of something we use frequently to slightly simplify an internal function nobody looks at.

[Albus Dompeldorius]

Makes sense!

[Yury G. Kudryashov]

Floris van Doorn said:

You can also teach to_additive to automatically suggest the correct name by modifying this definition and adding a line

  | "le" :: "Zero" :: s        => "nonpos" :: fixAbbreviation s

If we do changes like this one, should we verify if any of @[to_additive]-generated names changed and add deprecated aliases?

[Albus Dompeldorius]

I implemented the code here: https://github.com/leanprover-community/mathlib4/tree/adompeldorius/leOne

The checks passed, but I guess it is still possible that some @[to_additive]-generated names have changed, if the generated code is not used by any other code in mathlib. Is it possible to get a diff of generated code after a commit?

[Yury G. Kudryashov]

I have a local branch with mostly forward-ported leaff locally. I'll try to fix the remaining issues and run it on your branch tomorrow.

[Yury G. Kudryashov]

Please remind me if I don't report back in 48h.

[Albus Dompeldorius]

Thank you so much!

[Albus Dompeldorius]

@Yury G. Kudryashov Hi, did you have a chance to check the diff? I could also try doing it myself. I guess my change is small enough that it would be also possible to just generate the olean files and do a regular diff.