internlm/Lean-Github huggingface dataset:
Theorem: b₁_lo_of_of_round_le_of_no_uflow_of_of_ulp_le
Proof state before:
case hab
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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - trunc n (a - b) ≤ 2 * b
Tactic:
rewrite [Nat.two_mul]
Proof state after:
case hab
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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - trunc n (a - b) ≤ b + b
Theorem: b₁_lo_of_of_round_le_of_no_uflow_of_of_ulp_le
Proof state before:
case hab
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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - trunc n (a - b) ≤ b + b
Tactic:
rewrite [← tsub_le_iff_left]
Proof state after:
case hab
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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - trunc n (a - b) - b ≤ b
Theorem: b₁_lo_of_of_round_le_of_no_uflow_of_of_ulp_le
Proof state before:
case hab
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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - trunc n (a - b) - b ≤ b
Tactic:
rewrite [tsub_right_comm]
Proof state after:
case hab
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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - b - trunc n (a - b) ≤ b
Theorem: b₁_lo_of_of_round_le_of_no_uflow_of_of_ulp_le
Proof state before:
case hab
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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - b - trunc n (a - b) ≤ b
Tactic:
trans 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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - b - trunc n (a - b) ≤ ulp n (a - b) / 2

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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ ulp n (a - b) / 2 ≤ b
Theorem: b₁_lo_of_of_round_le_of_no_uflow_of_of_ulp_le
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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - b - trunc n (a - b) ≤ ulp n (a - b) / 2

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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ ulp n (a - b) / 2 ≤ b
Tactic:
. rewrite [tsub_le_iff_left]
  apply le_midpoint_of_round_eq_trunc npos hcorrect₀
  exact round_eq_trunc_of_le npos hfaithful₁ round_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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ ulp n (a - b) / 2 ≤ b
Theorem: b₁_lo_of_of_round_le_of_no_uflow_of_of_ulp_le
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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ ulp n (a - b) / 2 ≤ b
Tactic:
. refine Nat.le_of_mul_le_mul_left ?_ two_pos
  rewrite [Nat.mul_comm, Nat.div_mul_cancel ulp_even]
  exact ulp_le'
Proof state after:
no goals
Theorem: b₁_lo_of_of_round_le_of_no_uflow_of_of_ulp_le
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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - b - trunc n (a - b) ≤ ulp n (a - b) / 2
Tactic:
rewrite [tsub_le_iff_left]
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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - b ≤ trunc n (a - b) + ulp n (a - b) / 2
Theorem: b₁_lo_of_of_round_le_of_no_uflow_of_of_ulp_le
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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - b ≤ trunc n (a - b) + ulp n (a - b) / 2
Tactic:
apply le_midpoint_of_round_eq_trunc npos hcorrect₀
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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ round (a - b) = trunc n (a - b)
Theorem: b₁_lo_of_of_round_le_of_no_uflow_of_of_ulp_le
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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ round (a - b) = trunc n (a - b)
Tactic:
exact round_eq_trunc_of_le npos hfaithful₁ round_le
Proof state after:
no goals
Theorem: b₁_lo_of_of_round_le_of_no_uflow_of_of_ulp_le
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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ ulp n (a - b) / 2 ≤ b
Tactic:
refine Nat.le_of_mul_le_mul_left ?_ two_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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ 2 * (ulp n (a - b) / 2) ≤ 2 * b
Theorem: b₁_lo_of_of_round_le_of_no_uflow_of_of_ulp_le
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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ 2 * (ulp n (a - b) / 2) ≤ 2 * b
Tactic:
rewrite [Nat.mul_comm, Nat.div_mul_cancel ulp_even]
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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ ulp n (a - b) ≤ 2 * b
Theorem: b₁_lo_of_of_round_le_of_no_uflow_of_of_ulp_le
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_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ ulp n (a - b) ≤ 2 * b
Tactic:
exact ulp_le'
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
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)
Tactic:
apply b₁_lo_of_round_lt_of_ulp_le npos hfaithful₀ hfaithful₁ hfa hfb hba round_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 : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
⊢ ulp n a ≤ 2 * b
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
⊢ ulp n a ≤ 2 * b
Tactic:
have apos : 0 < a := Nat.lt_of_lt_of_le two_pow_pos $ Nat.le_trans no_uflow 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 : 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 n a ≤ 2 * b
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 n a ≤ 2 * b
Tactic:
have ulp_even : 2 ∣ ulp n a :=
  two_dvd_ulp_of_no_uflow $ Nat.le_trans no_uflow 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 : 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
⊢ ulp n a ≤ 2 * b
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
⊢ ulp n a ≤ 2 * b
Tactic:
have h₁ : round (a - b) = trunc n (a - b) := 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 : 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)
⊢ ulp n a ≤ 2 * b
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)
⊢ ulp n a ≤ 2 * b
Tactic:
have h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2 := by
  rewrite [← tsub_le_tsub_iff_left (Nat.mod_le _ _)]
  rewrite [← trunc_eq_sub_mod]
  rewrite [tsub_le_iff_right]
  exact le_midpoint_of_round_eq_trunc npos hcorrect₀ h₁
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 : 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
⊢ ulp n a ≤ 2 * b
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
⊢ ulp n a ≤ 2 * b
Tactic:
have h₃ : a - b = a - ulp n a + (ulp n a - b) := by
   rewrite [← add_tsub_assoc_of_le le_ulp]
   rw [tsub_add_cancel_of_le $ ulp_le_self npos apos]
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 : 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)
⊢ ulp n a ≤ 2 * b
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)
⊢ ulp n a ≤ 2 * b
Tactic:
have h₄ : (a - b) % ulp n (a - b) = ulp n a - b := by
  rewrite [ulp_eq_ulp]
  rewrite [h₃]
  rewrite [← Nat.mod_add_mod]
  rewrite [mod_sub_mod _ _ _ (ulp_le_self npos apos)]
  rewrite [Nat.mod_self, tsub_zero]
  rewrite [Nat.mod_eq_zero_of_dvd (ulp_dvd_of_trunc_eq hfa), Nat.zero_add]
  exact Nat.mod_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 : 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
⊢ ulp n a ≤ 2 * b
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
⊢ ulp n a ≤ 2 * b
Tactic:
have h₅ : ulp n a - b ≤ ulp n a / 2 := by
  rewrite [← h₄]
  rewrite [← ulp_eq_ulp]
  exact h₂
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 : 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 ≤ 2 * b
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 ≤ 2 * b
Tactic:
have h₆ : ulp n a / 2 ≤ b := by
  rewrite [← tsub_tsub_cancel_of_le le_ulp]
  rewrite [← sub_half_of_even ulp_even]
  apply tsub_le_tsub_left
  exact h₅
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 : 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
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:
rewrite [Nat.two_mul]
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 : 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 + b
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 + b
Tactic:
rewrite [← tsub_le_iff_left]
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 : 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 ≤ b