internlm/Lean-Github huggingface dataset:
Theorem: trunc_pow_mul
Proof 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
Proof 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
Theorem: trunc_pow_mul
Proof 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
Proof 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
Theorem: trunc_pow_mul
Proof 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]
Proof 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
Theorem: trunc_pow_mul
Proof 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
Proof state after:
no goals
Theorem: trunc_pow_mul
Proof 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]
Proof state after:
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
⊢ Nat.size x ≤ n
Theorem: trunc_pow_mul
Proof 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
Proof state after:
no goals
Theorem: trunc_pow_mul
Proof 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
Proof 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
Theorem: trunc_pow_mul
Proof 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
Proof 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
Theorem: trunc_pow_mul
Proof 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]
Proof 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
Theorem: trunc_pow_mul
Proof 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)]
Proof 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
Theorem: trunc_pow_mul
Proof 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]
Proof 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
Theorem: trunc_pow_mul
Proof 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
Proof 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
Theorem: trunc_pow_mul
Proof 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
Proof state after:
no goals
Theorem: trunc_pow_mul
Proof 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
Proof 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)
Theorem: trunc_pow_mul
Proof 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)]
Proof 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)
Theorem: trunc_pow_mul
Proof 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]
Proof 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)
Theorem: trunc_pow_mul
Proof 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)]
Proof state after:
no goals
Theorem: trunc_two_mul
Proof state before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ trunc n (2 * x) = 2 * trunc n x
Tactic:
rw [← pow_one 2, trunc_pow_mul npos x 1]
Proof state after:
no goals
Theorem: trunc_le_size_sub_ulp
Proof state before:
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a ≤ 2 ^ Nat.size a - ulp n a
Tactic:
rewrite [← size_trunc_eq_size npos]
Proof state after:
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a ≤ 2 ^ Nat.size (trunc n a) - ulp n a
Theorem: trunc_le_size_sub_ulp
Proof state before:
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a ≤ 2 ^ Nat.size (trunc n a) - ulp n a
Tactic:
rewrite [← ulp_trunc npos]
Proof state after:
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a ≤ 2 ^ Nat.size (trunc n a) - ulp n (trunc n a)
Theorem: trunc_le_size_sub_ulp
Proof state before:
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a ≤ 2 ^ Nat.size (trunc n a) - ulp n (trunc n a)
Tactic:
apply le_sub_of_dvd_of_dvd_of_lt
Proof state after:
case h₁
n : ℕ
npos : 0 < n
a : ℕ
⊢ ulp n (trunc n a) ∣ trunc n a

case h₂
n : ℕ
npos : 0 < n
a : ℕ
⊢ ulp n (trunc n a) ∣ 2 ^ Nat.size (trunc n a)

case h₃
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a < 2 ^ Nat.size (trunc n a)
Theorem: trunc_le_size_sub_ulp
Proof state before:
case h₁
n : ℕ
npos : 0 < n
a : ℕ
⊢ ulp n (trunc n a) ∣ trunc n a

case h₂
n : ℕ
npos : 0 < n
a : ℕ
⊢ ulp n (trunc n a) ∣ 2 ^ Nat.size (trunc n a)

case h₃
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a < 2 ^ Nat.size (trunc n a)
Tactic:
. exact ulp_dvd_of_trunc_eq (trunc_idempotent npos _)
Proof state after:
case h₂
n : ℕ
npos : 0 < n
a : ℕ
⊢ ulp n (trunc n a) ∣ 2 ^ Nat.size (trunc n a)

case h₃
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a < 2 ^ Nat.size (trunc n a)
Theorem: trunc_le_size_sub_ulp
Proof state before:
case h₂
n : ℕ
npos : 0 < n
a : ℕ
⊢ ulp n (trunc n a) ∣ 2 ^ Nat.size (trunc n a)

case h₃
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a < 2 ^ Nat.size (trunc n a)
Tactic:
. rewrite [ulp, expt, Nat.pow_dvd_pow_iff_le_right one_lt_two]
  exact tsub_le_self
