internlm/Lean-Github huggingface dataset:
Theorem: size_div_pow
Proof state before:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x
⊢ x / 2 ^ m < 2 ^ (Nat.size x - m)
Tactic:
rewrite [Nat.div_lt_iff_lt_mul two_pow_pos]
Proof state after:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x
⊢ x < 2 ^ (Nat.size x - m) * 2 ^ m
Theorem: size_div_pow
Proof state before:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x
⊢ x < 2 ^ (Nat.size x - m) * 2 ^ m
Tactic:
rewrite [← Nat.pow_div lt_size.le two_pos]
Proof state after:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x
⊢ x < 2 ^ Nat.size x / 2 ^ m * 2 ^ m
Theorem: size_div_pow
Proof state before:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x
⊢ x < 2 ^ Nat.size x / 2 ^ m * 2 ^ m
Tactic:
rewrite [Nat.div_mul_cancel pow_dvd]
Proof state after:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x
⊢ x < 2 ^ Nat.size x
Theorem: size_div_pow
Proof state before:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x
⊢ x < 2 ^ Nat.size x
Tactic:
exact Nat.lt_size_self x
Proof state after:
no goals
Theorem: size_div_mul
Proof state before:
x m : ℕ
h : 2 ^ m ≤ x
⊢ Nat.size (x / 2 ^ m * 2 ^ m) = Nat.size x
Tactic:
have div_pow_pos : 0 < x / 2 ^ m := Nat.div_pos h two_pow_pos
Proof state after:
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ Nat.size (x / 2 ^ m * 2 ^ m) = Nat.size x
Theorem: size_div_mul
Proof state before:
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ Nat.size (x / 2 ^ m * 2 ^ m) = Nat.size x
Tactic:
rewrite [size_mul_pow div_pow_pos m]
Proof state after:
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ Nat.size (x / 2 ^ m) + m = Nat.size x
Theorem: size_div_mul
Proof state before:
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ Nat.size (x / 2 ^ m) + m = Nat.size x
Tactic:
rewrite [size_div_pow h]
Proof state after:
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ Nat.size x - m + m = Nat.size x
Theorem: size_div_mul
Proof state before:
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ Nat.size x - m + m = Nat.size x
Tactic:
apply tsub_add_cancel_of_le
Proof state after:
case h
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ m ≤ Nat.size x
Theorem: size_div_mul
Proof state before:
case h
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ m ≤ Nat.size x
Tactic:
apply Nat.le_of_pred_lt
Proof state after:
case h.a
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ Nat.pred m < Nat.size x
Theorem: size_div_mul
Proof state before:
case h.a
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ Nat.pred m < Nat.size x
Tactic:
rewrite [Nat.lt_size]
Proof state after:
case h.a
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ 2 ^ Nat.pred m ≤ x
Theorem: size_div_mul
Proof state before:
case h.a
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ 2 ^ Nat.pred m ≤ x
Tactic:
calc 2 ^ Nat.pred m
  _ ≤ 2 ^ m := Nat.pow_le_pow_of_le_right two_pos (Nat.pred_le m)
  _ ≤ x     := h
