Golfing `(x:Int) / d / d ^ n = x / d ^ (n + 1)`

Stream: new members

[Johannes Choo]

I have two lemmas on integer E-division that I think are suitable for inclusion in Mathlib after being golfed, but I don't know where I should start. The current approach is to convert the edivs into emods generally, then use modular arithmetic to show that the intermediate residues generally don't matter.

Furthermore they presently use Int.ModEq notions, and I suppose it would be nice to just rely on more basic constructs.

theorem Int.ediv_mul_eq_sub_emod (a b : ℤ) : a / b * b = a - a % b :=
  eq_sub_iff_add_eq.mpr (Int.ediv_add_emod' _ _)

theorem Int.ediv_pow_add_one_eq_left (x : ℤ) (hd : 0 < d) (n : ℕ) :
    x / d / d ^ n = x / d ^ (n + 1) := by
  rw [← Int.mul_eq_mul_right_iff (by positivity : d ^ n ≠ 0),
    ← Int.mul_eq_mul_right_iff (by positivity : d ≠ 0),
    mul_assoc (x / d ^ (n + 1)),
    Int.ediv_mul_eq_sub_emod,
    ← Int.pow_succ,
    Int.ediv_mul_eq_sub_emod,
    Int.sub_mul,
    Int.ediv_mul_eq_sub_emod,
    sub_sub,
  ]
  congr
  /-
    x / d % d ^ n ≡ x / d [ ZMOD d ]
      ↔ (x / d % d ^ n) * d ≡ (x / d) * d [ ZMOD d ^ (n + 1) ]
      ↔ x % d + (x / d % d ^ n) * d ≡ x [ ZMOD d ^ (n + 1) ]
      ↔ x % d + (x / d % d ^ n) * d ≡ x % d ^ (n + 1)
  -/
  nth_rw 3 [← Int.ediv_add_emod' x d]
  have : x % d + x / d % d ^ n * d = (x % d + x / d % d ^ n * d) % d ^ (n + 1) := by
    refine (Int.emod_eq_of_lt ?_ ?_).symm
    · exact Int.add_nonneg (Int.emod_nonneg _ (by positivity)) (Int.mul_nonneg (Int.emod_nonneg _ (by positivity)) (le_of_lt hd))
    · calc
        x % d + x / d % d ^ n * d
          < d + x / d % d ^ n * d := by rel [Int.emod_lt_of_pos x hd]
        _ = (1 + x / d % d ^ n) * d := by rw [add_mul, one_mul]
        _ ≤ (1 + (d ^ n - 1)) * d := by
          have : x / d % d ^ n < d ^ n := Int.emod_lt_of_pos (x / d) (by positivity)
          have := Int.le_sub_one_of_lt this
          rel [this]
        _ = d ^ n * d := by rw [add_comm, sub_add_cancel]
        _ = d ^ (n + 1) := by rw [Int.pow_succ]
  have hmodeq : x % d + x / d % d ^ n * d ≡ x / d * d + x % d [ZMOD d ^ (n + 1)] := by
    rw [add_comm (x % d), Int.pow_succ]
    exact Int.ModEq.add_right _ (Int.ModEq.mul_right' (Int.mod_modEq _ _))
  rw [Int.modEq_iff_add_fac] at hmodeq
  rcases hmodeq with ⟨t, hmodeq⟩
  rw [hmodeq, mul_comm (d ^ (n + 1)), Int.add_mul_emod_self]
  exact this

private theorem Int.ediv_pow_add_one_eq_right (x : ℤ) (hd : 0 < d) (n : ℕ) :
    x / d ^ n / d = x / d ^ (n + 1) := by
  rw [
    ← Int.mul_eq_mul_right_iff (by positivity : d ≠ 0),
    ← Int.mul_eq_mul_right_iff (by positivity : d ^ n ≠ 0),
    mul_assoc (x / d ^ (n + 1)),
    Int.ediv_mul_eq_sub_emod,
    ← Int.pow_succ',
    Int.ediv_mul_eq_sub_emod,
    Int.sub_mul,
    Int.ediv_mul_eq_sub_emod,
    sub_sub,
  ]
  congr
  /-
    x / d ^ n % d ≡ x / d ^ n [ ZMOD d ]
      ↔ (x / d ^ n % d) * d ^ n ≡ (x / d ^ n) * d ^ n [ ZMOD d ^ (n + 1) ]
      ↔ x % d ^ n + (x / d ^ n % d) * d ^ n ≡ x [ ZMOD d ^ (n + 1) ]
      ↔ x % d ^ n + (x / d ^ n % d) * d ^ n ≡ x % d ^ (n + 1)
  -/
  nth_rw 3 [← Int.ediv_add_emod' x (d ^ n)]
  have : x % d ^ n + x / d ^ n % d * d ^ n = (x % d ^ n + x / d ^ n % d * d ^ n) % d ^ (n + 1) := by
    refine (Int.emod_eq_of_lt ?_ ?_).symm
    · exact Int.add_nonneg (Int.emod_nonneg _ (by positivity)) (Int.mul_nonneg (Int.emod_nonneg _ (by positivity)) (by positivity))
    · calc
        x % d ^ n + x / d ^ n % d * d ^ n
          < d ^ n + x / d ^ n % d * d ^ n := by rel [Int.emod_lt_of_pos x (by positivity : 0 < d ^ n)]
        _ = (1 + x / d ^ n % d) * d ^ n := by rw [add_mul, one_mul]
        _ ≤ (1 + (d - 1)) * d ^ n := by
          have : x / d ^ n % d < d := Int.emod_lt_of_pos _ hd
          have := Int.le_sub_one_of_lt this
          rel [this]
        _ = d * d ^ n := by rw [add_comm, sub_add_cancel]
        _ = d ^ (n + 1) := by rw [Int.pow_succ']
  have hmodeq : x % d ^ n + x / d ^ n % d * d ^ n ≡ x / d ^ n * d ^ n + x % d ^ n [ZMOD d ^ (n + 1)] := by
    rw [add_comm (x % d ^ n), Int.pow_succ']
    exact Int.ModEq.add_right _ (Int.ModEq.mul_right' (Int.mod_modEq _ _))
  rw [Int.modEq_iff_add_fac] at hmodeq
  rcases hmodeq with ⟨t, hmodeq⟩
  rw [hmodeq, mul_comm (d ^ (n + 1)), Int.add_mul_emod_self]
  exact this

[Ilmārs Cīrulis]

My try, where I prove the result for Nat and then move to Int. I haven't done the private theorem yet.

import Mathlib

theorem T0 (x a b: ℕ): x / a / b = x / (a * b) := by
  exact Nat.div_div_eq_div_mul x a b

theorem T1 (x d n: ℕ): x / d / d ^ n = x / d ^ (n + 1) := by
  rw [T0]; congr 1; exact Eq.symm Nat.pow_succ'

theorem T2 (x d: ℤ) (hd: 0 < d) (hx: 0 ≤ x) (n: ℕ):
    x / d / d ^ n = x / d ^ (n + 1) := by
  have H0: max d 0 = d := by omega
  have H1: max x 0 = x := by omega
  have H: x / d / d ^ n = Int.ofNat (x.toNat / d.toNat / d.toNat ^ n) := by
    simp [H0, H1]
  rw [H, T1]
  simp [H0, H1]

theorem T4 (x d: ℤ) (hd: 0 < d) (hx: x < 0) (n: ℕ):
    x / d / d ^ n = x / d ^ (n + 1) := by
  have H: x / d < 0 := by exact Int.ediv_neg' hx hd
  have H0: ∀ n, 0 < d ^ n := by intro n; exact Lean.Omega.Int.pos_pow_of_pos d n hd
  rw [Int.div_def, Int.ediv_of_neg_of_pos H (H0 n)]
  rw [Int.div_def x (d ^ (n + 1)), Int.ediv_of_neg_of_pos hx (H0 (n + 1))]
  congr 2
  rw [<- T2 _ _ hd (by omega)]
  congr
  rw [Int.div_def x, Int.ediv_of_neg_of_pos hx hd]
  simp

theorem Int.ediv_pow_add_one_eq_left (x d: ℤ) (hd: 0 < d) (n: ℕ):
    x / d / d ^ n = x / d ^ (n + 1) := by
  obtain H | H := Int.lt_or_le x 0
  . apply T4 _ _ hd H
  . apply T2 _ _ hd H

[Johannes Choo]

Ohh separate cases for nonpositive and positive.

Ah I forgot to remove the private there when posting this

[Johannes Choo]

Does Nat.div_div_eq_div_mul still hold in general for integers and ediv (but positive denominators)

[Johannes Choo]

Ok I think it is always the case and I should prove that instead.

[Ilmārs Cīrulis]

Yes, I have almost proved that, too.

[Ilmārs Cīrulis]

import Mathlib

theorem T1 {x d1 d2: ℤ} (hd1: 0 < d1) (hd2: 0 < d2) (hx: 0 ≤ x):
    x / d1 / d2 = x / (d1 * d2) := by
  have H0: max d1 0 = d1 := max_eq_left_of_lt hd1
  have H1: max d2 0 = d2 := max_eq_left_of_lt hd2
  have H2: max x 0 = x := Int.max_eq_left hx
  have H: x / d1 / d2 = Int.ofNat (x.toNat / d1.toNat / d2.toNat) := by
    simp [H0, H1, H2]
  rw [H, Nat.div_div_eq_div_mul]
  simp [H0, H1, H2]

theorem T2 {x d1 d2: ℤ} (hd1: 0 < d1) (hd2: 0 < d2) (hx: x < 0):
    x / d1 / d2 = x / (d1 * d2) := by
  have H: x / d1 < 0 := Int.ediv_neg' hx hd1
  rw [Int.div_def, Int.ediv_of_neg_of_pos H hd2,
      Int.div_def x (d1 * d2), Int.ediv_of_neg_of_pos hx (Int.mul_pos hd1 hd2),
      <- T1 hd1 hd2 (by linarith), Int.div_def x, Int.ediv_of_neg_of_pos hx hd1]
  simp

theorem Int.div_div_eq_div_mul (x d1 d2: ℤ) (hd1: 0 < d1) (hd2: 0 < d2):
    x / d1 / d2 = x / (d1 * d2) := by
  obtain H | H := Int.lt_or_le x 0
  . apply T2 hd1 hd2 H
  . apply T1 hd1 hd2 H

Edit:
Removed T0 (used Nat.div_div_eq_div_mul directly).
Removed congrs from T2 because proof works without them too. Replaced all the omegas.

[Johannes Choo]

Int.ediv_ediv_eq_ediv_mul (m : ℤ) {n k : ℤ} (hn : 0 < n) (hk : 0 < k) :
    m / n / k = m / (n * k) := by
  have hmnpos : 0 ≤ m % n := Int.emod_nonneg _ (by positivity)
  have hmnkpos : 0 ≤ m / n % k := Int.emod_nonneg _ (by positivity)
  have hmn : m % n < n := Int.emod_lt_of_pos _ hn
  have hmnk : m / n % k ≤ k - 1 := Int.le_sub_one_of_lt (Int.emod_lt_of_pos _ hk)
  have ineq1 := calc
    m / n / k * (k * n) ≤ m / n / k * (k * n) + (m / n % k * n + m % n) :=
      Int.le_add_of_nonneg_right (Int.add_nonneg
        (Int.mul_nonneg hmnkpos (le_of_lt hn)) hmnpos)
    _ = (m / n / k * k + m / n % k) * n + m % n := by rw [add_mul]; group
    _ = m := by rw [Int.ediv_add_emod', Int.ediv_add_emod']
  apply Int.ediv_le_ediv (by positivity : 0 < k * n) at ineq1
  rw [Int.mul_ediv_cancel _ (by positivity), mul_comm] at ineq1
  have ineq2 := calc
    m = (m / n / k * k + m / n % k) * n + m % n := by rw [Int.ediv_add_emod', Int.ediv_add_emod']
    _ = m / n / k * (n * k) + (m / n % k * n + m % n) := by rw [add_mul]; group
    _ < m / n / k * (n * k) + (m / n % k * n + n) := by rel [hmn]
    _ ≤ m / n / k * (n * k) + ((k-1) * n + n) := by rel [hmnk]
    _ = (m / n / k + 1) * (n * k) := by ring
  apply Int.ediv_lt_of_lt_mul (by positivity) at ineq2
  omega

Ok I have a clear direct proof of it now

[Ilmārs Cīrulis]

Looks impressive!