internlm/Lean-Github huggingface dataset:
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_eq_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 : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
⊢ ulp n a - ulp n a / 2 ≤ ulp n a - (ulp n a - b)
Tactic:
apply tsub_le_tsub_left
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 : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
⊢ ulp n a - b ≤ ulp n a / 2
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_eq_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 : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
⊢ ulp n a - b ≤ ulp n a / 2
Tactic:
exact h₅
Proof state after:
no goals
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_eq_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 : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
h₆ : ulp n a / 2 ≤ b
⊢ ulp n a - b ≤ ulp n a / 2
Tactic:
exact h₅
Proof state after:
no goals
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_eq_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 : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
h₆ : ulp n a / 2 ≤ b
⊢ ulp n a / 2 ≤ b
Tactic:
exact h₆
Proof state after:
no goals
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ ulp n a ≤ ulp n (a - b)
Tactic:
unfold ulp expt
Proof state after:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - n) ≤ 2 ^ (Nat.size (a - b) - n)
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - n) ≤ 2 ^ (Nat.size (a - b) - n)
Tactic:
apply Nat.pow_le_pow_of_le_right two_pos
Proof state after:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ Nat.size a - n ≤ Nat.size (a - b) - n
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ Nat.size a - n ≤ Nat.size (a - b) - n
Tactic:
apply tsub_le_tsub_right
Proof state after:
case h
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ Nat.size a ≤ Nat.size (a - b)
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
case h
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ Nat.size a ≤ Nat.size (a - b)
Tactic:
apply Nat.le_of_pred_lt
Proof state after:
case h.a
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ Nat.pred (Nat.size a) < Nat.size (a - b)
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
case h.a
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ Nat.pred (Nat.size a) < Nat.size (a - b)
Tactic:
rewrite [← Nat.sub_one]
Proof state after:
case h.a
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ Nat.size a - 1 < Nat.size (a - b)
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
case h.a
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ Nat.size a - 1 < Nat.size (a - b)
Tactic:
rewrite [Nat.lt_size]
Proof state after:
case h.a
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) ≤ a - b
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
case h.a
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) ≤ a - b
Tactic:
trans 2 ^ (Nat.size a - 1) + (ulp n a - b)
Proof state after:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) ≤ 2 ^ (Nat.size a - 1) + (ulp n a - b)

n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) + (ulp n a - b) ≤ a - b
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) ≤ 2 ^ (Nat.size a - 1) + (ulp n a - b)

n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) + (ulp n a - b) ≤ a - b
Tactic:
. exact Nat.le_add_right _ _
Proof state after:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) + (ulp n a - b) ≤ a - b
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) + (ulp n a - b) ≤ a - b
Tactic:
. rewrite [← add_tsub_assoc_of_le le_ulp]
  apply tsub_le_tsub_right
  apply add_le_of_dvd_of_dvd_of_lt
  . exact ulp_dvd_of_trunc_eq hfa
  . unfold ulp expt
    rewrite [Nat.pow_dvd_pow_iff_le_right one_lt_two]
    apply tsub_le_tsub_left
    exact Nat.one_le_of_lt npos
  . exact size_lt
Proof state after:
no goals
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) ≤ 2 ^ (Nat.size a - 1) + (ulp n a - b)
Tactic:
exact Nat.le_add_right _ _
Proof state after:
no goals
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) + (ulp n a - b) ≤ a - b
Tactic:
rewrite [← add_tsub_assoc_of_le le_ulp]
Proof state after:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) + ulp n a - b ≤ a - b
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) + ulp n a - b ≤ a - b
Tactic:
apply tsub_le_tsub_right
Proof state after:
case h
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) + ulp n a ≤ a
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
case h
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) + ulp n a ≤ a
Tactic:
apply add_le_of_dvd_of_dvd_of_lt
Proof state after:
case h.h₁
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ ulp n a ∣ a

case h.h₂
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ ulp n a ∣ 2 ^ (Nat.size a - 1)

case h.h₃
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) < a
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
case h.h₁
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ ulp n a ∣ a

case h.h₂
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ ulp n a ∣ 2 ^ (Nat.size a - 1)

case h.h₃
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) < a
Tactic:
. exact ulp_dvd_of_trunc_eq hfa
Proof state after:
case h.h₂
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ ulp n a ∣ 2 ^ (Nat.size a - 1)

case h.h₃
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) < a
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
case h.h₂
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ ulp n a ∣ 2 ^ (Nat.size a - 1)