Proof state after:
case h₃
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a < 2 ^ Nat.size (trunc n a)
Theorem: trunc_le_size_sub_ulp
Proof state before:
case h₃
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a < 2 ^ Nat.size (trunc n a)
Tactic:
. exact Nat.lt_size_self _
Proof state after:
no goals
Theorem: trunc_le_size_sub_ulp
Proof state before:
case h₁
n : ℕ
npos : 0 < n
a : ℕ
⊢ ulp n (trunc n a) ∣ trunc n a
Tactic:
exact ulp_dvd_of_trunc_eq (trunc_idempotent npos _)
Proof state after:
no goals
Theorem: trunc_le_size_sub_ulp
Proof state before:
case h₂
n : ℕ
npos : 0 < n
a : ℕ
⊢ ulp n (trunc n a) ∣ 2 ^ Nat.size (trunc n a)
Tactic:
rewrite [ulp, expt, Nat.pow_dvd_pow_iff_le_right one_lt_two]
Proof state after:
case h₂
n : ℕ
npos : 0 < n
a : ℕ
⊢ Nat.size (trunc n a) - n ≤ Nat.size (trunc n a)
Theorem: trunc_le_size_sub_ulp
Proof state before:
case h₂
n : ℕ
npos : 0 < n
a : ℕ
⊢ Nat.size (trunc n a) - n ≤ Nat.size (trunc n a)
Tactic:
exact tsub_le_self
Proof state after:
no goals
Theorem: trunc_le_size_sub_ulp
Proof state before:
case h₃
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a < 2 ^ Nat.size (trunc n a)
Tactic:
exact Nat.lt_size_self _
Proof state after:
no goals
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ n ≤ Nat.size a ∧ ulp n (a + b) = 2 * ulp n a
Tactic:
have size_eq : Nat.size (a + b) = Nat.size a + 1 := by
  apply Nat.le_antisymm
  . rewrite [Nat.size_le, pow_succ, Nat.two_mul]
    apply Nat.add_lt_add
    . exact Nat.lt_size_self _
    . exact Nat.lt_of_le_of_lt hba (Nat.lt_size_self _)
  . rewrite [Nat.succ_le, Nat.lt_size]
    exact carry
Proof state after:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
⊢ n ≤ Nat.size a ∧ ulp n (a + b) = 2 * ulp n a
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
⊢ n ≤ Nat.size a ∧ ulp n (a + b) = 2 * ulp n a
Tactic:
have le_size : n ≤ Nat.size a := by
  rewrite [← Nat.lt_succ, Nat.succ_eq_add_one]
  calc
    n < Nat.size (a + b) := by rwa [Nat.lt_size]
    _ = Nat.size a + 1   := size_eq
Proof state after:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
le_size : n ≤ Nat.size a
⊢ n ≤ Nat.size a ∧ ulp n (a + b) = 2 * ulp n a
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
le_size : n ≤ Nat.size a
⊢ n ≤ Nat.size a ∧ ulp n (a + b) = 2 * ulp n a
Tactic:
have ulp_eq : ulp n (a + b) = 2 * ulp n a := by
  calc
    ulp n (a + b)
      = 2 ^ (Nat.size (a + b) - n) := rfl
    _ = 2 ^ (Nat.size a + 1 - n)   := by rw [size_eq]
    _ = 2 ^ (Nat.size a - n + 1)   := by rw [← tsub_add_eq_add_tsub le_size]
    _ = 2 * 2 ^ (Nat.size a - n)   := by rw [pow_succ]
    _ = 2 * ulp n a                := rfl
Proof state after:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
⊢ n ≤ Nat.size a ∧ ulp n (a + b) = 2 * ulp n a
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
⊢ n ≤ Nat.size a ∧ ulp n (a + b) = 2 * ulp n a
Tactic:
exact ⟨le_size, ulp_eq⟩
Proof state after:
no goals
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ Nat.size (a + b) = Nat.size a + 1
Tactic:
apply Nat.le_antisymm
Proof state after:
case h₁
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ Nat.size (a + b) ≤ Nat.size a + 1

