casting natural division to rat

Stream: Is there code for X?

[Jakob von Raumer]

Do we have a lemma for this or a lemma that would make such a lemma superfluous?

theorem Rat.nat_cast_div_eq {a b : ℕ} :
    ↑(a / b) = (a : ℚ) / (b : ℚ) - (a % b : ℚ) / (b : ℚ) := by
  by_cases hb : b = 0
  · subst hb; simp
  · rw [Nat.div_eq_sub_mod_div, Nat.cast_div (Nat.dvd_sub_mod a) (Nat.cast_ne_zero.mpr hb),
      Nat.cast_sub (Nat.mod_le a b), sub_div]

[Edward van de Meent]

why are you assuming z : ℚ?

[Jakob von Raumer]

Fixed :grinning_face_with_smiling_eyes:

[Richard Copley]

That proof doesn't work (because the statement isn't true) if you import Mathlib. Perhaps this has something to do with Mathlib redefining /.

import Mathlib

example {a b : ℕ} :
    ↑(a / b) = (a : ℚ) / (b : ℚ) - (a % b : ℚ) / (b : ℚ) ↔
      ((a / b : ℕ) : ℚ) = (a : ℚ) / (b : ℚ) := by
  by_cases hb : b = 0
  . subst hb ; simp
  rw [EuclideanDomain.mod_eq_sub_mul_div, div_sub_div_same, sub_sub_self, mul_div,
    mul_div_right_comm, mul_div_right_comm, ← Rat.coe_nat_div_self,
    Nat.div_self (Nat.pos_of_ne_zero hb), div_mul_comm, show ((1 : ℕ) : ℚ) = (1 : ℚ) from rfl,
    mul_one]

Did you have a set of imports where it does work?

[Jakob von Raumer]

This is a snippet that works stand-alone for me:

import Mathlib.Data.Rat.Basic
import Mathlib.Data.Nat.Order.Basic
import Mathlib.Data.Nat.Cast.Field
import Mathlib.Algebra.CharZero.Defs
import Mathlib.Data.ZMod.Basic

theorem Rat.nat_cast_div_eq {a b : ℕ} :
    ↑(a / b) = (a : ℚ) / (b : ℚ) - (a % b : ℚ) / (b : ℚ) := by
  by_cases hb : b = 0
  · subst hb; simp
  · rw [Nat.div_eq_sub_mod_div, Nat.cast_div (Nat.dvd_sub_mod a) (Nat.cast_ne_zero.mpr hb),
      Nat.cast_sub (Nat.mod_le a b), sub_div]

[Richard Copley]

Here's what changed, for what it's worth:

import Mathlib.Data.Rat.Basic

def xxx (a b : ℕ) := (a % b : ℚ)

set_option pp.coercions false in
#print xxx
-- def xxx : ℕ → ℕ → ℚ :=
-- fun a b => Nat.cast (a % b)

import Mathlib.Data.Rat.Basic
import Mathlib.Algebra.EuclideanDomain.Instances

def xxx (a b : ℕ) := (a % b : ℚ)

set_option pp.coercions false in
#print xxx
-- def xxx : ℕ → ℕ → ℚ :=
-- fun a b => Nat.cast a % Nat.cast b

[Jakob von Raumer]

Yes, writing ↑(a % b) instead, solves the disambiguity.

[Richard Copley]

@Kevin Buzzard, I was shocked too, but I think I have come to terms with it.
We want for example (a / b : ℝ) to mean ↑a / ↑b, not ↑(a / b).
And we want (a % b : ℚ) to mean something, but ↑a % ↑b doesn't make sense until ℚ gets a Mod instance, so ↑(a % b) it is.

[Richard Copley]

And @Jakob von Raumer's is the right solution, not a workaround

[Kevin Buzzard]

Since we switched from lean 3 to lean 4 I've never had any idea what we want (a / b : \R) to mean.

[Ruben Van de Velde]

Neither does lean!

[Eric Rodriguez]

We really don't want fields getting this % instance but it's not really possible (I don't think) to turn it off, right?

[Eric Rodriguez]

Maybe we could make a linter for % on Q