Proof state after:
no goals
Theorem: mod_eq_sub_div_mul
Proof state before:
m k : ℕ
⊢ m % k = m - m / k * k
Tactic:
apply eq_tsub_of_add_eq
Proof state after:
case h
m k : ℕ
⊢ m % k + m / k * k = m
Theorem: mod_eq_sub_div_mul
Proof state before:
case h
m k : ℕ
⊢ m % k + m / k * k = m
Tactic:
exact Nat.mod_add_div' m k
Proof state after:
no goals
Theorem: expt_le_expt
Proof state before:
n x y : ℕ
h : x ≤ y
⊢ expt n x ≤ expt n y
Tactic:
unfold expt
Proof state after:
n x y : ℕ
h : x ≤ y
⊢ Nat.size x - n ≤ Nat.size y - n
Theorem: expt_le_expt
Proof state before:
n x y : ℕ
h : x ≤ y
⊢ Nat.size x - n ≤ Nat.size y - n
Tactic:
exact tsub_le_tsub_right (Nat.size_le_size h) n
Proof state after:
no goals
Theorem: trunc_zero
Proof state before:
n : ℕ
⊢ trunc n 0 = 0
Tactic:
unfold trunc
Proof state after:
n : ℕ
⊢ 0 / ulp n 0 * ulp n 0 = 0
Theorem: trunc_zero
Proof state before:
n : ℕ
⊢ 0 / ulp n 0 * ulp n 0 = 0
Tactic:
rw [Nat.zero_div, Nat.zero_mul]
Proof state after:
no goals
Theorem: one_le_expt_of_no_uflow
Proof state before:
n x : ℕ
no_uflow : 2 ^ n ≤ x
⊢ 1 ≤ expt n x
Tactic:
unfold expt
Proof state after:
n x : ℕ
no_uflow : 2 ^ n ≤ x
⊢ 1 ≤ Nat.size x - n
Theorem: one_le_expt_of_no_uflow
Proof state before:
n x : ℕ
no_uflow : 2 ^ n ≤ x
⊢ 1 ≤ Nat.size x - n
Tactic:
apply le_tsub_of_add_le_left
Proof state after:
case h
n x : ℕ
no_uflow : 2 ^ n ≤ x
⊢ n + 1 ≤ Nat.size x
Theorem: one_le_expt_of_no_uflow
Proof state before:
case h
n x : ℕ
no_uflow : 2 ^ n ≤ x
⊢ n + 1 ≤ Nat.size x
Tactic:
rewrite [Nat.add_one, Nat.succ_le, Nat.lt_size]
Proof state after:
case h
n x : ℕ
no_uflow : 2 ^ n ≤ x
⊢ 2 ^ n ≤ x
Theorem: one_le_expt_of_no_uflow
Proof state before:
case h
n x : ℕ
no_uflow : 2 ^ n ≤ x
⊢ 2 ^ n ≤ x
Tactic:
exact no_uflow
Proof state after:
no goals
Theorem: ulp_eq_one_of_uflow
Proof state before:
n x : ℕ
uflow : x < 2 ^ n
⊢ ulp n x = 1
Tactic:
unfold ulp
Proof state after:
n x : ℕ
uflow : x < 2 ^ n
⊢ 2 ^ expt n x = 1
Theorem: ulp_eq_one_of_uflow
Proof state before:
n x : ℕ
uflow : x < 2 ^ n
⊢ 2 ^ expt n x = 1
Tactic:
rw [expt_eq_zero_of_uflow uflow, Nat.pow_zero]
Proof state after:
no goals
Theorem: trunc_add_half_ulp_eq_of_uflow
Proof state before:
n x : ℕ
uflow : x < 2 ^ n
⊢ trunc n x + ulp n x / 2 = x
Tactic:
unfold trunc
Proof state after:
n x : ℕ
uflow : x < 2 ^ n
⊢ x / ulp n x * ulp n x + ulp n x / 2 = x
Theorem: trunc_add_half_ulp_eq_of_uflow
Proof state before:
n x : ℕ
uflow : x < 2 ^ n
⊢ x / ulp n x * ulp n x + ulp n x / 2 = x
Tactic:
rewrite [ulp_eq_one_of_uflow uflow]
Proof state after:
n x : ℕ
uflow : x < 2 ^ n
⊢ x / 1 * 1 + 1 / 2 = x
Theorem: trunc_add_half_ulp_eq_of_uflow
Proof state before:
n x : ℕ
uflow : x < 2 ^ n
⊢ x / 1 * 1 + 1 / 2 = x
Tactic:
rw [Nat.mul_one, Nat.div_one, Nat.div_eq_of_lt one_lt_two, Nat.add_zero]
Proof state after:
no goals
Theorem: trunc_eq_self_of_uflow
Proof state before:
n x : ℕ
uflow : x < 2 ^ n
⊢ trunc n x = x
Tactic:
unfold trunc
Proof state after:
n x : ℕ
uflow : x < 2 ^ n
⊢ x / ulp n x * ulp n x = x
Theorem: trunc_eq_self_of_uflow
Proof state before:
n x : ℕ
uflow : x < 2 ^ n
⊢ x / ulp n x * ulp n x = x
Tactic:
rw [ulp_eq_one_of_uflow uflow, Nat.mul_one, Nat.div_one]
Proof state after:
no goals
Theorem: trunc_pred_eq_sub_ulp_of_pos_of_trunc_eq
Proof state before:
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ trunc n (x - 1) = x - ulp n (x - 1)
Tactic:
unfold trunc
Proof state after:
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ (x - 1) / ulp n (x - 1) * ulp n (x - 1) = x - ulp n (x - 1)
Theorem: trunc_pred_eq_sub_ulp_of_pos_of_trunc_eq
Proof state before:
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ (x - 1) / ulp n (x - 1) * ulp n (x - 1) = x - ulp n (x - 1)
Tactic:
apply div_mul_pred_eq_sub_of_pos_of_dvd
Proof state after:
case h₀
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ 0 < ulp n (x - 1)