case h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ Nat.size a + 1 ≤ Nat.size (a + b)
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
case h₁
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ Nat.size (a + b) ≤ Nat.size a + 1

case h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ Nat.size a + 1 ≤ Nat.size (a + b)
Tactic:
. rewrite [Nat.size_le, pow_succ, Nat.two_mul]
  apply Nat.add_lt_add
  . exact Nat.lt_size_self _
  . exact Nat.lt_of_le_of_lt hba (Nat.lt_size_self _)
Proof state after:
case h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ Nat.size a + 1 ≤ Nat.size (a + b)
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
case h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ Nat.size a + 1 ≤ Nat.size (a + b)
Tactic:
. rewrite [Nat.succ_le, Nat.lt_size]
  exact carry
Proof state after:
no goals
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
case h₁
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ Nat.size (a + b) ≤ Nat.size a + 1
Tactic:
rewrite [Nat.size_le, pow_succ, Nat.two_mul]
Proof state after:
case h₁
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ a + b < 2 ^ Nat.size a + 2 ^ Nat.size a
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
case h₁
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ a + b < 2 ^ Nat.size a + 2 ^ Nat.size a
Tactic:
apply Nat.add_lt_add
Proof state after:
case h₁.h₁
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ a < 2 ^ Nat.size a

case h₁.h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ b < 2 ^ Nat.size a
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
case h₁.h₁
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ a < 2 ^ Nat.size a

case h₁.h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ b < 2 ^ Nat.size a
Tactic:
. exact Nat.lt_size_self _
Proof state after:
case h₁.h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ b < 2 ^ Nat.size a
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
case h₁.h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ b < 2 ^ Nat.size a
Tactic:
. exact Nat.lt_of_le_of_lt hba (Nat.lt_size_self _)
Proof state after:
no goals
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
case h₁.h₁
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ a < 2 ^ Nat.size a
Tactic:
exact Nat.lt_size_self _
Proof state after:
no goals
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
case h₁.h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ b < 2 ^ Nat.size a
Tactic:
exact Nat.lt_of_le_of_lt hba (Nat.lt_size_self _)
Proof state after:
no goals
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
case h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ Nat.size a + 1 ≤ Nat.size (a + b)
Tactic:
rewrite [Nat.succ_le, Nat.lt_size]
Proof state after:
case h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ 2 ^ Nat.size a ≤ a + b
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
case h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ 2 ^ Nat.size a ≤ a + b
Tactic:
exact carry
Proof state after:
no goals
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
⊢ n ≤ Nat.size a
Tactic:
rewrite [← Nat.lt_succ, Nat.succ_eq_add_one]
Proof state after:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
⊢ n < Nat.size a + 1
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
⊢ n < Nat.size a + 1
Tactic:
calc
  n < Nat.size (a + b) := by rwa [Nat.lt_size]
  _ = Nat.size a + 1   := size_eq
Proof state after:
no goals
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
⊢ n < Nat.size (a + b)
Tactic:
rwa [Nat.lt_size]
Proof state after:
no goals
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
le_size : n ≤ Nat.size a
⊢ ulp n (a + b) = 2 * ulp n a
Tactic:
calc
  ulp n (a + b)
    = 2 ^ (Nat.size (a + b) - n) := rfl
  _ = 2 ^ (Nat.size a + 1 - n)   := by rw [size_eq]
  _ = 2 ^ (Nat.size a - n + 1)   := by rw [← tsub_add_eq_add_tsub le_size]
  _ = 2 * 2 ^ (Nat.size a - n)   := by rw [pow_succ]
  _ = 2 * ulp n a                := rfl