case h.h₃
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) < a
Tactic:
. unfold ulp expt
  rewrite [Nat.pow_dvd_pow_iff_le_right one_lt_two]
  apply tsub_le_tsub_left
  exact Nat.one_le_of_lt npos
Proof state after:
case h.h₃
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) < a
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
case h.h₃
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) < a
Tactic:
. exact size_lt
Proof state after:
no goals
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
case h.h₁
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ ulp n a ∣ a
Tactic:
exact ulp_dvd_of_trunc_eq hfa
Proof state after:
no goals
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
case h.h₂
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ ulp n a ∣ 2 ^ (Nat.size a - 1)
Tactic:
unfold ulp expt
Proof state after:
case h.h₂
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - n) ∣ 2 ^ (Nat.size a - 1)
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
case h.h₂
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - n) ∣ 2 ^ (Nat.size a - 1)
Tactic:
rewrite [Nat.pow_dvd_pow_iff_le_right one_lt_two]
Proof state after:
case h.h₂
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ Nat.size a - n ≤ Nat.size a - 1
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
case h.h₂
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ Nat.size a - n ≤ Nat.size a - 1
Tactic:
apply tsub_le_tsub_left
Proof state after:
case h.h₂.h
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 1 ≤ n
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
case h.h₂.h
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 1 ≤ n
Tactic:
exact Nat.one_le_of_lt npos
Proof state after:
no goals
Theorem: ulp_le_ulp_of_le_ulp_of_size_lt
Proof state before:
case h.h₃
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) < a
Tactic:
exact size_lt
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)
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)
Tactic:
apply b₁_lo_of_of_round_le_of_no_uflow_of_of_ulp_le
  npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
  round_lt.le no_uflow
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 n (a - b) ≤ 2 * 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 n (a - b) ≤ 2 * b
Tactic:
have ulp_even : 2 ∣ ulp n (a - b) := two_dvd_ulp_of_no_uflow no_uflow
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)
⊢ ulp n (a - b) ≤ 2 * 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)
⊢ ulp n (a - b) ≤ 2 * b
Tactic:
have lt_ulp : b < ulp n a := Nat.lt_of_le_of_lt le_ulp ulp_lt_ulp
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
⊢ ulp n (a - b) ≤ 2 * 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
⊢ ulp n (a - b) ≤ 2 * b
Tactic:
have lt_size : n < Nat.size a := by
  rewrite [Nat.lt_size]
  trans a - b
  . exact no_uflow
  . exact tsub_le_self
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
⊢ ulp n (a - b) ≤ 2 * 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
⊢ ulp n (a - b) ≤ 2 * b
Tactic:
have size_sub_one_pos : 0 < Nat.size a - 1 :=
  Nat.lt_of_lt_of_le npos $ Nat.le_pred_of_lt lt_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
⊢ ulp n (a - b) ≤ 2 * 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
⊢ ulp n (a - b) ≤ 2 * b
Tactic:
have size_pos : 0 < Nat.size a := Nat.lt_of_lt_of_le size_sub_one_pos tsub_le_self
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
⊢ ulp n (a - b) ≤ 2 * 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
⊢ ulp n (a - b) ≤ 2 * b
Tactic:
have apos : 0 < a := Nat.size_pos.mp size_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
⊢ ulp n (a - b) ≤ 2 * 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
⊢ ulp n (a - b) ≤ 2 * b
Tactic:
have eq_pow : a = 2 ^ (Nat.size a - 1) := by
  apply Nat.le_antisymm
  . rewrite [← Nat.not_lt]
    intro (size_lt : 2 ^ (Nat.size a - 1) < a)
    apply Nat.lt_le_asymm ulp_lt_ulp
    apply ulp_le_ulp_of_le_ulp_of_size_lt npos hfa lt_ulp.le size_lt
  . apply le_size_of_pos
    apply Nat.zero_lt_of_lt
    apply Nat.lt_of_le_of_lt
    . exact no_uflow.le
    . exact tsub_lt_self apos 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)
⊢ ulp n (a - b) ≤ 2 * 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)
⊢ ulp n (a - b) ≤ 2 * b
Tactic:
have even : 2 ∣ 2 ^ (Nat.size a - 1) := by
  apply dvd_pow_self 2
  apply Nat.not_eq_zero_of_lt
  exact size_sub_one_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 n (a - b) ≤ 2 * b