case h₂
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ 0 < x

case h₁
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ x
Theorem: trunc_pred_eq_sub_ulp_of_pos_of_trunc_eq
Proof state before:
case h₀
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ 0 < ulp n (x - 1)

case h₂
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ 0 < x

case h₁
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ x
Tactic:
. exact ulp_pos n _
Proof state after:
case h₂
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ 0 < x

case h₁
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ x
Theorem: trunc_pred_eq_sub_ulp_of_pos_of_trunc_eq
Proof state before:
case h₂
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ 0 < x

case h₁
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ x
Tactic:
. exact xpos
Proof state after:
case h₁
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ x
Theorem: trunc_pred_eq_sub_ulp_of_pos_of_trunc_eq
Proof state before:
case h₁
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ x
Tactic:
. trans ulp n x
  . exact ulp_dvd_ulp n tsub_le_self
  . exact ulp_dvd_of_trunc_eq hfx
Proof state after:
no goals
Theorem: trunc_pred_eq_sub_ulp_of_pos_of_trunc_eq
Proof state before:
case h₀
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ 0 < ulp n (x - 1)
Tactic:
exact ulp_pos n _
Proof state after:
no goals
Theorem: trunc_pred_eq_sub_ulp_of_pos_of_trunc_eq
Proof state before:
case h₂
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ 0 < x
Tactic:
exact xpos
Proof state after:
no goals
Theorem: trunc_pred_eq_sub_ulp_of_pos_of_trunc_eq
Proof state before:
case h₁
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ x
Tactic:
trans ulp n x
Proof state after:
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ ulp n x

x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n x ∣ x
Theorem: trunc_pred_eq_sub_ulp_of_pos_of_trunc_eq
Proof state before:
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ ulp n x

x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n x ∣ x
Tactic:
. exact ulp_dvd_ulp n tsub_le_self
Proof state after:
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n x ∣ x
Theorem: trunc_pred_eq_sub_ulp_of_pos_of_trunc_eq
Proof state before:
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n x ∣ x
Tactic:
. exact ulp_dvd_of_trunc_eq hfx
Proof state after:
no goals
Theorem: trunc_pred_eq_sub_ulp_of_pos_of_trunc_eq
Proof state before:
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ ulp n x
Tactic:
exact ulp_dvd_ulp n tsub_le_self
Proof state after:
no goals
Theorem: trunc_pred_eq_sub_ulp_of_pos_of_trunc_eq
Proof state before:
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n x ∣ x
Tactic:
exact ulp_dvd_of_trunc_eq hfx
Proof state after:
no goals
Theorem: trunc_eq_sub_mod
Proof state before:
n x : ℕ
⊢ trunc n x = x - x % ulp n x
Tactic:
apply eq_tsub_of_add_eq
Proof state after:
case h
n x : ℕ
⊢ trunc n x + x % ulp n x = x
Theorem: trunc_eq_sub_mod
Proof state before:
case h
n x : ℕ
⊢ trunc n x + x % ulp n x = x
Tactic:
exact Nat.div_add_mod' x (ulp n x)
Proof state after:
no goals
Theorem: ulp_le_self
Proof state before:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ ulp n x ≤ x
Tactic:
unfold ulp expt
Proof state after:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - n) ≤ x
Theorem: ulp_le_self
Proof state before:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - n) ≤ x
Tactic:
trans 2 ^ (Nat.size x - 1)
Proof state after:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - n) ≤ 2 ^ (Nat.size x - 1)

