internlm/Lean-Github huggingface dataset:
Theorem: a₁_hi_of_lt_round_of_ulp_sub_le
Proof state before:
case hdvd.h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
lt_round : a + b < round (a + b)
ulp_sub_le : ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
⊢ ulp n b ∣ a + b
Tactic:
apply Nat.dvd_add
Proof state after:
case hdvd.h₂.h₁
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
lt_round : a + b < round (a + b)
ulp_sub_le : ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
⊢ ulp n b ∣ a

case hdvd.h₂.h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
lt_round : a + b < round (a + b)
ulp_sub_le : ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
⊢ ulp n b ∣ b
Theorem: a₁_hi_of_lt_round_of_ulp_sub_le
Proof state before:
case hdvd.h₂.h₁
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
lt_round : a + b < round (a + b)
ulp_sub_le : ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
⊢ ulp n b ∣ a

case hdvd.h₂.h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
lt_round : a + b < round (a + b)
ulp_sub_le : ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
⊢ ulp n b ∣ b
Tactic:
. trans ulp n a
  . exact ulp_dvd_ulp n hba
  . exact ulp_dvd_of_trunc_eq hfa
Proof state after:
case hdvd.h₂.h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
lt_round : a + b < round (a + b)
ulp_sub_le : ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
⊢ ulp n b ∣ b
Theorem: a₁_hi_of_lt_round_of_ulp_sub_le
Proof state before:
case hdvd.h₂.h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
lt_round : a + b < round (a + b)
ulp_sub_le : ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
⊢ ulp n b ∣ b
Tactic:
. exact ulp_dvd_of_trunc_eq hfb
Proof state after:
no goals
Theorem: a₁_hi_of_lt_round_of_ulp_sub_le
Proof state before:
case hdvd.h₂.h₁
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
lt_round : a + b < round (a + b)
ulp_sub_le : ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
⊢ ulp n b ∣ a
Tactic:
trans ulp n a
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
lt_round : a + b < round (a + b)
ulp_sub_le : ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
⊢ ulp n b ∣ ulp n a

round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
lt_round : a + b < round (a + b)
ulp_sub_le : ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
⊢ ulp n a ∣ a
Theorem: a₁_hi_of_lt_round_of_ulp_sub_le
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
lt_round : a + b < round (a + b)
ulp_sub_le : ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
⊢ ulp n b ∣ ulp n a

round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
lt_round : a + b < round (a + b)
ulp_sub_le : ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
⊢ ulp n a ∣ a
Tactic:
. exact ulp_dvd_ulp n hba
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
lt_round : a + b < round (a + b)
ulp_sub_le : ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
⊢ ulp n a ∣ a
Theorem: a₁_hi_of_lt_round_of_ulp_sub_le
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
lt_round : a + b < round (a + b)
ulp_sub_le : ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
⊢ ulp n a ∣ a
Tactic:
. exact ulp_dvd_of_trunc_eq hfa
Proof state after:
no goals
Theorem: a₁_hi_of_lt_round_of_ulp_sub_le
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
lt_round : a + b < round (a + b)
ulp_sub_le : ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
⊢ ulp n b ∣ ulp n a
Tactic:
exact ulp_dvd_ulp n hba
Proof state after:
no goals
Theorem: a₁_hi_of_lt_round_of_ulp_sub_le
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
lt_round : a + b < round (a + b)
ulp_sub_le : ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
⊢ ulp n a ∣ a
Tactic:
exact ulp_dvd_of_trunc_eq hfa
Proof state after:
no goals
Theorem: a₁_hi_of_lt_round_of_ulp_sub_le
Proof state before:
case hdvd.h₂.h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
lt_round : a + b < round (a + b)
ulp_sub_le : ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
⊢ ulp n b ∣ b
Tactic:
exact ulp_dvd_of_trunc_eq hfb
Proof state after:
no goals
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
⊢ ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
Tactic:
have size_eq : Nat.size (a + b) = Nat.size a := by
  apply Nat.le_antisymm
  . exact Nat.size_le.mpr no_carry
  . exact Nat.size_le_size (Nat.le_add_right _ _)
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
⊢ ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
⊢ ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
Tactic:
have ulp_eq : ulp n (a + b) = ulp n a := by
  unfold ulp expt
  rw [size_eq]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
