internlm/Lean-Github huggingface dataset:
Theorem: b₁_lo_of_round_lt_of_ulp_le
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
hfe : round (a - round (a - b)) = a - round (a - b)
h₀ : b < round (a - round (a - b))
⊢ trunc n (round (a - round (a - b)) - b) = round (a - round (a - b)) - b
Tactic:
apply s₃ npos hfaithful₀ hfaithful₁ hfa hfb hfb hba le_rfl ulp_le h₀ h₀.le
Proof state after:
no goals
Theorem: b₁_lo_of_round_lt_of_ulp_le
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
⊢ round (a - round (a - b)) = a - round (a - b)
Tactic:
apply round_eq_of_trunc_eq npos hfaithful₀
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
⊢ trunc n (a - round (a - b)) = a - round (a - b)
Theorem: b₁_lo_of_round_lt_of_ulp_le
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
⊢ trunc n (a - round (a - b)) = a - round (a - b)
Tactic:
apply s₂ npos hfaithful₀ hfaithful₁ hfa hfb hba
Proof state after:
no goals
Theorem: b₁_lo_of_round_lt_of_ulp_le
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
hfe : round (a - round (a - b)) = a - round (a - b)
⊢ b < round (a - round (a - b))
Tactic:
rewrite [hfe]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
hfe : round (a - round (a - b)) = a - round (a - b)
⊢ b < a - round (a - b)
Theorem: b₁_lo_of_round_lt_of_ulp_le
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
hfe : round (a - round (a - b)) = a - round (a - b)
⊢ b < a - round (a - b)
Tactic:
rewrite [lt_tsub_comm]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
hfe : round (a - round (a - b)) = a - round (a - b)
⊢ round (a - b) < a - b
Theorem: b₁_lo_of_round_lt_of_ulp_le
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
hfe : round (a - round (a - b)) = a - round (a - b)
⊢ round (a - b) < a - b
Tactic:
exact round_lt
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
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)
Tactic:
have hca : round (a - b) ≤ a := round_sub_le npos hfaithful₀ hfaithful₁ b hfa
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
⊢ trunc n (a - b - round (a - b)) = a - b - round (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
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - 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_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)
⊢ trunc n (a - b - round (a - b)) = a - b - round (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)
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)
Tactic:
have hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b := by
  apply sterbenz
  . exact s₂ npos hfaithful₀ hfaithful₁ hfa hfb hba
  . exact hfb
  . rewrite [le_tsub_iff_left hca, ← le_tsub_iff_right hba]
    exact round_le
  . rewrite [round_eq_trunc_of_le npos hfaithful₁ round_le]
    rewrite [Nat.two_mul]
    rewrite [← tsub_le_iff_left]
    rewrite [tsub_right_comm]
    trans ulp n (a - b) / 2
    . rewrite [tsub_le_iff_left]
      apply le_midpoint_of_round_eq_trunc npos hcorrect₀
      exact round_eq_trunc_of_le npos hfaithful₁ round_le
    . 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:
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)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ trunc n (a - b - round (a - b)) = a - b - round (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)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)
Tactic:
rewrite [eq_tsub_iff_add_eq_of_le 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)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ trunc n (a - b - round (a - b)) + round (a - b) = 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)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ trunc n (a - b - round (a - b)) + round (a - b) = a - b
Tactic:
rewrite [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_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)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ round (a - b) + trunc n (a - b - round (a - b)) = 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)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ round (a - b) + trunc n (a - b - round (a - b)) = a - b
Tactic:
rewrite [tsub_right_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_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)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ round (a - b) + trunc n (a - round (a - b) - b) = 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)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ round (a - b) + trunc n (a - round (a - b) - b) = a - b
Tactic:
rewrite [hfd]
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)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ round (a - b) + (a - round (a - b) - b) = 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)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ round (a - b) + (a - round (a - b) - b) = a - b
Tactic:
rewrite [tsub_right_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_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)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ round (a - b) + (a - b - round (a - b)) = 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)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ round (a - b) + (a - b - round (a - b)) = a - b
Tactic:
exact add_tsub_cancel_of_le 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)
⊢ trunc n (a - round (a - b) - b) = a - round (a - b) - b
Tactic:
apply sterbenz
Proof state after:
case hfa
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)
⊢ trunc n (a - round (a - b)) = a - round (a - b)

case hfb
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)
⊢ trunc n b = b

case hba
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)
⊢ b ≤ a - round (a - b)

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 - round (a - b) ≤ 2 * b
Theorem: b₁_lo_of_of_round_le_of_no_uflow_of_of_ulp_le
Proof state before:
case hfa
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)
⊢ trunc n (a - round (a - b)) = a - round (a - b)

case hfb
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)
⊢ trunc n b = b

case hba
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)
⊢ b ≤ a - round (a - b)

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 - round (a - b) ≤ 2 * b
Tactic:
. exact s₂ npos hfaithful₀ hfaithful₁ hfa hfb hba
Proof state after:
case hfb
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)
⊢ trunc n b = b

case hba
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)
⊢ b ≤ a - round (a - b)

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 - round (a - b) ≤ 2 * b
Theorem: b₁_lo_of_of_round_le_of_no_uflow_of_of_ulp_le
Proof state before:
case hfb
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)
⊢ trunc n b = b

case hba
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)
⊢ b ≤ a - round (a - b)

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 - round (a - b) ≤ 2 * b
Tactic:
. exact hfb
Proof state after:
case hba
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)
⊢ b ≤ a - round (a - b)

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 - round (a - b) ≤ 2 * b
Theorem: b₁_lo_of_of_round_le_of_no_uflow_of_of_ulp_le
Proof state before:
case hba
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)
⊢ b ≤ a - round (a - b)

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 - round (a - b) ≤ 2 * b
Tactic:
. rewrite [le_tsub_iff_left hca, ← le_tsub_iff_right hba]
  exact round_le
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 - round (a - b) ≤ 2 * 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 - round (a - b) ≤ 2 * b
Tactic:
. rewrite [round_eq_trunc_of_le npos hfaithful₁ round_le]
  rewrite [Nat.two_mul]
  rewrite [← tsub_le_iff_left]
  rewrite [tsub_right_comm]
  trans ulp n (a - b) / 2
  . rewrite [tsub_le_iff_left]
    apply le_midpoint_of_round_eq_trunc npos hcorrect₀
    exact round_eq_trunc_of_le npos hfaithful₁ round_le
  . 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:
case hfa
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)
⊢ trunc n (a - round (a - b)) = a - round (a - b)
Tactic:
exact s₂ npos hfaithful₀ hfaithful₁ hfa hfb hba
Proof state after:
no goals
Theorem: b₁_lo_of_of_round_le_of_no_uflow_of_of_ulp_le
Proof state before:
case hfb
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)
⊢ trunc n b = b
Tactic:
exact hfb
Proof state after:
no goals
Theorem: b₁_lo_of_of_round_le_of_no_uflow_of_of_ulp_le
Proof state before:
case hba
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)
⊢ b ≤ a - round (a - b)
Tactic:
rewrite [le_tsub_iff_left hca, ← le_tsub_iff_right hba]
Proof state after:
case hba
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) ≤ a - b
Theorem: b₁_lo_of_of_round_le_of_no_uflow_of_of_ulp_le
Proof state before:
case hba
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) ≤ a - b
Tactic:
exact round_le
Proof state after:
no goals
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 - round (a - b) ≤ 2 * b
Tactic:
rewrite [round_eq_trunc_of_le npos hfaithful₁ round_le]
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) ≤ 2 * b