n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - 1) ≤ x
Theorem: ulp_le_self
Proof state before:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - n) ≤ 2 ^ (Nat.size x - 1)

n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - 1) ≤ x
Tactic:
. apply Nat.pow_le_pow_of_le_right two_pos
  exact tsub_le_tsub_left (Nat.one_le_of_lt npos) _
Proof state after:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - 1) ≤ x
Theorem: ulp_le_self
Proof state before:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - 1) ≤ x
Tactic:
. exact le_size_of_pos xpos
Proof state after:
no goals
Theorem: ulp_le_self
Proof state before:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - n) ≤ 2 ^ (Nat.size x - 1)
Tactic:
apply Nat.pow_le_pow_of_le_right two_pos
Proof state after:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ Nat.size x - n ≤ Nat.size x - 1
Theorem: ulp_le_self
Proof state before:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ Nat.size x - n ≤ Nat.size x - 1
Tactic:
exact tsub_le_tsub_left (Nat.one_le_of_lt npos) _
Proof state after:
no goals
Theorem: ulp_le_self
Proof state before:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - 1) ≤ x
Tactic:
exact le_size_of_pos xpos
Proof state after:
no goals
Theorem: size_trunc_eq_size
Proof state before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ Nat.size (trunc n x) = Nat.size x
Tactic:
unfold trunc ulp expt
Proof state after:
n : ℕ
npos : 0 < n
x : ℕ
⊢ Nat.size (x / 2 ^ (Nat.size x - n) * 2 ^ (Nat.size x - n)) = Nat.size x
Theorem: size_trunc_eq_size
Proof state before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ Nat.size (x / 2 ^ (Nat.size x - n) * 2 ^ (Nat.size x - n)) = Nat.size x
Tactic:
cases Nat.eq_zero_or_pos x with
| inl zero => rw [zero, Nat.zero_div, Nat.zero_mul]
| inr pos =>
  apply size_div_mul
  rewrite [← Nat.lt_size]
  exact tsub_lt_self (Nat.size_pos.mpr pos) npos
Proof state after:
no goals
Theorem: size_trunc_eq_size
Proof state before:
case inl
n : ℕ
npos : 0 < n
x : ℕ
zero : x = 0
⊢ Nat.size (x / 2 ^ (Nat.size x - n) * 2 ^ (Nat.size x - n)) = Nat.size x
Tactic:
rw [zero, Nat.zero_div, Nat.zero_mul]
Proof state after:
no goals
Theorem: size_trunc_eq_size
Proof state before:
case inr
n : ℕ
npos : 0 < n
x : ℕ
pos : x > 0
⊢ Nat.size (x / 2 ^ (Nat.size x - n) * 2 ^ (Nat.size x - n)) = Nat.size x
Tactic:
apply size_div_mul
Proof state after:
case inr.h
n : ℕ
npos : 0 < n
x : ℕ
pos : x > 0
⊢ 2 ^ (Nat.size x - n) ≤ x
Theorem: size_trunc_eq_size
Proof state before:
case inr.h
n : ℕ
npos : 0 < n
x : ℕ
pos : x > 0
⊢ 2 ^ (Nat.size x - n) ≤ x
Tactic:
rewrite [← Nat.lt_size]
Proof state after:
case inr.h
n : ℕ
npos : 0 < n
x : ℕ
pos : x > 0
⊢ Nat.size x - n < Nat.size x
Theorem: size_trunc_eq_size
Proof state before:
case inr.h
n : ℕ
npos : 0 < n
x : ℕ
pos : x > 0
⊢ Nat.size x - n < Nat.size x
Tactic:
exact tsub_lt_self (Nat.size_pos.mpr pos) npos
Proof state after:
no goals
Theorem: ulp_trunc
Proof state before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ ulp n (trunc n x) = ulp n x
Tactic:
unfold ulp expt
Proof state after:
n : ℕ
npos : 0 < n
x : ℕ
⊢ 2 ^ (Nat.size (trunc n x) - n) = 2 ^ (Nat.size x - n)
Theorem: ulp_trunc
Proof state before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ 2 ^ (Nat.size (trunc n x) - n) = 2 ^ (Nat.size x - n)
Tactic:
rw [size_trunc_eq_size npos x]
Proof state after:
no goals
Theorem: trunc_idempotent
Proof state before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ trunc n (trunc n x) = trunc n x
Tactic:
rw [trunc, ulp_trunc npos, trunc, Nat.mul_div_cancel _ (ulp_pos _ _)]
Proof state after:
no goals
Theorem: trunc_le_trunc
Proof state before:
n x y : ℕ
npos : 0 < n
h : x ≤ y
⊢ trunc n x ≤ trunc n y
Tactic:
cases Nat.lt_or_ge (Nat.size x) (Nat.size y) with
| inl size_lt_size =>
  rewrite [← size_trunc_eq_size npos x] at size_lt_size
  rewrite [← size_trunc_eq_size npos y] at size_lt_size
  exact le_of_lt (lt_of_size_lt_size size_lt_size)
