basic facts for `fmod` for negative second argument

Stream: Is there code for X?

[Moritz Firsching]

While doing #14756, I need some basic theorems on fmod, namely

theorem lt_fmod_of_pos (a : Int) {b : Int} (h : b < 0) : b < a.fmod b := sorry

and

theorem fmod_nonpos (a : Int) {b : Int} (h : b < 0) : a.fmod b ≤ 0 := sorry

Did I miss to find them somewhere? I was also looking for anything that has a.fmod -b for a positive or nonnegative b, but didn't find anything. Maybe they even follow trivially from stuff in the library and I'm missing it.
If we don't have this, where would be a good place to put those facts on fmod?

[Kim Morrison]

Could you #xy and explain why fmod is relevant here in the first place? We otherwise don't touch it in Mathlib.

[Moritz Firsching]

Sure, the reason why I was looking at fmod is because this theorem

theorem fract_div_intCast_eq_div_intCast_mod {m : ℤ} {n : ℕ} : fract ((m : k) / n) = ↑(m % n) / n :=

can be generalized to have an integer {n : ℤ} instead of the {n : ℕ} for the second argument.
But then m % n needs to be replaced by m.fmod n, at least this was suggested in a todo. Assuming this generalization makes sense, then I started proving it and found myself needing those two lemmas above.
This could really be a case of #xy, perhaps the generalization should use something other than Int.fmod?

[Kim Morrison]

Why not use emod, like the rest of Mathlib?

[Yury G. Kudryashov]

Because you want the numerator to be negative, if n is negative.

[Moritz Firsching]

yes, I think the definition of fract seems to be more compatible with fmod, I haven't managed to come up with a generalization using emod.

[Ruben Van de Velde]

I might wonder if the generalisation is worth it in that case

[Moritz Firsching]

Perhaps not then

[Moritz Firsching]

If we the generalization is not worth it, then I think might want to delete the TODO
https://github.com/leanprover-community/mathlib4/blob/496527772ac807ef3d1ddd4868f2048f9ea478e1/Mathlib/Algebra/Order/Floor.lean#L1047
. This was added by @Oliver Nash .
What do you think: delete TODO or generalize? The work to generalize it is pretty much done in #14756, except for a little cleanup and golf and finding better places for intermediate results.

[Oliver Nash]

I'm sorry for writing that TODO, and for the fact that you have invested non-trivial time implementing it. I agree with the comments above that we should not be building API for Int.fmod in Mathlib and should just excise the remark.

[Moritz Firsching]

No problem at all, I'll make the PR simply removing the todo later

[Moritz Firsching]

done, opened #19652, closing  #14756

[Eric Wieser]

Oliver Nash said:

we should not be building API for Int.fmod in Mathlib and should just excise the remark.

I think it's sensible to build as much API as is needed to translate to the preferred spelling that uses floor, so since Moritz already seemingly did the work, I think we should try to merge the generalized version.

[Oliver Nash]

Unless I mistake, we currently have no use of docs#Int.fmod in Mathlib and can use docs#Int.floor anywhere we might want to express it. Surely we should just avoid supporting what is essentially a redundant spelling?

[Eric Wieser]

The argument would be that if we have some algorithm written in Lean (core) using fmod, it would be nice to be able to prove things about it using Mathlib. We don't need a large API for fmod for that, but we do need lemmas to turn fmod into something we have API for.

[Eric Wieser]

Or phrased another way; our mechanisms for redundant spellings are:

1. Delete the spellling (not possible here)
2. Create a (simp) lemma that turns the unwanted spellling into the preferred one

[Oliver Nash]

I agree with these remarks at a logical level but this seems to me like quite a theoretical benefit. I feel like our bandwidth is better spent reviewing and maintaining the many definitely-valuable additions to Mathlib.

Notwithstanding the above, I don't have especially strong feelings and I certainly won't object if someone else does.

[Kim Morrison]

My preference is that Mathlib avoids mentioning fmod entirely. None of its business. :-)

[Mario Carneiro]

If a definition like fmod exists in lean+batteries+mathlib, I want to see enough characterizing lemmas for it in lean+batteries+mathlib. I don't care where it is, but it should exist

[Kim Morrison]

Yes, I agree. But please not Mathlib for things like fmod. I would happily merge PRs to Batteries with any reasonable material about fmod, and PRs to Lean that increase the uniformity of the treatment of emod/fmod/tmod/bmod.

[Eric Wieser]

If we want a lemma that translates fmod to Int.floor, it has to live in Mathlib. The helper lemmas to get there could probably survive in Batteries.