Lifting Nat lemmas to Int

Stream: new members

[Gareth Ma]

How should I prove the following?

example (a b : ℕ) (h : a ≤ a / b * b + b) :
    ofNat a ≤ ofNat a / ofNat b * ofNat b + ofNat b := by
  sorry

[Eric Wieser]

exact h

[Gareth Ma]

Nope :(

[Gareth Ma]

ofNat is Int.ofNat

[Gareth Ma]

Let me edit

[Eric Wieser]

Gareth Ma said:

ofNat is Int.ofNat

The preferred spelling is Nat.cast

[Gareth Ma]

I got this from cases on an Int :(

[Eric Wieser]

Well that was your first mistake :)

[Eric Wieser]

obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg is usually a better choice

[Gareth Ma]

Lmao. How should I prove the following then? Or at least the first steps I guess

lemma lt_div_mul_add_pos (a b : ℕ) (hb : 0 < b) : a < a / b * b + b := by
  nth_rw 2 [← Nat.div_add_mod' a b, mul_comm _ b]
  rw [Nat.mul_add_div hb (a / b) (a % b), add_mul, add_rotate]
  nth_rw 1 [← Nat.div_add_mod' a b, add_comm]
  apply add_lt_add_right $ Nat.lt_add_left _ $ Nat.mod_lt _ hb

example (a b : ℤ) (hb : 0 < b) : a < a / b * b + b := by
  slim_check

[Gareth Ma]

Ohh okay I will try

[Gareth Ma]

Ahha so I use that to get Nat.cast, from which norm_cast can simplify all of that away

[Gareth Ma]

amazing

[Gareth Ma]

Any hint on closing this?

theorem Int.mul_add_div {m : Int} (hm : m ≠ 0) (x y : Int) : (m * x + y) / m = x + y / m := by
  sorry

[Gareth Ma]

It seems the Int part is missing a ton of lemmas from Nat, and I can't prove them even with the entire Mathlib. Or is it my skill issue

[Rida Hamadani]

Assuming you are using the division from Data.Int.Basic, this is not true due to rounding, right?

[Gareth Ma]

Why?

theorem Int.mul_add_div {m : Int} (hm : m ≠ 0) (x y : Int) : (m * x + y) / m = x + y / m := by
  slim_check (config:={numInst:=1000,maxSize:=1000}) /- passes -/

[Gareth Ma]

If m stays the same, a -> a / m rounds the same way

[Gareth Ma]

If that's what you mean

[Gareth Ma]

I think

[Gareth Ma]

lemma Int.fdiv_eq_floor {a b : ℤ} : Int.fdiv a b = ⌊(a : ℚ) / (b : ℚ)⌋ := by
  cases' a with a a <;> cases' b with b b
  · cases' a with a <;> simp [fdiv]
    have : 0 ≤ ((a : ℚ) + 1) / (b : ℚ) := by apply div_nonneg <;> norm_cast <;> omega
    rw [← ofNat_floor_eq_floor this, show (1 : ℚ) = (1 : ℕ) by rfl, ← Nat.cast_add,
      Nat.floor_div_eq_div]
    norm_cast
  · cases' a with a <;> simp [fdiv]
    rw [negSucc_eq, Nat.succ_eq_add_one, neg_add, ← sub_eq_add_neg]
    rw [← neg_add, div_neg, sub_eq_iff_eq_add, ← floor_add_one]

I am now stuck on this. Int is painful...

[Gareth Ma]

Like fdiv is defined in core Lean (?) but never used again

[Rida Hamadani]

Gareth Ma said:

If m stays the same, a -> a / m rounds the same way

Ah I see, sorry!

[Gareth Ma]

Okay I got mul_add_div down:

theorem Int.mul_add_div {m : Int} (hm : m ≠ 0) (x y : Int) : (m * x + y) / m = x + y / m := by
  rw [add_comm, add_mul_ediv_left _ _ hm, add_comm]

[Gareth Ma]

https://github.com/leanprover/std4/commit/9ccf392be03aa7b3b80c9e5b2c5e24272d36ee27#diff-efd89f01e8fa474be03044698b70ca62e27ffaddc9440e5570fe97daaf5cbc70R132 there's no way I can figure this out myself