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)
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 = 2 ^ n * ulp n (a - b) - ulp n (a - b) + ulp n (a - b) - b
Tactic:
rewrite [tsub_add_cancel_of_le (Nat.le_mul_of_pos_left two_pow_pos)]
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 = 2 ^ n * ulp n (a - b) - 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:
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 = 2 ^ n * ulp n (a - b) - b
Tactic:
rw [← k₁]
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
k₁ : a = 2 ^ n * ulp n (a - b)
k₂ : a - b = (2 ^ n - 1) * ulp n (a - b) + (ulp n (a - b) - b)
⊢ trunc n (a - b) = (2 ^ n - 1) * ulp n (a - b)
Tactic:
unfold trunc
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)
k₂ : a - b = (2 ^ n - 1) * ulp n (a - b) + (ulp n (a - b) - b)
⊢ (a - b) / ulp n (a - b) * ulp n (a - b) = (2 ^ n - 1) * ulp 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:
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)
k₂ : a - b = (2 ^ n - 1) * ulp n (a - b) + (ulp n (a - b) - b)
⊢ (a - b) / ulp n (a - b) * ulp n (a - b) = (2 ^ n - 1) * ulp n (a - b)
Tactic:
conv => lhs ; left ; left ; rewrite [k₂]
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)
k₂ : a - b = (2 ^ n - 1) * ulp n (a - b) + (ulp n (a - b) - b)
⊢ ((2 ^ n - 1) * ulp n (a - b) + (ulp n (a - b) - b)) / ulp n (a - b) * ulp n (a - b) = (2 ^ n - 1) * ulp 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:
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)
k₂ : a - b = (2 ^ n - 1) * ulp n (a - b) + (ulp n (a - b) - b)
⊢ ((2 ^ n - 1) * ulp n (a - b) + (ulp n (a - b) - b)) / ulp n (a - b) * ulp n (a - b) = (2 ^ n - 1) * ulp n (a - b)
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)
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)
k₂ : a - b = (2 ^ n - 1) * ulp n (a - b) + (ulp n (a - b) - b)
⊢ (ulp n (a - b) - b + (2 ^ n - 1) * ulp n (a - b)) / ulp n (a - b) * ulp n (a - b) = (2 ^ n - 1) * ulp 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:
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)
k₂ : a - b = (2 ^ n - 1) * ulp n (a - b) + (ulp n (a - b) - b)
⊢ (ulp n (a - b) - b + (2 ^ n - 1) * ulp n (a - b)) / ulp n (a - b) * ulp n (a - b) = (2 ^ n - 1) * ulp n (a - b)
Tactic:
rewrite [Nat.add_mul_div_right _ _ (ulp_pos _ _)]
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)
k₂ : a - b = (2 ^ n - 1) * ulp n (a - b) + (ulp n (a - b) - b)
⊢ ((ulp n (a - b) - b) / ulp n (a - b) + (2 ^ n - 1)) * ulp n (a - b) = (2 ^ n - 1) * ulp 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:
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)
k₂ : a - b = (2 ^ n - 1) * ulp n (a - b) + (ulp n (a - b) - b)
⊢ ((ulp n (a - b) - b) / ulp n (a - b) + (2 ^ n - 1)) * ulp n (a - b) = (2 ^ n - 1) * ulp n (a - b)
Tactic:
rewrite [Nat.div_eq_of_lt (tsub_lt_self (ulp_pos _ _) bpos)]
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)
k₂ : a - b = (2 ^ n - 1) * ulp n (a - b) + (ulp n (a - b) - b)
⊢ (0 + (2 ^ n - 1)) * ulp n (a - b) = (2 ^ n - 1) * ulp 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:
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)
k₂ : a - b = (2 ^ n - 1) * ulp n (a - b) + (ulp n (a - b) - b)
⊢ (0 + (2 ^ n - 1)) * ulp n (a - b) = (2 ^ n - 1) * ulp n (a - b)
Tactic:
rw [Nat.zero_add]
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
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
⊢ ulp n (a - b) / 2 ≤ b
Tactic:
rewrite [← Nat.not_lt]
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
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
⊢ ¬b < ulp n (a - b) / 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:
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
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
⊢ ¬b < ulp n (a - b) / 2
Tactic:
intro (lt : b < ulp n (a - b) / 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)
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
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
lt : b < ulp n (a - b) / 2
⊢ False
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
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
lt : b < ulp n (a - b) / 2
⊢ False
Tactic:
have k₁ : ulp n (a - b) / 2 < ulp n (a - b) - b := by
  rewrite [lt_tsub_comm]
  rewrite [sub_half_of_even ulp_even]
  exact lt
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
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
lt : b < ulp n (a - b) / 2
k₁ : ulp n (a - b) / 2 < ulp n (a - b) - b
⊢ False
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
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
lt : b < ulp n (a - b) / 2
k₁ : ulp n (a - b) / 2 < ulp n (a - b) - b
⊢ False
Tactic:
have k₂ : ulp n (a - b) / 2 < a - b - trunc n (a - b) := by
  rewrite [h₂]
  exact k₁
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
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
lt : b < ulp n (a - b) / 2
k₁ : ulp n (a - b) / 2 < ulp n (a - b) - b
k₂ : ulp n (a - b) / 2 < a - b - trunc n (a - b)
⊢ False
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
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
lt : b < ulp n (a - b) / 2
k₁ : ulp n (a - b) / 2 < ulp n (a - b) - b
k₂ : ulp n (a - b) / 2 < a - b - trunc n (a - b)
⊢ False
Tactic:
have k₃ : a - b - trunc n (a - b) ≤ ulp n (a - b) / 2 := by
  rewrite [tsub_le_iff_left]
  apply le_midpoint_of_round_eq_trunc npos hcorrect₀
  exact round_eq_trunc_of_le npos hfaithful₁ round_lt.le
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
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
lt : b < ulp n (a - b) / 2
k₁ : ulp n (a - b) / 2 < ulp n (a - b) - b
k₂ : ulp n (a - b) / 2 < a - b - trunc n (a - b)
k₃ : a - b - trunc n (a - b) ≤ ulp n (a - b) / 2
⊢ False
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
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
lt : b < ulp n (a - b) / 2
k₁ : ulp n (a - b) / 2 < ulp n (a - b) - b
k₂ : ulp n (a - b) / 2 < a - b - trunc n (a - b)
k₃ : a - b - trunc n (a - b) ≤ ulp n (a - b) / 2
⊢ False
Tactic:
exact Nat.lt_le_asymm k₂ k₃
Proof state after:
no goals