| inr size_ge_size =>
  have ulp_eq_ulp : ulp n x = ulp n y := by
    apply congr_arg (fun w => 2 ^ (w - n))
    exact Nat.le_antisymm (Nat.size_le_size h) size_ge_size
  unfold trunc
  rewrite [ulp_eq_ulp]
  exact Nat.mul_le_mul_right _ (Nat.div_le_div_right h)
Proof state after:
no goals
Theorem: trunc_le_trunc
Proof state before:
case inl
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_lt_size : Nat.size x < Nat.size y
⊢ trunc n x ≤ trunc n y
Tactic:
rewrite [← size_trunc_eq_size npos x] at size_lt_size
Proof state after:
case inl
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_lt_size : Nat.size (trunc n x) < Nat.size y
⊢ trunc n x ≤ trunc n y
Theorem: trunc_le_trunc
Proof state before:
case inl
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_lt_size : Nat.size (trunc n x) < Nat.size y
⊢ trunc n x ≤ trunc n y
Tactic:
rewrite [← size_trunc_eq_size npos y] at size_lt_size
Proof state after:
case inl
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_lt_size : Nat.size (trunc n x) < Nat.size (trunc n y)
⊢ trunc n x ≤ trunc n y
Theorem: trunc_le_trunc
Proof state before:
case inl
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_lt_size : Nat.size (trunc n x) < Nat.size (trunc n y)
⊢ trunc n x ≤ trunc n y
Tactic:
exact le_of_lt (lt_of_size_lt_size size_lt_size)
Proof state after:
no goals
Theorem: trunc_le_trunc
Proof state before:
case inr
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
⊢ trunc n x ≤ trunc n y
Tactic:
have ulp_eq_ulp : ulp n x = ulp n y := by
  apply congr_arg (fun w => 2 ^ (w - n))
  exact Nat.le_antisymm (Nat.size_le_size h) size_ge_size
Proof state after:
case inr
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
ulp_eq_ulp : ulp n x = ulp n y
⊢ trunc n x ≤ trunc n y
Theorem: trunc_le_trunc
Proof state before:
case inr
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
ulp_eq_ulp : ulp n x = ulp n y
⊢ trunc n x ≤ trunc n y
Tactic:
unfold trunc
Proof state after:
case inr
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
ulp_eq_ulp : ulp n x = ulp n y
⊢ x / ulp n x * ulp n x ≤ y / ulp n y * ulp n y
Theorem: trunc_le_trunc
Proof state before:
case inr
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
ulp_eq_ulp : ulp n x = ulp n y
⊢ x / ulp n x * ulp n x ≤ y / ulp n y * ulp n y
Tactic:
rewrite [ulp_eq_ulp]
Proof state after:
case inr
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
ulp_eq_ulp : ulp n x = ulp n y
⊢ x / ulp n y * ulp n y ≤ y / ulp n y * ulp n y
Theorem: trunc_le_trunc
Proof state before:
case inr
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
ulp_eq_ulp : ulp n x = ulp n y
⊢ x / ulp n y * ulp n y ≤ y / ulp n y * ulp n y
Tactic:
exact Nat.mul_le_mul_right _ (Nat.div_le_div_right h)
Proof state after:
no goals
Theorem: trunc_le_trunc
Proof state before:
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
⊢ ulp n x = ulp n y
Tactic:
apply congr_arg (fun w => 2 ^ (w - n))
Proof state after:
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
⊢ Nat.size x = Nat.size y
Theorem: trunc_le_trunc
Proof state before:
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
⊢ Nat.size x = Nat.size y
Tactic:
exact Nat.le_antisymm (Nat.size_le_size h) size_ge_size
Proof state after:
no goals
Theorem: trunc_trunc_sub_ulp_eq
Proof state before:
n x : ℕ
npos : 0 < n
⊢ trunc n (trunc n x - ulp n x) = trunc n x - ulp n x
Tactic:
apply trunc_eq_of_le_of_ulp_dvd
Proof state after:
case hle
n x : ℕ
npos : 0 < n
⊢ trunc n x - ulp n x ≤ ?x