Proof state after:
no goals
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
le_size : n ≤ Nat.size a
⊢ 2 ^ (Nat.size (a + b) - n) = 2 ^ (Nat.size a + 1 - n)
Tactic:
rw [size_eq]
Proof state after:
no goals
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
le_size : n ≤ Nat.size a
⊢ 2 ^ (Nat.size a + 1 - n) = 2 ^ (Nat.size a - n + 1)
Tactic:
rw [← tsub_add_eq_add_tsub le_size]
Proof state after:
no goals
Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry
Proof state before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
le_size : n ≤ Nat.size a
⊢ 2 ^ (Nat.size a - n + 1) = 2 * 2 ^ (Nat.size a - n)
Tactic:
rw [pow_succ]
Proof state after:
no goals
Theorem: size_next_le_succ_size
Proof state before:
n x : ℕ
⊢ Nat.size (next n x) ≤ Nat.size x + 1
Tactic:
rewrite [Nat.size_le, Nat.pow_succ, Nat.mul_two]
Proof state after:
n x : ℕ
⊢ next n x < 2 ^ Nat.size x + 2 ^ Nat.size x
Theorem: size_next_le_succ_size
Proof state before:
n x : ℕ
⊢ next n x < 2 ^ Nat.size x + 2 ^ Nat.size x
Tactic:
unfold next ulp
Proof state after:
n x : ℕ
⊢ x + 2 ^ expt n x < 2 ^ Nat.size x + 2 ^ Nat.size x
Theorem: size_next_le_succ_size
Proof state before:
n x : ℕ
⊢ x + 2 ^ expt n x < 2 ^ Nat.size x + 2 ^ Nat.size x
Tactic:
rewrite [Nat.add_comm, ← Nat.add_one_le_iff, add_rotate]
Proof state after:
n x : ℕ
⊢ x + 1 + 2 ^ expt n x ≤ 2 ^ Nat.size x + 2 ^ Nat.size x
Theorem: size_next_le_succ_size
Proof state before:
n x : ℕ
⊢ x + 1 + 2 ^ expt n x ≤ 2 ^ Nat.size x + 2 ^ Nat.size x
Tactic:
apply Nat.add_le_add
Proof state after:
case h₁
n x : ℕ
⊢ x + 1 ≤ 2 ^ Nat.size x

case h₂
n x : ℕ
⊢ 2 ^ expt n x ≤ 2 ^ Nat.size x
Theorem: size_next_le_succ_size
Proof state before:
case h₁
n x : ℕ
⊢ x + 1 ≤ 2 ^ Nat.size x

case h₂
n x : ℕ
⊢ 2 ^ expt n x ≤ 2 ^ Nat.size x
Tactic:
. exact Nat.lt_size_self x
Proof state after:
case h₂
n x : ℕ
⊢ 2 ^ expt n x ≤ 2 ^ Nat.size x
Theorem: size_next_le_succ_size
Proof state before:
case h₂
n x : ℕ
⊢ 2 ^ expt n x ≤ 2 ^ Nat.size x
Tactic:
. exact Nat.pow_le_pow_of_le_right two_pos tsub_le_self
Proof state after:
no goals
Theorem: size_next_le_succ_size
Proof state before:
case h₁
n x : ℕ
⊢ x + 1 ≤ 2 ^ Nat.size x
Tactic:
exact Nat.lt_size_self x
Proof state after:
no goals
Theorem: size_next_le_succ_size
Proof state before:
case h₂
n x : ℕ
⊢ 2 ^ expt n x ≤ 2 ^ Nat.size x
Tactic:
exact Nat.pow_le_pow_of_le_right two_pos tsub_le_self
Proof state after:
no goals
Theorem: size_next_eq_size_of_no_carry
Proof state before:
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ Nat.size (next n x) = Nat.size x
Tactic:
apply Nat.le_antisymm
Proof state after:
case h₁
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ Nat.size (next n x) ≤ Nat.size x

case h₂
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ Nat.size x ≤ Nat.size (next n x)
Theorem: size_next_eq_size_of_no_carry
Proof state before:
case h₁
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ Nat.size (next n x) ≤ Nat.size x

