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
h₆ : ulp n a / 2 ≤ b
⊢ ulp n a - b ≤ b
Tactic:
trans ulp n a / 2
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : 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

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 - b ≤ ulp n a / 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_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:
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:
. 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)
⊢ (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
Tactic:
rewrite [← tsub_le_tsub_iff_left (Nat.mod_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)
⊢ a - b - ulp n (a - b) / 2 ≤ a - b - (a - b) % ulp n (a - 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)
⊢ a - b - ulp n (a - b) / 2 ≤ a - b - (a - b) % ulp n (a - b)
Tactic:
rewrite [← trunc_eq_sub_mod]
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)
⊢ a - b - ulp n (a - b) / 2 ≤ trunc n (a - 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)
⊢ a - b - ulp n (a - b) / 2 ≤ trunc n (a - b)
Tactic:
rewrite [tsub_le_iff_right]
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)
⊢ a - b ≤ trunc n (a - b) + ulp n (a - b) / 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:
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)
⊢ a - b ≤ trunc n (a - b) + ulp n (a - b) / 2
Tactic:
exact le_midpoint_of_round_eq_trunc npos hcorrect₀ 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
⊢ a - b = a - ulp n a + (ulp n a - b)
Tactic:
rewrite [← add_tsub_assoc_of_le le_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 : 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
⊢ a - b = a - ulp n a + ulp n a - 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
⊢ a - b = a - ulp n a + ulp n a - b
Tactic:
rw [tsub_add_cancel_of_le $ ulp_le_self npos apos]
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)
⊢ (a - b) % ulp n (a - b) = ulp n a - b
Tactic:
rewrite [ulp_eq_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 : 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)
⊢ (a - b) % ulp n a = ulp n a - 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)
⊢ (a - b) % ulp n a = ulp n a - b
Tactic:
rewrite [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)
⊢ (a - ulp n a + (ulp n a - b)) % ulp n a = ulp n a - 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)
⊢ (a - ulp n a + (ulp n a - b)) % ulp n a = ulp n a - b
Tactic:
rewrite [← Nat.mod_add_mod]
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)
⊢ ((a - ulp n a) % ulp n a + (ulp n a - b)) % ulp n a = ulp n a - 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)
⊢ ((a - ulp n a) % ulp n a + (ulp n a - b)) % ulp n a = ulp n a - b
Tactic:
rewrite [mod_sub_mod _ _ _ (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)
⊢ ((a - ulp n a % ulp n a) % ulp n a + (ulp n a - b)) % ulp n a = ulp n a - 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)
⊢ ((a - ulp n a % ulp n a) % ulp n a + (ulp n a - b)) % ulp n a = ulp n a - b
Tactic:
rewrite [Nat.mod_self, tsub_zero]
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)
⊢ (a % ulp n a + (ulp n a - b)) % ulp n a = ulp n a - 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)
⊢ (a % ulp n a + (ulp n a - b)) % ulp n a = ulp n a - b
Tactic:
rewrite [Nat.mod_eq_zero_of_dvd (ulp_dvd_of_trunc_eq hfa), Nat.zero_add]
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 - b) % ulp n a = ulp n a - 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 - b) % ulp n a = ulp n a - b
Tactic:
exact Nat.mod_eq_of_lt (tsub_lt_self (ulp_pos _ _) bpos)
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
⊢ ulp n a - b ≤ ulp n a / 2
Tactic:
rewrite [← 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
⊢ (a - b) % 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:
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
⊢ (a - b) % ulp n (a - b) ≤ ulp n a / 2
Tactic:
rewrite [← ulp_eq_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 : 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
⊢ (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 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:
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
⊢ (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 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
⊢ ulp n a / 2 ≤ b
Tactic:
rewrite [← tsub_tsub_cancel_of_le le_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 : 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 ≤ ulp n a - (ulp n a - 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 ≤ ulp n a - (ulp n a - b)
Tactic:
rewrite [← sub_half_of_even 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_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)