case hdvd
n x : ℕ
npos : 0 < n
⊢ ulp n ?x ∣ trunc n x - ulp n x

case x
n x : ℕ
npos : 0 < n
⊢ ℕ
Theorem: trunc_trunc_sub_ulp_eq
Proof state before:
case hle
n x : ℕ
npos : 0 < n
⊢ trunc n x - ulp n x ≤ ?x

case hdvd
n x : ℕ
npos : 0 < n
⊢ ulp n ?x ∣ trunc n x - ulp n x

case x
n x : ℕ
npos : 0 < n
⊢ ℕ
Tactic:
. exact tsub_le_self
Proof state after:
case hdvd
n x : ℕ
npos : 0 < n
⊢ ulp n (trunc n x) ∣ trunc n x - ulp n x
Theorem: trunc_trunc_sub_ulp_eq
Proof state before:
case hdvd
n x : ℕ
npos : 0 < n
⊢ ulp n (trunc n x) ∣ trunc n x - ulp n x
Tactic:
. rewrite [ulp_trunc npos]
  apply Nat.dvd_sub'
  . exact ulp_dvd_trunc n _
  . exact Nat.dvd_refl _
Proof state after:
no goals
Theorem: trunc_trunc_sub_ulp_eq
Proof state before:
case hle
n x : ℕ
npos : 0 < n
⊢ trunc n x - ulp n x ≤ ?x
Tactic:
exact tsub_le_self
Proof state after:
no goals
Theorem: trunc_trunc_sub_ulp_eq
Proof state before:
case hdvd
n x : ℕ
npos : 0 < n
⊢ ulp n (trunc n x) ∣ trunc n x - ulp n x
Tactic:
rewrite [ulp_trunc npos]
Proof state after:
case hdvd
n x : ℕ
npos : 0 < n
⊢ ulp n x ∣ trunc n x - ulp n x
Theorem: trunc_trunc_sub_ulp_eq
Proof state before:
case hdvd
n x : ℕ
npos : 0 < n
⊢ ulp n x ∣ trunc n x - ulp n x
Tactic:
apply Nat.dvd_sub'
Proof state after:
case hdvd.h₁
n x : ℕ
npos : 0 < n
⊢ ulp n x ∣ trunc n x

case hdvd.h₂
n x : ℕ
npos : 0 < n
⊢ ulp n x ∣ ulp n x
Theorem: trunc_trunc_sub_ulp_eq
Proof state before:
case hdvd.h₁
n x : ℕ
npos : 0 < n
⊢ ulp n x ∣ trunc n x

