internlm/Lean-Github huggingface dataset:
Theorem: sum_and_error₁_hi
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
hi : a + b ≤ round (a + b)
⊢ round (a + b) - round (round (round (a + b) - a) - b) = a + b
Tactic:
have hac : a ≤ round (a + b) := Nat.le_trans (Nat.le_add_right _ _) hi
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
hi : a + b ≤ round (a + b)
hac : a ≤ round (a + b)
⊢ round (a + b) - round (round (round (a + b) - a) - b) = a + b
Theorem: sum_and_error₁_hi
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
hi : a + b ≤ round (a + b)
hac : a ≤ round (a + b)
⊢ round (a + b) - round (round (round (a + b) - a) - b) = a + b
Tactic:
have hca : round (a + b) ≤ 2 * a := round_add_le npos hfaithful₀ hfaithful₁ hfa hba
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
hi : a + b ≤ round (a + b)
hac : a ≤ round (a + b)
hca : round (a + b) ≤ 2 * a
⊢ round (a + b) - round (round (round (a + b) - a) - b) = a + b
Theorem: sum_and_error₁_hi
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
hi : a + b ≤ round (a + b)
hac : a ≤ round (a + b)
hca : round (a + b) ≤ 2 * a
⊢ round (a + b) - round (round (round (a + b) - a) - b) = a + b
Tactic:
have hfc : trunc n (round (a + b)) = round (a + b) := trunc_round npos hfaithful₁ _
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
hi : a + b ≤ round (a + b)
hac : a ≤ round (a + b)
hca : round (a + b) ≤ 2 * a
hfc : trunc n (round (a + b)) = round (a + b)
⊢ round (a + b) - round (round (round (a + b) - a) - b) = a + b
Theorem: sum_and_error₁_hi
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
hi : a + b ≤ round (a + b)
hac : a ≤ round (a + b)
hca : round (a + b) ≤ 2 * a
hfc : trunc n (round (a + b)) = round (a + b)
⊢ round (a + b) - round (round (round (a + b) - a) - b) = a + b
Tactic:
have hfe : round (round (a + b) - a) = round (a + b) - a := by
  apply round_eq_of_trunc_eq npos hfaithful₀
  exact sterbenz hfc hfa hac hca
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
hi : a + b ≤ round (a + b)
hac : a ≤ round (a + b)
hca : round (a + b) ≤ 2 * a
hfc : trunc n (round (a + b)) = round (a + b)
hfe : round (round (a + b) - a) = round (a + b) - a
⊢ round (a + b) - round (round (round (a + b) - a) - b) = a + b
Theorem: sum_and_error₁_hi
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
hi : a + b ≤ round (a + b)
hac : a ≤ round (a + b)
hca : round (a + b) ≤ 2 * a
hfc : trunc n (round (a + b)) = round (a + b)
hfe : round (round (a + b) - a) = round (a + b) - a
⊢ round (a + b) - round (round (round (a + b) - a) - b) = a + b
Tactic:
have ⟨_, hfr₂⟩ := a₁ npos hfaithful₀ hfaithful₁ hcorrect₁ hfa hfb
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
hi : a + b ≤ round (a + b)
hac : a ≤ round (a + b)
hca : round (a + b) ≤ 2 * a
hfc : trunc n (round (a + b)) = round (a + b)
hfe : round (round (a + b) - a) = round (a + b) - a
left✝ : trunc n (a + b - round (a + b)) = a + b - round (a + b)
hfr₂ : trunc n (round (a + b) - (a + b)) = round (a + b) - (a + b)
⊢ round (a + b) - round (round (round (a + b) - a) - b) = a + b
Theorem: sum_and_error₁_hi
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
hi : a + b ≤ round (a + b)
hac : a ≤ round (a + b)
hca : round (a + b) ≤ 2 * a
hfc : trunc n (round (a + b)) = round (a + b)
hfe : round (round (a + b) - a) = round (a + b) - a
left✝ : trunc n (a + b - round (a + b)) = a + b - round (a + b)
hfr₂ : trunc n (round (a + b) - (a + b)) = round (a + b) - (a + b)
⊢ round (a + b) - round (round (round (a + b) - a) - b) = a + b
Tactic:
rewrite [hfe]
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
hi : a + b ≤ round (a + b)
hac : a ≤ round (a + b)
hca : round (a + b) ≤ 2 * a
hfc : trunc n (round (a + b)) = round (a + b)
hfe : round (round (a + b) - a) = round (a + b) - a
left✝ : trunc n (a + b - round (a + b)) = a + b - round (a + b)
hfr₂ : trunc n (round (a + b) - (a + b)) = round (a + b) - (a + b)
⊢ round (a + b) - round (round (a + b) - a - b) = a + b
Theorem: sum_and_error₁_hi
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
hi : a + b ≤ round (a + b)
hac : a ≤ round (a + b)
hca : round (a + b) ≤ 2 * a
hfc : trunc n (round (a + b)) = round (a + b)
hfe : round (round (a + b) - a) = round (a + b) - a
left✝ : trunc n (a + b - round (a + b)) = a + b - round (a + b)
hfr₂ : trunc n (round (a + b) - (a + b)) = round (a + b) - (a + b)
⊢ round (a + b) - round (round (a + b) - a - b) = a + b
Tactic:
rewrite [tsub_tsub]
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
hi : a + b ≤ round (a + b)
hac : a ≤ round (a + b)
hca : round (a + b) ≤ 2 * a
hfc : trunc n (round (a + b)) = round (a + b)
hfe : round (round (a + b) - a) = round (a + b) - a
left✝ : trunc n (a + b - round (a + b)) = a + b - round (a + b)
hfr₂ : trunc n (round (a + b) - (a + b)) = round (a + b) - (a + b)
⊢ round (a + b) - round (round (a + b) - (a + b)) = a + b
Theorem: sum_and_error₁_hi
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
hi : a + b ≤ round (a + b)
hac : a ≤ round (a + b)
hca : round (a + b) ≤ 2 * a
hfc : trunc n (round (a + b)) = round (a + b)
hfe : round (round (a + b) - a) = round (a + b) - a
left✝ : trunc n (a + b - round (a + b)) = a + b - round (a + b)
hfr₂ : trunc n (round (a + b) - (a + b)) = round (a + b) - (a + b)
⊢ round (a + b) - round (round (a + b) - (a + b)) = a + b
Tactic:
rewrite [round_eq_of_trunc_eq npos hfaithful₀ hfr₂]
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
hi : a + b ≤ round (a + b)
hac : a ≤ round (a + b)
hca : round (a + b) ≤ 2 * a
hfc : trunc n (round (a + b)) = round (a + b)
hfe : round (round (a + b) - a) = round (a + b) - a
left✝ : trunc n (a + b - round (a + b)) = a + b - round (a + b)
hfr₂ : trunc n (round (a + b) - (a + b)) = round (a + b) - (a + b)
⊢ round (a + b) - (round (a + b) - (a + b)) = a + b
Theorem: sum_and_error₁_hi
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
hi : a + b ≤ round (a + b)
hac : a ≤ round (a + b)
hca : round (a + b) ≤ 2 * a
hfc : trunc n (round (a + b)) = round (a + b)
hfe : round (round (a + b) - a) = round (a + b) - a
left✝ : trunc n (a + b - round (a + b)) = a + b - round (a + b)
hfr₂ : trunc n (round (a + b) - (a + b)) = round (a + b) - (a + b)
⊢ round (a + b) - (round (a + b) - (a + b)) = a + b
Tactic:
exact tsub_tsub_cancel_of_le hi
Proof state after:
no goals
Theorem: sum_and_error₁_hi
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
hi : a + b ≤ round (a + b)
hac : a ≤ round (a + b)
hca : round (a + b) ≤ 2 * a
hfc : trunc n (round (a + b)) = round (a + b)
⊢ round (round (a + b) - a) = round (a + b) - a
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
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hi : a + b ≤ round (a + b)
hac : a ≤ round (a + b)
hca : round (a + b) ≤ 2 * a
hfc : trunc n (round (a + b)) = round (a + b)
⊢ trunc n (round (a + b) - a) = round (a + b) - a
Theorem: sum_and_error₁_hi
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
hi : a + b ≤ round (a + b)
hac : a ≤ round (a + b)
hca : round (a + b) ≤ 2 * a
hfc : trunc n (round (a + b)) = round (a + b)
⊢ trunc n (round (a + b) - a) = round (a + b) - a
Tactic:
exact sterbenz hfc hfa hac hca
Proof state after:
no goals
Theorem: b₁_of_round_eq
Proof state before:
round : ℕ → ℕ
n a b : ℕ
round_eq : round (a - b) = a - b
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
rewrite [round_eq, tsub_self, trunc_zero]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
round_eq : round (a - b) = a - b
⊢ 0 = 0 ∧ 0 = 0
Theorem: b₁_of_round_eq
Proof state before:
round : ℕ → ℕ
n a b : ℕ
round_eq : round (a - b) = a - b
⊢ 0 = 0 ∧ 0 = 0
Tactic:
exact ⟨rfl, rfl⟩
Proof state after:
no goals
Theorem: b₁_lo_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
lt_round : a - b < round (a - b)
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)
Tactic:
rewrite [round_eq_next_trunc_of_gt hfaithful₁ lt_round]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
lt_round : a - b < round (a - b)
⊢ trunc n (a - b - next n (trunc n (a - b))) = a - b - next n (trunc n (a - b))
Theorem: b₁_lo_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
lt_round : a - b < round (a - b)
⊢ trunc n (a - b - next n (trunc n (a - b))) = a - b - next n (trunc n (a - b))
Tactic:
rewrite [tsub_eq_zero_of_le $ Nat.le_of_lt $ lt_next_trunc npos _]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
lt_round : a - b < round (a - b)
⊢ trunc n 0 = 0
Theorem: b₁_lo_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
lt_round : a - b < round (a - b)
⊢ trunc n 0 = 0
Tactic:
exact trunc_zero n
Proof state after:
no goals
Theorem: b₁_hi_of_round_le
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
round_le : round (a - b) ≤ a - b
⊢ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
rewrite [round_eq_trunc_of_le npos hfaithful₁ round_le]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
round_le : round (a - b) ≤ a - b
⊢ trunc n (trunc n (a - b) - (a - b)) = trunc n (a - b) - (a - b)
Theorem: b₁_hi_of_round_le
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
round_le : round (a - b) ≤ a - b
⊢ trunc n (trunc n (a - b) - (a - b)) = trunc n (a - b) - (a - b)
Tactic:
rewrite [tsub_eq_zero_of_le (trunc_le n (a - b))]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
round_le : round (a - b) ≤ a - b
⊢ trunc n 0 = 0
Theorem: b₁_hi_of_round_le
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
round_le : round (a - b) ≤ a - b
⊢ trunc n 0 = 0
Tactic:
exact trunc_zero n
Proof state after:
no goals
Theorem: ulp_sub_le_of_two_mul_le_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
⊢ ulp n (a - b) - (a - b) % ulp n (a - b) ≤ b
Tactic:
have hba' : b ≤ a := Nat.le_trans (Nat.le_mul_of_pos_left two_pos) hba
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ ulp n (a - b) - (a - b) % ulp n (a - b) ≤ b
Theorem: ulp_sub_le_of_two_mul_le_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ ulp n (a - b) - (a - b) % ulp n (a - b) ≤ b
Tactic:
have h₁ : a ≤ b + round (a - b) := by
  trans b + (a - b)
  . rewrite [← add_tsub_assoc_of_le hba']
    exact Nat.le_of_eq $ Eq.symm $ add_tsub_cancel_left _ _
  . apply Nat.add_le_add_left
    exact lt_round.le
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
⊢ ulp n (a - b) - (a - b) % ulp n (a - b) ≤ b
Theorem: ulp_sub_le_of_two_mul_le_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
⊢ ulp n (a - b) - (a - b) % ulp n (a - b) ≤ b
Tactic:
have h₂ : a ≤ round (a - b) + b := by rwa [Nat.add_comm]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
⊢ ulp n (a - b) - (a - b) % ulp n (a - b) ≤ b
Theorem: ulp_sub_le_of_two_mul_le_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
⊢ ulp n (a - b) - (a - b) % ulp n (a - b) ≤ b
Tactic:
have h₃ : 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
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ ulp n (a - b) - (a - b) % ulp n (a - b) ≤ b
Theorem: ulp_sub_le_of_two_mul_le_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ ulp n (a - b) - (a - b) % ulp n (a - b) ≤ b
Tactic:
rewrite [← next_trunc_sub_eq_ulp_sub_mod npos]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ next n (trunc n (a - b)) - (a - b) ≤ b
Theorem: ulp_sub_le_of_two_mul_le_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ next n (trunc n (a - b)) - (a - b) ≤ b
Tactic:
rewrite [← round_eq_next_trunc_of_gt hfaithful₁ lt_round]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ round (a - b) - (a - b) ≤ b
Theorem: ulp_sub_le_of_two_mul_le_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ round (a - b) - (a - b) ≤ b
Tactic:
rewrite [← add_tsub_assoc' h₁ hba']
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ round (a - b) + b - a ≤ b
Theorem: ulp_sub_le_of_two_mul_le_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ round (a - b) + b - 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
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ b + round (a - b) - a ≤ b
Theorem: ulp_sub_le_of_two_mul_le_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ b + round (a - b) - a ≤ b
Tactic:
rewrite [add_tsub_assoc' h₂ h₃]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ b - (a - round (a - b)) ≤ b
Theorem: ulp_sub_le_of_two_mul_le_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ b - (a - round (a - b)) ≤ b
Tactic:
exact tsub_le_self
Proof state after:
no goals
Theorem: ulp_sub_le_of_two_mul_le_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ a ≤ b + round (a - b)
Tactic:
trans b + (a - b)
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ a ≤ b + (a - b)

round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ b + (a - b) ≤ b + round (a - b)
Theorem: ulp_sub_le_of_two_mul_le_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ a ≤ b + (a - b)

round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ b + (a - b) ≤ b + round (a - b)
Tactic:
. rewrite [← add_tsub_assoc_of_le hba']
  exact Nat.le_of_eq $ Eq.symm $ add_tsub_cancel_left _ _
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ b + (a - b) ≤ b + round (a - b)
Theorem: ulp_sub_le_of_two_mul_le_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ b + (a - b) ≤ b + round (a - b)
Tactic:
. apply Nat.add_le_add_left
  exact lt_round.le
Proof state after:
no goals
Theorem: ulp_sub_le_of_two_mul_le_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ a ≤ b + (a - b)
Tactic:
rewrite [← add_tsub_assoc_of_le hba']
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ a ≤ b + a - b
Theorem: ulp_sub_le_of_two_mul_le_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ a ≤ b + a - b
Tactic:
exact Nat.le_of_eq $ Eq.symm $ add_tsub_cancel_left _ _
Proof state after:
no goals
Theorem: ulp_sub_le_of_two_mul_le_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ b + (a - b) ≤ b + round (a - b)
Tactic:
apply Nat.add_le_add_left
Proof state after:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ a - b ≤ round (a - b)
Theorem: ulp_sub_le_of_two_mul_le_of_lt_round
Proof state before:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ a - b ≤ round (a - b)
Tactic:
exact lt_round.le
Proof state after:
no goals
Theorem: ulp_sub_le_of_two_mul_le_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
⊢ a ≤ round (a - b) + b
Tactic:
rwa [Nat.add_comm]
Proof state after:
no goals
Theorem: b₁_hi_of_two_mul_le_of_lt_round
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 : 2 * b ≤ a
lt_round : a - b < round (a - b)
⊢ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
rewrite [round_eq_next_trunc_of_gt hfaithful₁ lt_round]
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 : 2 * b ≤ a
lt_round : a - b < round (a - b)
⊢ trunc n (next n (trunc n (a - b)) - (a - b)) = next n (trunc n (a - b)) - (a - b)