case h₂
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ Nat.size x ≤ Nat.size (next n x)
Tactic:
. rwa [Nat.size_le]
Proof state after:
case h₂
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ Nat.size x ≤ Nat.size (next n x)
Theorem: size_next_eq_size_of_no_carry
Proof state before:
case h₂
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ Nat.size x ≤ Nat.size (next n x)
Tactic:
. exact Nat.size_le_size (Nat.le_add_right _ _)
Proof state after:
no goals
Theorem: size_next_eq_size_of_no_carry
Proof state before:
case h₁
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ Nat.size (next n x) ≤ Nat.size x
Tactic:
rwa [Nat.size_le]
Proof state after:
no goals
Theorem: size_next_eq_size_of_no_carry
Proof state before:
case h₂
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ Nat.size x ≤ Nat.size (next n x)
Tactic:
exact Nat.size_le_size (Nat.le_add_right _ _)
Proof state after:
no goals
Theorem: size_next_eq_succ_size_of_carry
Proof state before:
n x : ℕ
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size (next n x) = Nat.size x + 1
Tactic:
apply Nat.le_antisymm
Proof state after:
case h₁
n x : ℕ
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size (next n x) ≤ Nat.size x + 1

case h₂
n x : ℕ
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 ≤ Nat.size (next n x)
Theorem: size_next_eq_succ_size_of_carry
Proof state before:
case h₁
n x : ℕ
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size (next n x) ≤ Nat.size x + 1

case h₂
n x : ℕ
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 ≤ Nat.size (next n x)
Tactic:
. exact size_next_le_succ_size n x
Proof state after:
case h₂
n x : ℕ
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 ≤ Nat.size (next n x)
Theorem: size_next_eq_succ_size_of_carry
Proof state before:
case h₂
n x : ℕ
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 ≤ Nat.size (next n x)
Tactic:
. rwa [Nat.add_one, Nat.succ_le, Nat.lt_size]
Proof state after:
no goals
Theorem: size_next_eq_succ_size_of_carry
Proof state before:
case h₁
n x : ℕ
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size (next n x) ≤ Nat.size x + 1
Tactic:
exact size_next_le_succ_size n x
Proof state after:
no goals
Theorem: size_next_eq_succ_size_of_carry
Proof state before:
case h₂
n x : ℕ
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 ≤ Nat.size (next n x)
Tactic:
rwa [Nat.add_one, Nat.succ_le, Nat.lt_size]
Proof state after:
no goals
Theorem: ulp_next_of_no_carry
Proof state before:
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ ulp n (next n x) = ulp n x
Tactic:
unfold ulp expt
Proof state after:
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ 2 ^ (Nat.size (next n x) - n) = 2 ^ (Nat.size x - n)
Theorem: ulp_next_of_no_carry
Proof state before:
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ 2 ^ (Nat.size (next n x) - n) = 2 ^ (Nat.size x - n)
Tactic:
rw [size_next_eq_size_of_no_carry no_carry]
Proof state after:
no goals
Theorem: trunc_next_of_no_carry
Proof state before:
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ trunc n (next n x) = trunc n x + ulp n x
Tactic:
rw [trunc, ulp_next_of_no_carry no_carry, next, trunc, ← Nat.succ_mul,
    Nat.add_div_right _ (ulp_pos n x)]
Proof state after:
no goals
Theorem: trunc_next_comm_of_no_carry
Proof state before:
n x : ℕ
npos : 0 < n
no_carry : next n x < 2 ^ Nat.size x
⊢ trunc n (next n x) = next n (trunc n x)
Tactic:
rw [trunc_next_of_no_carry no_carry, next, ulp_trunc npos x]
Proof state after:
no goals
Theorem: trunc_next_of_carry
Proof state before:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ trunc n (next n x) = 2 ^ Nat.size x
Tactic:
apply div_mul_eq_of_le_of_lt
Proof state after:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ expt n (next n x) ≤ Nat.size x

case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ 2 ^ Nat.size x ≤ next n x

case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ next n x < 2 ^ Nat.size x + 2 ^ expt n (next n x)