Theorem: trunc_pow_mul (Fl/Trunc.lean)

State before:
n : ℕ
npos : 0 < n
x k : ℕ
⊢ trunc n (2 ^ k * x) = 2 ^ k * trunc n x
Tactic:
cases eq_or_ne x 0 with
| inl eq_zero =>
  unfold trunc ulp expt
  rw [eq_zero, Nat.mul_zero, Nat.zero_div, Nat.zero_mul, Nat.mul_zero]
| inr ne_zero =>
  cases Nat.lt_or_ge n (Nat.size x) with
  | inr size_le =>
    have uflow : x < 2 ^ n := by
      rewrite [← Nat.size_le]
      exact size_le.le
    have d : ulp n (2 ^ k * x) ∣ 2 ^ k * x := by
      unfold ulp expt
      apply dvd_mul_of_dvd_left
      rewrite [Nat.pow_dvd_pow_iff_le_right one_lt_two]
      rewrite [size_pow_mul (Nat.zero_lt_of_ne_zero ne_zero)]
      rewrite [tsub_le_iff_left]
      apply Nat.add_le_add_right
      exact size_le
    rewrite [trunc_eq_self_of_uflow uflow]
    exact trunc_eq_of_le_of_ulp_dvd (2 ^ k * x) le_rfl d
  | inl lt_size =>
    unfold trunc
    rewrite [ulp_pow_mul npos (le_of_lt lt_size)]
    rewrite [Nat.mul_div_mul_left _ _ two_pow_pos]
    rw [mul_rotate', Nat.mul_comm (ulp n x)]
State after:
no goals

State before:
case inl
n : ℕ
npos : 0 < n
x k : ℕ
eq_zero : x = 0
⊢ trunc n (2 ^ k * x) = 2 ^ k * trunc n x
Tactic:
unfold trunc ulp expt
State after:
case inl
n : ℕ
npos : 0 < n
x k : ℕ
eq_zero : x = 0
⊢ 2 ^ k * x / 2 ^ (Nat.size (2 ^ k * x) - n) * 2 ^ (Nat.size (2 ^ k * x) - n) =
    2 ^ k * (x / 2 ^ (Nat.size x - n) * 2 ^ (Nat.size x - n))

State before:
case inl
n : ℕ
npos : 0 < n
x k : ℕ
eq_zero : x = 0
⊢ 2 ^ k * x / 2 ^ (Nat.size (2 ^ k * x) - n) * 2 ^ (Nat.size (2 ^ k * x) - n) =
    2 ^ k * (x / 2 ^ (Nat.size x - n) * 2 ^ (Nat.size x - n))
Tactic:
rw [eq_zero, Nat.mul_zero, Nat.zero_div, Nat.zero_mul, Nat.mul_zero]
State after:
no goals

State before:
case inr
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
⊢ trunc n (2 ^ k * x) = 2 ^ k * trunc n x
Tactic:
cases Nat.lt_or_ge n (Nat.size x) with
| inr size_le =>
  have uflow : x < 2 ^ n := by
    rewrite [← Nat.size_le]
    exact size_le.le
  have d : ulp n (2 ^ k * x) ∣ 2 ^ k * x := by
    unfold ulp expt
    apply dvd_mul_of_dvd_left
    rewrite [Nat.pow_dvd_pow_iff_le_right one_lt_two]
    rewrite [size_pow_mul (Nat.zero_lt_of_ne_zero ne_zero)]
    rewrite [tsub_le_iff_left]
    apply Nat.add_le_add_right
    exact size_le
  rewrite [trunc_eq_self_of_uflow uflow]
  exact trunc_eq_of_le_of_ulp_dvd (2 ^ k * x) le_rfl d
| inl lt_size =>
  unfold trunc
  rewrite [ulp_pow_mul npos (le_of_lt lt_size)]
  rewrite [Nat.mul_div_mul_left _ _ two_pow_pos]
  rw [mul_rotate', Nat.mul_comm (ulp n x)]
State after:
no goals

State before:
case inr.inr
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
⊢ trunc n (2 ^ k * x) = 2 ^ k * trunc n x
Tactic:
have uflow : x < 2 ^ n := by
  rewrite [← Nat.size_le]
  exact size_le.le
State after:
case inr.inr
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
⊢ trunc n (2 ^ k * x) = 2 ^ k * trunc n x

State before:
case inr.inr
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
⊢ trunc n (2 ^ k * x) = 2 ^ k * trunc n x
Tactic:
have d : ulp n (2 ^ k * x) ∣ 2 ^ k * x := by
  unfold ulp expt
  apply dvd_mul_of_dvd_left
  rewrite [Nat.pow_dvd_pow_iff_le_right one_lt_two]
  rewrite [size_pow_mul (Nat.zero_lt_of_ne_zero ne_zero)]
  rewrite [tsub_le_iff_left]
  apply Nat.add_le_add_right
  exact size_le
State after:
case inr.inr
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
d : ulp n (2 ^ k * x) ∣ 2 ^ k * x
⊢ trunc n (2 ^ k * x) = 2 ^ k * trunc n x

State before:
case inr.inr
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
d : ulp n (2 ^ k * x) ∣ 2 ^ k * x
⊢ trunc n (2 ^ k * x) = 2 ^ k * trunc n x
Tactic:
rewrite [trunc_eq_self_of_uflow uflow]
State after:
case inr.inr
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
d : ulp n (2 ^ k * x) ∣ 2 ^ k * x
⊢ trunc n (2 ^ k * x) = 2 ^ k * x

State before:
case inr.inr
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
d : ulp n (2 ^ k * x) ∣ 2 ^ k * x
⊢ trunc n (2 ^ k * x) = 2 ^ k * x
Tactic:
exact trunc_eq_of_le_of_ulp_dvd (2 ^ k * x) le_rfl d
State after:
no goals

State before:
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
⊢ x < 2 ^ n
Tactic:
rewrite [← Nat.size_le]
State after:
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
⊢ Nat.size x ≤ n

State before:
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
⊢ Nat.size x ≤ n
Tactic:
exact size_le.le
State after:
no goals

State before:
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
⊢ ulp n (2 ^ k * x) ∣ 2 ^ k * x
Tactic:
unfold ulp expt
State after:
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
⊢ 2 ^ (Nat.size (2 ^ k * x) - n) ∣ 2 ^ k * x

State before:
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
⊢ 2 ^ (Nat.size (2 ^ k * x) - n) ∣ 2 ^ k * x
Tactic:
apply dvd_mul_of_dvd_left
State after:
case h
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
⊢ 2 ^ (Nat.size (2 ^ k * x) - n) ∣ 2 ^ k

State before:
case h
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
⊢ 2 ^ (Nat.size (2 ^ k * x) - n) ∣ 2 ^ k
Tactic:
rewrite [Nat.pow_dvd_pow_iff_le_right one_lt_two]
State after:
case h
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
⊢ Nat.size (2 ^ k * x) - n ≤ k

State before:
case h
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
⊢ Nat.size (2 ^ k * x) - n ≤ k
Tactic:
rewrite [size_pow_mul (Nat.zero_lt_of_ne_zero ne_zero)]
State after:
case h
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
⊢ Nat.size x + k - n ≤ k

State before:
case h
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
⊢ Nat.size x + k - n ≤ k
Tactic:
rewrite [tsub_le_iff_left]
State after:
case h
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
⊢ Nat.size x + k ≤ n + k

State before:
case h
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
⊢ Nat.size x + k ≤ n + k
Tactic:
apply Nat.add_le_add_right
State after:
case h.h
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
⊢ Nat.size x ≤ n

State before:
case h.h
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
⊢ Nat.size x ≤ n
Tactic:
exact size_le
State after:
no goals

State before:
case inr.inl
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
lt_size : n < Nat.size x
⊢ trunc n (2 ^ k * x) = 2 ^ k * trunc n x
Tactic:
unfold trunc
State after:
case inr.inl
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
lt_size : n < Nat.size x
⊢ 2 ^ k * x / ulp n (2 ^ k * x) * ulp n (2 ^ k * x) = 2 ^ k * (x / ulp n x * ulp n x)

State before:
case inr.inl
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
lt_size : n < Nat.size x
⊢ 2 ^ k * x / ulp n (2 ^ k * x) * ulp n (2 ^ k * x) = 2 ^ k * (x / ulp n x * ulp n x)
Tactic:
rewrite [ulp_pow_mul npos (le_of_lt lt_size)]
State after:
case inr.inl
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
lt_size : n < Nat.size x
⊢ 2 ^ k * x / (2 ^ k * ulp n x) * (2 ^ k * ulp n x) = 2 ^ k * (x / ulp n x * ulp n x)

State before:
case inr.inl
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
lt_size : n < Nat.size x
⊢ 2 ^ k * x / (2 ^ k * ulp n x) * (2 ^ k * ulp n x) = 2 ^ k * (x / ulp n x * ulp n x)
Tactic:
rewrite [Nat.mul_div_mul_left _ _ two_pow_pos]
State after:
case inr.inl
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
lt_size : n < Nat.size x
⊢ x / ulp n x * (2 ^ k * ulp n x) = 2 ^ k * (x / ulp n x * ulp n x)

State before:
case inr.inl
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
lt_size : n < Nat.size x
⊢ x / ulp n x * (2 ^ k * ulp n x) = 2 ^ k * (x / ulp n x * ulp n x)
Tactic:
rw [mul_rotate', Nat.mul_comm (ulp n x)]
State after:
no goals