internlm/Lean-Github huggingface dataset:
Theorem: a₁_lo_of_no_carry_of_round_le
Proof state before:
case hle
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
error_eq : a + b - trunc n (a + b) = b % ulp n a
⊢ b % ulp n a ≤ b
Tactic:
exact Nat.mod_le _ _
Proof state after:
no goals
Theorem: a₁_lo_of_no_carry_of_round_le
Proof state before:
case hdvd
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
error_eq : a + b - trunc n (a + b) = b % ulp n a
⊢ ulp n b ∣ b % ulp n a
Tactic:
rewrite [Nat.dvd_mod_iff (ulp_dvd_ulp n hba)]
Proof state after:
case hdvd
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
error_eq : a + b - trunc n (a + b) = b % ulp n a
⊢ ulp n b ∣ b
Theorem: a₁_lo_of_no_carry_of_round_le
Proof state before:
case hdvd
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
error_eq : a + b - trunc n (a + b) = b % ulp n a
⊢ ulp n b ∣ b
Tactic:
exact ulp_dvd_of_trunc_eq hfb
Proof state after:
no goals
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Tactic:
have ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a :=
  (le_size_and_ulp_eq_of_no_uflow_of_carry hba no_uflow carry).right
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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Tactic:
have ulp_le : ulp n a ≤ b := by
  apply Nat.le_of_add_le_add_left (a := a)
  have ulp_le_pow : ulp n a ≤ 2 ^ Nat.size a := by
    unfold ulp expt
    exact Nat.pow_le_pow_of_le_right two_pos tsub_le_self
  trans 2 ^ Nat.size a
  . apply add_le_of_le_tsub_right_of_le ulp_le_pow
    exact le_size_sub_ulp_of_trunc_eq npos hfa
  . exact carry
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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Tactic:
have h₀ : b % ulp n a = (a + b) % ulp n a := by
  rewrite [← Nat.mod_add_mod]
  rewrite [Nat.mod_eq_zero_of_dvd (ulp_dvd_of_trunc_eq hfa)]
  rw [Nat.zero_add]
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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
h₀ : b % ulp n a = (a + b) % ulp n a
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
h₀ : b % ulp n a = (a + b) % ulp n a
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Tactic:
have h₁ : ulp n a ∣ ulp n (a + b) := ulp_dvd_ulp n $ Nat.le_add_right _ _
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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
h₀ : b % ulp n a = (a + b) % ulp n a
h₁ : ulp n a ∣ ulp n (a + b)
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
h₀ : b % ulp n a = (a + b) % ulp n a
h₁ : ulp n a ∣ ulp n (a + b)
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Tactic:
have h₂ : a + b - trunc n (a + b) =
            (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a := by
  unfold trunc
  rewrite [h₀]
  rewrite [mod_eq_sub_div_mul]
  rewrite [tsub_add_eq_add_tsub (Nat.div_mul_le_self _ _)]
  rewrite [div_mul_div_cancel_of_dvd h₁]
  rw [Nat.div_add_mod' _ _]
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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
h₀ : b % ulp n a = (a + b) % ulp n a
h₁ : ulp n a ∣ ulp n (a + b)
h₂ : a + b - trunc n (a + b) = (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
h₀ : b % ulp n a = (a + b) % ulp n a
h₁ : ulp n a ∣ ulp n (a + b)
h₂ : a + b - trunc n (a + b) = (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Tactic:
have h₃ : (a + b) / ulp n a * ulp n a % ulp n (a + b) ≤
            b / ulp n a * ulp n a := by
  trans ulp n (a + b) - ulp n a
  . apply le_sub_of_dvd_of_dvd_of_lt
    . rewrite [Nat.dvd_mod_iff h₁]
      exact Nat.dvd_mul_left _ _
    . exact h₁
    . exact Nat.mod_lt _ (ulp_pos n _)
  . rewrite [ulp_add_eq_two_mul_ulp]
    rewrite [← Nat.mul_pred_left]
    rewrite [← one_add_one_eq_two, Nat.add_one, Nat.pred_succ]
    apply Nat.mul_le_mul_right
    rewrite [Nat.one_le_div_iff (ulp_pos n _)]
    exact ulp_le
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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
h₀ : b % ulp n a = (a + b) % ulp n a
h₁ : ulp n a ∣ ulp n (a + b)
h₂ : a + b - trunc n (a + b) = (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
h₃ : (a + b) / ulp n a * ulp n a % ulp n (a + b) ≤ b / ulp n a * ulp n a
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
h₀ : b % ulp n a = (a + b) % ulp n a
h₁ : ulp n a ∣ ulp n (a + b)
h₂ : a + b - trunc n (a + b) = (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
h₃ : (a + b) / ulp n a * ulp n a % ulp n (a + b) ≤ b / ulp n a * ulp n a
⊢ trunc n (a + b - round (a + b)) = a + b - round (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
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
h₀ : b % ulp n a = (a + b) % ulp n a
h₁ : ulp n a ∣ ulp n (a + b)
h₂ : a + b - trunc n (a + b) = (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
h₃ : (a + b) / ulp n a * ulp n a % ulp n (a + b) ≤ b / ulp n a * ulp n a
⊢ trunc n (a + b - trunc n (a + b)) = a + b - trunc n (a + b)
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
h₀ : b % ulp n a = (a + b) % ulp n a
h₁ : ulp n a ∣ ulp n (a + b)
h₂ : a + b - trunc n (a + b) = (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
h₃ : (a + b) / ulp n a * ulp n a % ulp n (a + b) ≤ b / ulp n a * ulp n a
⊢ trunc n (a + b - trunc n (a + b)) = a + b - trunc n (a + b)
Tactic:
rewrite [h₂]
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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
h₀ : b % ulp n a = (a + b) % ulp n a
h₁ : ulp n a ∣ ulp n (a + b)
h₂ : a + b - trunc n (a + b) = (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
h₃ : (a + b) / ulp n a * ulp n a % ulp n (a + b) ≤ b / ulp n a * ulp n a
⊢ trunc n ((a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a) =
    (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
h₀ : b % ulp n a = (a + b) % ulp n a
h₁ : ulp n a ∣ ulp n (a + b)
h₂ : a + b - trunc n (a + b) = (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
h₃ : (a + b) / ulp n a * ulp n a % ulp n (a + b) ≤ b / ulp n a * ulp n a
⊢ trunc n ((a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a) =
    (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
Tactic:
apply trunc_eq_of_le_of_ulp_dvd b
Proof state after:
case hle
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
h₀ : b % ulp n a = (a + b) % ulp n a
h₁ : ulp n a ∣ ulp n (a + b)
h₂ : a + b - trunc n (a + b) = (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
h₃ : (a + b) / ulp n a * ulp n a % ulp n (a + b) ≤ b / ulp n a * ulp n a
⊢ (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a ≤ b

case hdvd
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
h₀ : b % ulp n a = (a + b) % ulp n a
h₁ : ulp n a ∣ ulp n (a + b)
h₂ : a + b - trunc n (a + b) = (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
h₃ : (a + b) / ulp n a * ulp n a % ulp n (a + b) ≤ b / ulp n a * ulp n a
⊢ ulp n b ∣ (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_le
Proof state before:
case hle
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
h₀ : b % ulp n a = (a + b) % ulp n a
h₁ : ulp n a ∣ ulp n (a + b)
h₂ : a + b - trunc n (a + b) = (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
h₃ : (a + b) / ulp n a * ulp n a % ulp n (a + b) ≤ b / ulp n a * ulp n a
⊢ (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a ≤ b

case hdvd
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
h₀ : b % ulp n a = (a + b) % ulp n a
h₁ : ulp n a ∣ ulp n (a + b)
h₂ : a + b - trunc n (a + b) = (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
h₃ : (a + b) / ulp n a * ulp n a % ulp n (a + b) ≤ b / ulp n a * ulp n a
⊢ ulp n b ∣ (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
Tactic:
. conv => rhs; rewrite [← Nat.div_add_mod' b (ulp n a)]
  exact Nat.add_le_add_right h₃ (b % ulp n a)
Proof state after:
case hdvd
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
h₀ : b % ulp n a = (a + b) % ulp n a
h₁ : ulp n a ∣ ulp n (a + b)
h₂ : a + b - trunc n (a + b) = (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
h₃ : (a + b) / ulp n a * ulp n a % ulp n (a + b) ≤ b / ulp n a * ulp n a
⊢ ulp n b ∣ (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_le
Proof state before:
case hdvd
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
h₀ : b % ulp n a = (a + b) % ulp n a
h₁ : ulp n a ∣ ulp n (a + b)
h₂ : a + b - trunc n (a + b) = (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
h₃ : (a + b) / ulp n a * ulp n a % ulp n (a + b) ≤ b / ulp n a * ulp n a
⊢ ulp n b ∣ (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
Tactic:
. apply Nat.dvd_add
  . trans ulp n a
    . exact ulp_dvd_ulp n hba
    . rewrite [Nat.dvd_mod_iff h₁]
      exact Nat.dvd_mul_left _ _
  . rewrite [Nat.dvd_mod_iff (ulp_dvd_ulp n hba)]
    exact ulp_dvd_of_trunc_eq hfb
Proof state after:
no goals
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
⊢ ulp n a ≤ b
Tactic:
apply Nat.le_of_add_le_add_left (a := 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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
⊢ a + ulp n a ≤ a + b
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
⊢ a + ulp n a ≤ a + b
Tactic:
have ulp_le_pow : 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
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le_pow : ulp n a ≤ 2 ^ Nat.size a
⊢ a + ulp n a ≤ a + b
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le_pow : ulp n a ≤ 2 ^ Nat.size a
⊢ a + ulp n a ≤ a + b
Tactic:
trans 2 ^ Nat.size 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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le_pow : ulp n a ≤ 2 ^ Nat.size a
⊢ a + ulp n a ≤ 2 ^ Nat.size 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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le_pow : ulp n a ≤ 2 ^ Nat.size a
⊢ 2 ^ Nat.size a ≤ a + b
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le_pow : ulp n a ≤ 2 ^ Nat.size a
⊢ a + ulp n a ≤ 2 ^ Nat.size 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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le_pow : ulp n a ≤ 2 ^ Nat.size a
⊢ 2 ^ Nat.size a ≤ a + b
Tactic:
. apply add_le_of_le_tsub_right_of_le ulp_le_pow
  exact le_size_sub_ulp_of_trunc_eq npos hfa
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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le_pow : ulp n a ≤ 2 ^ Nat.size a
⊢ 2 ^ Nat.size a ≤ a + b
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le_pow : ulp n a ≤ 2 ^ Nat.size a
⊢ 2 ^ Nat.size a ≤ a + b
Tactic:
. exact carry
Proof state after:
no goals
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : 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
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
⊢ 2 ^ (Nat.size a - n) ≤ 2 ^ Nat.size a
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : 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: a₁_lo_of_no_uflow_of_carry_of_round_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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le_pow : ulp n a ≤ 2 ^ Nat.size a
⊢ a + ulp n a ≤ 2 ^ Nat.size a
Tactic:
apply add_le_of_le_tsub_right_of_le ulp_le_pow
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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le_pow : ulp n a ≤ 2 ^ Nat.size a
⊢ a ≤ 2 ^ Nat.size a - ulp n a
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le_pow : 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: a₁_lo_of_no_uflow_of_carry_of_round_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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le_pow : ulp n a ≤ 2 ^ Nat.size a
⊢ 2 ^ Nat.size a ≤ a + b
Tactic:
exact carry
Proof state after:
no goals
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
⊢ b % ulp n a = (a + b) % ulp n a
Tactic:
rewrite [← Nat.mod_add_mod]
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
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
round_le : round (a + b) ≤ a + b
ulp_add_eq_two_mul_ulp : ulp n (a + b) = 2 * ulp n a
ulp_le : ulp n a ≤ b
⊢ b % ulp n a = (a % ulp n a + b) % ulp n a