int div nat eq floor rat

Stream: new members

[Kevin Kappelmann]

Hi, I am a bit stuck proving the following lemma and was wondering if anyone has a clever idea how to solve it:

lemma div_eq_rat_floor (n : ℤ) (d : ℕ) : n / d = ⌊rat.mk n d⌋ :=
sorry

I was able to show it in case n and d are coprime, so alternatively, proving the following lemma would also work

lemma div_nat_int_eq_rat_num_denom_div (n : ℤ) (d : ℕ) :
  let q := rat.mk n d in n / d = q.num / q.denom :=
sorry

[Edward Ayers]

Perhaps this lemma in mathlib might be helpful?

theorem div_eq_div_of_mul_eq_mul {a b c d : ℤ} (H1 : b ∣ a) (H2 : d ∣ c) (H3 : b ≠ 0)
    (H4 : d ≠ 0) (H5 : a * d = b * c) :
  a / b = c / d

maybe withdenom_dvd and num_dvd?

[Kevin Kappelmann]

I don't know that q.denom | n for example. I think I sorted it out using rat.num_denom_mk now. I can post the code in a few mins :)

[Kevin Buzzard]

How far are the CS people from being able to prove this sort of thing using an all-purpose tactic?

[Mario Carneiro]

this is a lemma not a tactic

[Kevin Kappelmann]

My not so short but I'd say rather comprehensible solution:

lemma div_nat_int_eq_div_rat_num_denom (n : ℤ) (d : ℕ) :
  n / d = (rat.mk n d).num / (rat.mk n d).denom :=
begin
cases decidable.em (d = 0) with d_zero d_not_zero,
{ simp [d_zero] },
{
  cases decidable.em (n = 0) with n_zero n_not_zero,
  { simp [n_zero] },
  {
    set q := rat.mk n d with q_eq_rat_mk,
    replace d_not_zero : d ≠ 0, from d_not_zero,
    have : (d : ℤ) ≠ 0, by simp [d_not_zero],
    have : ∃ (c : ℤ), n = c * q.num ∧ (d : ℤ) = c * q.denom, from rat.num_denom_mk n_not_zero this q_eq_rat_mk,
    rcases this with ⟨c, ⟨n_eq_c_mul_num, d_eq_c_mul_denom⟩⟩,
    suffices : c > 0, by simp only [(int.mul_div_mul_of_pos _ _ ‹c > 0›), n_eq_c_mul_num, d_eq_c_mul_denom],
    show c > 0, by {
      have zero_lt_q_denom_mul_c : (0 : ℤ) < q.denom * c, by {
        have : 0 < d, by rwa ←nat.pos_iff_ne_zero at d_not_zero,
        have : (0 : ℤ) < d, by simp [this],
        rw [d_eq_c_mul_denom, mul_comm] at this,
        exact this
      },
      suffices : (0 : ℤ) ≤ q.denom, from pos_of_mul_pos_left zero_lt_q_denom_mul_c this,
      have : 0 < q.denom, from q.pos,
      simp [le_of_lt, this],
    }
  }
}
end

lemma div_eq_rat_floor (n : ℤ) (d : ℕ) : n / d = ⌊rat.mk n d⌋ :=
begin
  cases rat_n_d_eq : rat.mk n d with n' d',
  suffices : n / d = n' / d', by { unfold floor floor_ring.floor rat.floor, assumption },
  simp [(div_nat_int_eq_div_rat_num_denom n d), rat_n_d_eq]
end

Happy to hear about other ways to do it.