internlm/Lean-Github huggingface dataset:
Theorem: round_le_of_no_uflow_of_carry_of_lt_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
eq_pow : trunc n (a + b) = 2 ^ Nat.size a
lt_midpoint : a + b < trunc n (a + b) + ulp n (a + b) / 2
⊢ round (a + b) ≤ a + b
Tactic:
rewrite [round_eq_trunc_of_lt_midpoint npos hfaithful₀ hfaithful₁ hcorrect₁ lt_midpoint]
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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
eq_pow : trunc n (a + b) = 2 ^ Nat.size a
lt_midpoint : a + b < trunc n (a + b) + ulp n (a + b) / 2
⊢ trunc n (a + b) ≤ a + b
Theorem: round_le_of_no_uflow_of_carry_of_lt_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
eq_pow : trunc n (a + b) = 2 ^ Nat.size a
lt_midpoint : a + b < trunc n (a + b) + ulp n (a + b) / 2
⊢ trunc n (a + b) ≤ a + b
Tactic:
exact trunc_le _ _
Proof state after:
no goals
Theorem: round_le_of_no_uflow_of_carry_of_lt_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
⊢ a + b < 2 ^ Nat.size a + ulp n a
Tactic:
have ulp_le : ulp n a ≤ 2 ^ Nat.size a := by
  unfold ulp expt
  exact Nat.pow_le_pow_of_le_right two_pos tsub_le_self
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ 2 ^ Nat.size a
⊢ a + b < 2 ^ Nat.size a + ulp n a
Theorem: round_le_of_no_uflow_of_carry_of_lt_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ 2 ^ Nat.size a
⊢ a + b < 2 ^ Nat.size a + ulp n a
Tactic:
rewrite [← tsub_add_cancel_of_le 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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ 2 ^ Nat.size a
⊢ a + b < 2 ^ Nat.size a - ulp n a + ulp n a + ulp n a
Theorem: round_le_of_no_uflow_of_carry_of_lt_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ 2 ^ Nat.size a
⊢ a + b < 2 ^ Nat.size a - ulp n a + ulp n a + ulp n a
Tactic:
rewrite [Nat.add_assoc]
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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ 2 ^ Nat.size a
⊢ a + b < 2 ^ Nat.size a - ulp n a + (ulp n a + ulp n a)
Theorem: round_le_of_no_uflow_of_carry_of_lt_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ 2 ^ Nat.size a
⊢ a + b < 2 ^ Nat.size a - ulp n a + (ulp n a + ulp n a)
Tactic:
rewrite [← Nat.two_mul]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ 2 ^ Nat.size a
⊢ a + b < 2 ^ Nat.size a - ulp n a + 2 * ulp n a
Theorem: round_le_of_no_uflow_of_carry_of_lt_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ 2 ^ Nat.size a
⊢ a + b < 2 ^ Nat.size a - ulp n a + 2 * ulp n a
Tactic:
rewrite [← ulp_eq]
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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ 2 ^ Nat.size a
⊢ a + b < 2 ^ Nat.size a - ulp n a + ulp n (a + b)
Theorem: round_le_of_no_uflow_of_carry_of_lt_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ 2 ^ Nat.size a
⊢ a + b < 2 ^ Nat.size a - ulp n a + ulp n (a + b)
Tactic:
apply add_lt_add_of_le_of_lt
Proof state after:
case h₁
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ 2 ^ Nat.size a
⊢ a ≤ 2 ^ Nat.size a - ulp n a

case h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ 2 ^ Nat.size a
⊢ b < ulp n (a + b)
Theorem: round_le_of_no_uflow_of_carry_of_lt_ulp
Proof state before:
case h₁
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ 2 ^ Nat.size a
⊢ a ≤ 2 ^ Nat.size a - ulp n a

case h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ 2 ^ Nat.size a
⊢ b < ulp n (a + b)
Tactic:
. exact le_size_sub_ulp_of_trunc_eq npos hfa
Proof state after:
case h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ 2 ^ Nat.size a
⊢ b < ulp n (a + b)
Theorem: round_le_of_no_uflow_of_carry_of_lt_ulp
Proof state before:
case h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ 2 ^ Nat.size a
⊢ b < ulp n (a + b)
Tactic:
. exact lt_ulp
Proof state after:
no goals
Theorem: round_le_of_no_uflow_of_carry_of_lt_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
⊢ ulp n a ≤ 2 ^ Nat.size a
Tactic:
unfold ulp expt
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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
⊢ 2 ^ (Nat.size a - n) ≤ 2 ^ Nat.size a
Theorem: round_le_of_no_uflow_of_carry_of_lt_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
⊢ 2 ^ (Nat.size a - n) ≤ 2 ^ Nat.size a
Tactic:
exact Nat.pow_le_pow_of_le_right two_pos tsub_le_self
Proof state after:
no goals
Theorem: round_le_of_no_uflow_of_carry_of_lt_ulp
Proof state before:
case h₁
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ 2 ^ Nat.size a
⊢ a ≤ 2 ^ Nat.size a - ulp n a
Tactic:
exact le_size_sub_ulp_of_trunc_eq npos hfa
Proof state after:
no goals
Theorem: round_le_of_no_uflow_of_carry_of_lt_ulp
Proof state before:
case h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ 2 ^ Nat.size a
⊢ b < ulp n (a + b)
Tactic:
exact lt_ulp
Proof state after:
no goals
Theorem: round_le_of_no_uflow_of_carry_of_lt_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
⊢ trunc n (a + b) = 2 ^ Nat.size a
Tactic:
have pow_size_eq_pow_mul_ulp : 2 ^ Nat.size a = 2 ^ n * ulp n a := by
  unfold ulp expt
  rewrite [← pow_add]
  rw [add_tsub_cancel_of_le le_size]
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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
pow_size_eq_pow_mul_ulp : 2 ^ Nat.size a = 2 ^ n * ulp n a
⊢ trunc n (a + b) = 2 ^ Nat.size a
Theorem: round_le_of_no_uflow_of_carry_of_lt_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
pow_size_eq_pow_mul_ulp : 2 ^ Nat.size a = 2 ^ n * ulp n a
⊢ trunc n (a + b) = 2 ^ Nat.size a
Tactic:
have div_ulp_eq_pow : (a + b) / ulp n a = 2 ^ n := by
  apply Nat.eq_of_mul_eq_mul_right (ulp_pos n a)
  apply div_mul_eq_of_dvd_of_le_of_lt
  . exact Nat.dvd_mul_left _ _
  . exact pow_size_eq_pow_mul_ulp.ge.trans carry
  . apply Nat.lt_of_lt_of_le add_lt_pow_add_ulp
    rw [pow_size_eq_pow_mul_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
pow_size_eq_pow_mul_ulp : 2 ^ Nat.size a = 2 ^ n * ulp n a
div_ulp_eq_pow : (a + b) / ulp n a = 2 ^ n
⊢ trunc n (a + b) = 2 ^ Nat.size a
Theorem: round_le_of_no_uflow_of_carry_of_lt_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
pow_size_eq_pow_mul_ulp : 2 ^ Nat.size a = 2 ^ n * ulp n a
div_ulp_eq_pow : (a + b) / ulp n a = 2 ^ n
⊢ trunc n (a + b) = 2 ^ Nat.size a
Tactic:
unfold trunc
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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
pow_size_eq_pow_mul_ulp : 2 ^ Nat.size a = 2 ^ n * ulp n a
div_ulp_eq_pow : (a + b) / ulp n a = 2 ^ n
⊢ (a + b) / ulp n (a + b) * ulp n (a + b) = 2 ^ Nat.size a
Theorem: round_le_of_no_uflow_of_carry_of_lt_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
pow_size_eq_pow_mul_ulp : 2 ^ Nat.size a = 2 ^ n * ulp n a
div_ulp_eq_pow : (a + b) / ulp n a = 2 ^ n
⊢ (a + b) / ulp n (a + b) * ulp n (a + b) = 2 ^ Nat.size a
Tactic:
rewrite [ulp_eq]
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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
pow_size_eq_pow_mul_ulp : 2 ^ Nat.size a = 2 ^ n * ulp n a
div_ulp_eq_pow : (a + b) / ulp n a = 2 ^ n
⊢ (a + b) / (2 * ulp n a) * (2 * ulp n a) = 2 ^ Nat.size a
Theorem: round_le_of_no_uflow_of_carry_of_lt_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
pow_size_eq_pow_mul_ulp : 2 ^ Nat.size a = 2 ^ n * ulp n a
div_ulp_eq_pow : (a + b) / ulp n a = 2 ^ n
⊢ (a + b) / (2 * ulp n a) * (2 * ulp n a) = 2 ^ Nat.size a
Tactic:
rewrite [← Nat.mul_assoc]
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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
pow_size_eq_pow_mul_ulp : 2 ^ Nat.size a = 2 ^ n * ulp n a
div_ulp_eq_pow : (a + b) / ulp n a = 2 ^ n
⊢ (a + b) / (2 * ulp n a) * 2 * ulp n a = 2 ^ Nat.size a
Theorem: round_le_of_no_uflow_of_carry_of_lt_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
pow_size_eq_pow_mul_ulp : 2 ^ Nat.size a = 2 ^ n * ulp n a
div_ulp_eq_pow : (a + b) / ulp n a = 2 ^ n
⊢ (a + b) / (2 * ulp n a) * 2 * ulp n a = 2 ^ Nat.size a
Tactic:
rewrite [Nat.mul_comm 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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
pow_size_eq_pow_mul_ulp : 2 ^ Nat.size a = 2 ^ n * ulp n a
div_ulp_eq_pow : (a + b) / ulp n a = 2 ^ n
⊢ (a + b) / (ulp n a * 2) * 2 * ulp n a = 2 ^ Nat.size a
Theorem: round_le_of_no_uflow_of_carry_of_lt_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
pow_size_eq_pow_mul_ulp : 2 ^ Nat.size a = 2 ^ n * ulp n a
div_ulp_eq_pow : (a + b) / ulp n a = 2 ^ n
⊢ (a + b) / (ulp n a * 2) * 2 * ulp n a = 2 ^ Nat.size a
Tactic:
rewrite [← Nat.div_div_eq_div_mul]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
pow_size_eq_pow_mul_ulp : 2 ^ Nat.size a = 2 ^ n * ulp n a
div_ulp_eq_pow : (a + b) / ulp n a = 2 ^ n
⊢ (a + b) / ulp n a / 2 * 2 * ulp n a = 2 ^ Nat.size a
Theorem: round_le_of_no_uflow_of_carry_of_lt_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
pow_size_eq_pow_mul_ulp : 2 ^ Nat.size a = 2 ^ n * ulp n a
div_ulp_eq_pow : (a + b) / ulp n a = 2 ^ n
⊢ (a + b) / ulp n a / 2 * 2 * ulp n a = 2 ^ Nat.size a
Tactic:
rewrite [div_ulp_eq_pow]
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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
pow_size_eq_pow_mul_ulp : 2 ^ Nat.size a = 2 ^ n * ulp n a
div_ulp_eq_pow : (a + b) / ulp n a = 2 ^ n
⊢ 2 ^ n / 2 * 2 * ulp n a = 2 ^ Nat.size a
Theorem: round_le_of_no_uflow_of_carry_of_lt_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
pow_size_eq_pow_mul_ulp : 2 ^ Nat.size a = 2 ^ n * ulp n a
div_ulp_eq_pow : (a + b) / ulp n a = 2 ^ n
⊢ 2 ^ n / 2 * 2 * ulp n a = 2 ^ Nat.size a
Tactic:
rewrite [Nat.div_mul_cancel $ dvd_pow_self _ (Nat.not_eq_zero_of_lt npos)]
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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
pow_size_eq_pow_mul_ulp : 2 ^ Nat.size a = 2 ^ n * ulp n a
div_ulp_eq_pow : (a + b) / ulp n a = 2 ^ n
⊢ 2 ^ n * ulp n a = 2 ^ Nat.size a
Theorem: round_le_of_no_uflow_of_carry_of_lt_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
pow_size_eq_pow_mul_ulp : 2 ^ Nat.size a = 2 ^ n * ulp n a
div_ulp_eq_pow : (a + b) / ulp n a = 2 ^ n
⊢ 2 ^ n * ulp n a = 2 ^ Nat.size a
Tactic:
exact pow_size_eq_pow_mul_ulp.symm
Proof state after:
no goals
Theorem: round_le_of_no_uflow_of_carry_of_lt_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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
⊢ 2 ^ Nat.size a = 2 ^ n * ulp n a
Tactic:
unfold ulp expt
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
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
⊢ 2 ^ Nat.size a = 2 ^ n * 2 ^ (Nat.size a - n)