internlm/Lean-Github huggingface dataset:
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
size_lt_size : Nat.size (a - b) < Nat.size a
pow_lt : 2 ^ (Nat.size a - 1) / 2 < a - b
size_eq_size_sub_one : Nat.size (a - b) = Nat.size a - 1
size_add_one_eq_size : Nat.size (a - b) + 1 = Nat.size a
⊢ n ≤ Nat.size (a - b)
Tactic:
apply Nat.le_of_lt
Proof state after:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
size_lt_size : Nat.size (a - b) < Nat.size a
pow_lt : 2 ^ (Nat.size a - 1) / 2 < a - b
size_eq_size_sub_one : Nat.size (a - b) = Nat.size a - 1
size_add_one_eq_size : Nat.size (a - b) + 1 = Nat.size a
⊢ n < Nat.size (a - b)
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
size_lt_size : Nat.size (a - b) < Nat.size a
pow_lt : 2 ^ (Nat.size a - 1) / 2 < a - b
size_eq_size_sub_one : Nat.size (a - b) = Nat.size a - 1
size_add_one_eq_size : Nat.size (a - b) + 1 = Nat.size a
⊢ n < Nat.size (a - b)
Tactic:
rewrite [Nat.lt_size]
Proof state after:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
size_lt_size : Nat.size (a - b) < Nat.size a
pow_lt : 2 ^ (Nat.size a - 1) / 2 < a - b
size_eq_size_sub_one : Nat.size (a - b) = Nat.size a - 1
size_add_one_eq_size : Nat.size (a - b) + 1 = Nat.size a
⊢ 2 ^ n ≤ a - b
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
size_lt_size : Nat.size (a - b) < Nat.size a
pow_lt : 2 ^ (Nat.size a - 1) / 2 < a - b
size_eq_size_sub_one : Nat.size (a - b) = Nat.size a - 1
size_add_one_eq_size : Nat.size (a - b) + 1 = Nat.size a
⊢ 2 ^ n ≤ a - b
Tactic:
exact no_uflow
Proof state after:
no goals
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
size_lt_size : Nat.size (a - b) < Nat.size a
pow_lt : 2 ^ (Nat.size a - 1) / 2 < a - b
size_eq_size_sub_one : Nat.size (a - b) = Nat.size a - 1
size_add_one_eq_size : Nat.size (a - b) + 1 = Nat.size a
le_size : n ≤ Nat.size (a - b)
⊢ 2 * ulp n (a - b) = ulp n a
Tactic:
rewrite [← pow_one 2]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
size_lt_size : Nat.size (a - b) < Nat.size a
pow_lt : 2 ^ (Nat.size a - 1) / 2 < a - b
size_eq_size_sub_one : Nat.size (a - b) = Nat.size a - 1
size_add_one_eq_size : Nat.size (a - b) + 1 = Nat.size a
le_size : n ≤ Nat.size (a - b)
⊢ 2 ^ 1 * ulp n (a - b) = ulp n a
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
size_lt_size : Nat.size (a - b) < Nat.size a
pow_lt : 2 ^ (Nat.size a - 1) / 2 < a - b
size_eq_size_sub_one : Nat.size (a - b) = Nat.size a - 1
size_add_one_eq_size : Nat.size (a - b) + 1 = Nat.size a
le_size : n ≤ Nat.size (a - b)
⊢ 2 ^ 1 * ulp n (a - b) = ulp n a
Tactic:
unfold ulp expt
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
size_lt_size : Nat.size (a - b) < Nat.size a
pow_lt : 2 ^ (Nat.size a - 1) / 2 < a - b
size_eq_size_sub_one : Nat.size (a - b) = Nat.size a - 1
size_add_one_eq_size : Nat.size (a - b) + 1 = Nat.size a
le_size : n ≤ Nat.size (a - b)
⊢ 2 ^ 1 * 2 ^ (Nat.size (a - b) - n) = 2 ^ (Nat.size a - n)
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
size_lt_size : Nat.size (a - b) < Nat.size a
pow_lt : 2 ^ (Nat.size a - 1) / 2 < a - b
size_eq_size_sub_one : Nat.size (a - b) = Nat.size a - 1
size_add_one_eq_size : Nat.size (a - b) + 1 = Nat.size a
le_size : n ≤ Nat.size (a - b)
⊢ 2 ^ 1 * 2 ^ (Nat.size (a - b) - n) = 2 ^ (Nat.size a - n)
Tactic:
rewrite [← pow_add]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
size_lt_size : Nat.size (a - b) < Nat.size a
pow_lt : 2 ^ (Nat.size a - 1) / 2 < a - b
size_eq_size_sub_one : Nat.size (a - b) = Nat.size a - 1
size_add_one_eq_size : Nat.size (a - b) + 1 = Nat.size a
le_size : n ≤ Nat.size (a - b)
⊢ 2 ^ (1 + (Nat.size (a - b) - n)) = 2 ^ (Nat.size a - n)
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
size_lt_size : Nat.size (a - b) < Nat.size a
pow_lt : 2 ^ (Nat.size a - 1) / 2 < a - b
size_eq_size_sub_one : Nat.size (a - b) = Nat.size a - 1
size_add_one_eq_size : Nat.size (a - b) + 1 = Nat.size a
le_size : n ≤ Nat.size (a - b)
⊢ 2 ^ (1 + (Nat.size (a - b) - n)) = 2 ^ (Nat.size a - n)
Tactic:
rewrite [Nat.add_comm]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
size_lt_size : Nat.size (a - b) < Nat.size a
pow_lt : 2 ^ (Nat.size a - 1) / 2 < a - b
size_eq_size_sub_one : Nat.size (a - b) = Nat.size a - 1
size_add_one_eq_size : Nat.size (a - b) + 1 = Nat.size a
le_size : n ≤ Nat.size (a - b)
⊢ 2 ^ (Nat.size (a - b) - n + 1) = 2 ^ (Nat.size a - n)
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
size_lt_size : Nat.size (a - b) < Nat.size a
pow_lt : 2 ^ (Nat.size a - 1) / 2 < a - b
size_eq_size_sub_one : Nat.size (a - b) = Nat.size a - 1
size_add_one_eq_size : Nat.size (a - b) + 1 = Nat.size a
le_size : n ≤ Nat.size (a - b)
⊢ 2 ^ (Nat.size (a - b) - n + 1) = 2 ^ (Nat.size a - n)
Tactic:
rewrite [tsub_add_eq_add_tsub le_size]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
size_lt_size : Nat.size (a - b) < Nat.size a
pow_lt : 2 ^ (Nat.size a - 1) / 2 < a - b
size_eq_size_sub_one : Nat.size (a - b) = Nat.size a - 1
size_add_one_eq_size : Nat.size (a - b) + 1 = Nat.size a
le_size : n ≤ Nat.size (a - b)
⊢ 2 ^ (Nat.size (a - b) + 1 - n) = 2 ^ (Nat.size a - n)
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
size_lt_size : Nat.size (a - b) < Nat.size a
pow_lt : 2 ^ (Nat.size a - 1) / 2 < a - b
size_eq_size_sub_one : Nat.size (a - b) = Nat.size a - 1
size_add_one_eq_size : Nat.size (a - b) + 1 = Nat.size a
le_size : n ≤ Nat.size (a - b)
⊢ 2 ^ (Nat.size (a - b) + 1 - n) = 2 ^ (Nat.size a - n)
Tactic:
apply congr_arg (fun w => 2 ^ (w - n))
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
size_lt_size : Nat.size (a - b) < Nat.size a
pow_lt : 2 ^ (Nat.size a - 1) / 2 < a - b
size_eq_size_sub_one : Nat.size (a - b) = Nat.size a - 1
size_add_one_eq_size : Nat.size (a - b) + 1 = Nat.size a
le_size : n ≤ Nat.size (a - b)
⊢ Nat.size (a - b) + 1 = Nat.size a
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
size_lt_size : Nat.size (a - b) < Nat.size a
pow_lt : 2 ^ (Nat.size a - 1) / 2 < a - b
size_eq_size_sub_one : Nat.size (a - b) = Nat.size a - 1
size_add_one_eq_size : Nat.size (a - b) + 1 = Nat.size a
le_size : n ≤ Nat.size (a - b)
⊢ Nat.size (a - b) + 1 = Nat.size a
Tactic:
exact size_add_one_eq_size
Proof state after:
no goals
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
⊢ 1 ≤ Nat.size a - n
Tactic:
apply Nat.one_le_of_lt
Proof state after:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
⊢ ?n < Nat.size a - n

case n
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
⊢ ℕ
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
⊢ ?n < Nat.size a - n

case n
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
⊢ ℕ
Tactic:
rewrite [tsub_pos_iff_lt]
Proof state after:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
⊢ n < Nat.size a
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
⊢ n < Nat.size a
Tactic:
exact lt_size
Proof state after:
no goals
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
one_le_size_sub : 1 ≤ Nat.size a - n
le_size_sub_one : n ≤ Nat.size a - 1
⊢ a - b - trunc n (a - b) = ulp n (a - b) - b
Tactic:
have k₁ : a = 2 ^ n * ulp n (a - b) := by
  rewrite [ulp_eq_half_ulp]
  unfold ulp expt
  conv => rhs ; right ; right ; rewrite [← pow_one 2]
  rewrite [Nat.pow_div one_le_size_sub two_pos, ← pow_add]
  rewrite [tsub_right_comm]
  rewrite [add_tsub_cancel_of_le le_size_sub_one]
  exact eq_pow
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
one_le_size_sub : 1 ≤ Nat.size a - n
le_size_sub_one : n ≤ Nat.size a - 1
k₁ : a = 2 ^ n * ulp n (a - b)
⊢ a - b - trunc n (a - b) = ulp n (a - b) - b