⊢ ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
⊢ ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
Tactic:
have ulp_le : ulp n a ≤ 2 * b := by
  have ⟨d, hd⟩ := two_dvd_ulp_of_no_uflow no_uflow
  rewrite [← ulp_eq, hd]
  apply Nat.mul_le_mul_left
  apply Nat.le_of_add_le_add_left (a := a)
  trans trunc n (a + b) + ulp n (a + b) / 2
  . rewrite [hd, Nat.mul_div_cancel_left _ two_pos]
    apply Nat.add_le_add_right
    trans trunc n a
    . exact hfa.ge
    . apply trunc_le_trunc npos
      exact Nat.le_add_right _ _
  . apply midpoint_le_of_round_eq_next_trunc npos hcorrect₁
    exact round_eq_next_trunc_of_gt hfaithful₁ lt_round
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
ulp_le : ulp n a ≤ 2 * b
⊢ ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
ulp_le : ulp n a ≤ 2 * b
⊢ ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
Tactic:
rewrite [ulp_eq, ← Nat.mod_add_mod,
    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
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
ulp_le : ulp n a ≤ 2 * b
⊢ ulp n a - b % ulp n a ≤ b
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
ulp_le : ulp n a ≤ 2 * b
⊢ ulp n a - b % ulp n a ≤ b
Tactic:
cases Nat.lt_or_ge b (ulp n a) with
| inl lt_ulp' =>
  rewrite [tsub_le_iff_right, Nat.mod_eq_of_lt lt_ulp', ← Nat.two_mul]
  exact ulp_le
| inr ulp_le' => exact Nat.le_trans tsub_le_self ulp_le'
Proof state after:
no goals
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
⊢ Nat.size (a + b) = Nat.size a
Tactic:
apply Nat.le_antisymm
Proof state after:
case h₁
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
⊢ Nat.size (a + b) ≤ Nat.size a

case h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
⊢ Nat.size a ≤ Nat.size (a + b)
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
case h₁
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
⊢ Nat.size (a + b) ≤ Nat.size a

case h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
⊢ Nat.size a ≤ Nat.size (a + b)
Tactic:
. exact Nat.size_le.mpr no_carry
Proof state after:
case h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
⊢ Nat.size a ≤ Nat.size (a + b)
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
case h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
⊢ Nat.size a ≤ Nat.size (a + b)
Tactic:
. exact Nat.size_le_size (Nat.le_add_right _ _)
Proof state after:
no goals
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
case h₁
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
⊢ Nat.size (a + b) ≤ Nat.size a
Tactic:
exact Nat.size_le.mpr no_carry
Proof state after:
no goals
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
case h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
⊢ Nat.size a ≤ Nat.size (a + b)
Tactic:
exact Nat.size_le_size (Nat.le_add_right _ _)
Proof state after:
no goals
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
⊢ ulp n (a + b) = ulp n a
Tactic:
unfold ulp expt
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
⊢ 2 ^ (Nat.size (a + b) - n) = 2 ^ (Nat.size a - n)
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
⊢ 2 ^ (Nat.size (a + b) - n) = 2 ^ (Nat.size a - n)
Tactic:
rw [size_eq]
Proof state after:
no goals
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
⊢ ulp n a ≤ 2 * b
Tactic:
have ⟨d, hd⟩ := two_dvd_ulp_of_no_uflow no_uflow
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ ulp n a ≤ 2 * b
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ ulp n a ≤ 2 * b
Tactic:
rewrite [← ulp_eq, hd]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ 2 * d ≤ 2 * b
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ 2 * d ≤ 2 * b
Tactic:
apply Nat.mul_le_mul_left
Proof state after:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ d ≤ b
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ d ≤ b
Tactic:
apply Nat.le_of_add_le_add_left (a := a)
Proof state after:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ a + d ≤ a + b
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ a + d ≤ a + b
Tactic:
trans trunc n (a + b) + ulp n (a + b) / 2
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ a + d ≤ trunc n (a + b) + ulp n (a + b) / 2

round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ trunc n (a + b) + ulp n (a + b) / 2 ≤ a + b
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ a + d ≤ trunc n (a + b) + ulp n (a + b) / 2

round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ trunc n (a + b) + ulp n (a + b) / 2 ≤ a + b
Tactic:
. rewrite [hd, Nat.mul_div_cancel_left _ two_pos]
  apply Nat.add_le_add_right
  trans trunc n a
  . exact hfa.ge
  . apply trunc_le_trunc npos
    exact Nat.le_add_right _ _
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ trunc n (a + b) + ulp n (a + b) / 2 ≤ a + b
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ trunc n (a + b) + ulp n (a + b) / 2 ≤ a + b
Tactic:
. apply midpoint_le_of_round_eq_next_trunc npos hcorrect₁
  exact round_eq_next_trunc_of_gt hfaithful₁ lt_round
Proof state after:
no goals
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ a + d ≤ trunc n (a + b) + ulp n (a + b) / 2
Tactic:
rewrite [hd, Nat.mul_div_cancel_left _ two_pos]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ a + d ≤ trunc n (a + b) + d
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ a + d ≤ trunc n (a + b) + d
Tactic:
apply Nat.add_le_add_right
Proof state after:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ a ≤ trunc n (a + b)
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ a ≤ trunc n (a + b)
Tactic:
trans trunc n a
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ a ≤ trunc n a

round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ trunc n a ≤ trunc n (a + b)
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ a ≤ trunc n a

round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ trunc n a ≤ trunc n (a + b)
Tactic:
. exact hfa.ge
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ trunc n a ≤ trunc n (a + b)
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ trunc n a ≤ trunc n (a + b)
Tactic:
. apply trunc_le_trunc npos
  exact Nat.le_add_right _ _
Proof state after:
no goals