case hdvd.h₂
n x : ℕ
npos : 0 < n
⊢ ulp n x ∣ ulp n x
Tactic:
. exact ulp_dvd_trunc n _
Proof state after:
case hdvd.h₂
n x : ℕ
npos : 0 < n
⊢ ulp n x ∣ ulp n x
Theorem: trunc_trunc_sub_ulp_eq
Proof state before:
case hdvd.h₂
n x : ℕ
npos : 0 < n
⊢ ulp n x ∣ ulp n x
Tactic:
. exact Nat.dvd_refl _
Proof state after:
no goals
Theorem: trunc_trunc_sub_ulp_eq
Proof state before:
case hdvd.h₁
n x : ℕ
npos : 0 < n
⊢ ulp n x ∣ trunc n x
Tactic:
exact ulp_dvd_trunc n _
Proof state after:
no goals
Theorem: trunc_trunc_sub_ulp_eq
Proof state before:
case hdvd.h₂
n x : ℕ
npos : 0 < n
⊢ ulp n x ∣ ulp n x
Tactic:
exact Nat.dvd_refl _
Proof state after:
no goals
Theorem: trunc_sub_ulp_eq_of_trunc_eq
Proof state before:
n x : ℕ
npos : 0 < n
h : trunc n x = x
⊢ trunc n (x - ulp n x) = x - ulp n x
Tactic:
rewrite [← h, ulp_trunc npos]
Proof state after:
n x : ℕ
npos : 0 < n
h : trunc n x = x
⊢ trunc n (trunc n x - ulp n x) = trunc n x - ulp n x
Theorem: trunc_sub_ulp_eq_of_trunc_eq
Proof state before:
n x : ℕ
npos : 0 < n
h : trunc n x = x
⊢ trunc n (trunc n x - ulp n x) = trunc n x - ulp n x
Tactic:
exact trunc_trunc_sub_ulp_eq npos
Proof state after:
no goals
Theorem: ulp_pow_mul
Proof state before:
n x : ℕ
npos : 0 < n
h : n ≤ Nat.size x
k : ℕ
⊢ ulp n (2 ^ k * x) = 2 ^ k * ulp n x
Tactic:
unfold ulp expt
Proof state after:
n x : ℕ
npos : 0 < n
h : n ≤ Nat.size x
k : ℕ
⊢ 2 ^ (Nat.size (2 ^ k * x) - n) = 2 ^ k * 2 ^ (Nat.size x - n)
Theorem: ulp_pow_mul
Proof state before:
n x : ℕ
npos : 0 < n
h : n ≤ Nat.size x
k : ℕ
⊢ 2 ^ (Nat.size (2 ^ k * x) - n) = 2 ^ k * 2 ^ (Nat.size x - n)
Tactic:
have pos : 0 < x := by
  rewrite [← Nat.size_pos]
  exact Nat.lt_of_lt_of_le npos h
Proof state after:
n x : ℕ
npos : 0 < n
h : n ≤ Nat.size x
k : ℕ
pos : 0 < x
⊢ 2 ^ (Nat.size (2 ^ k * x) - n) = 2 ^ k * 2 ^ (Nat.size x - n)
Theorem: ulp_pow_mul
Proof state before:
n x : ℕ
npos : 0 < n
h : n ≤ Nat.size x
k : ℕ
pos : 0 < x
⊢ 2 ^ (Nat.size (2 ^ k * x) - n) = 2 ^ k * 2 ^ (Nat.size x - n)
Tactic:
rw [← pow_add, size_pow_mul pos, ← tsub_add_eq_add_tsub h, Nat.add_comm]
Proof state after:
no goals
Theorem: ulp_pow_mul
Proof state before:
n x : ℕ
npos : 0 < n
h : n ≤ Nat.size x
k : ℕ
⊢ 0 < x
Tactic:
rewrite [← Nat.size_pos]
Proof state after:
n x : ℕ
npos : 0 < n
h : n ≤ Nat.size x
k : ℕ
⊢ 0 < Nat.size x
Theorem: ulp_pow_mul
Proof state before:
n x : ℕ
npos : 0 < n
h : n ≤ Nat.size x
k : ℕ
⊢ 0 < Nat.size x
Tactic:
exact Nat.lt_of_lt_of_le npos h
Proof state after:
no goals
Theorem: trunc_pow_mul
Proof 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)]
Proof state after:
no goals
Theorem: trunc_pow_mul
Proof 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
Proof 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))
Theorem: trunc_pow_mul
Proof 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]
Proof state after:
no goals
Theorem: trunc_pow_mul
Proof 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)]
Proof state after:
no goals