internlm/Lean-Github huggingface dataset:
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
⊢ Nat.pred 2 * ulp n a ≤ b / ulp n a * ulp n a
Tactic:
rewrite [← one_add_one_eq_two, Nat.add_one, Nat.pred_succ]
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
⊢ 1 * ulp n a ≤ b / ulp n 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 : 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
⊢ 1 * ulp n a ≤ b / ulp n a * ulp n a
Tactic:
apply Nat.mul_le_mul_right
Proof state after:
case 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
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
⊢ 1 ≤ b / ulp n a
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_le
Proof state before:
case 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
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
⊢ 1 ≤ b / ulp n a
Tactic:
rewrite [Nat.one_le_div_iff (ulp_pos n _)]
Proof state after:
case 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
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
⊢ ulp n a ≤ b
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_le
Proof state before:
case 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
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
⊢ ulp n a ≤ b
Tactic:
exact ulp_le
Proof state after:
no goals
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
Tactic:
conv => rhs; rewrite [← Nat.div_add_mod' b (ulp n a)]
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 / ulp n a * ulp n a + 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 / ulp n a * ulp n a + b % ulp n a
Tactic:
exact Nat.add_le_add_right h₃ (b % ulp n a)
Proof state after:
no goals
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
Proof state after:
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
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)

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
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 ∣ b % ulp n a
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
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)

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
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 ∣ b % ulp n a
Tactic:
. trans ulp n a
  . exact ulp_dvd_ulp n hba
  . rewrite [Nat.dvd_mod_iff h₁]
    exact Nat.dvd_mul_left _ _
Proof state after:
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
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 ∣ b % ulp n a
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
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 ∣ b % ulp n a
Tactic:
. 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:
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
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)
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
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 ∣ 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
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 a ∣ (a + b) / ulp n a * ulp n a % ulp 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
⊢ 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
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 a ∣ (a + b) / ulp n a * ulp n a % ulp n (a + b)
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
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 a ∣ (a + b) / ulp n a * ulp n a % ulp 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
⊢ ulp n a ∣ (a + b) / ulp n a * ulp n a % ulp n (a + b)
Tactic:
. rewrite [Nat.dvd_mod_iff h₁]
  exact Nat.dvd_mul_left _ _
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
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 ∣ ulp n a
Tactic:
exact ulp_dvd_ulp n hba
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
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 a ∣ (a + b) / ulp n a * ulp n a % ulp n (a + b)
Tactic:
rewrite [Nat.dvd_mod_iff 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
⊢ ulp n a ∣ (a + b) / ulp n 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 : 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 a ∣ (a + b) / ulp n a * ulp n a
Tactic:
exact Nat.dvd_mul_left _ _
Proof state after:
no goals
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
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 ∣ b % ulp n a
Tactic:
rewrite [Nat.dvd_mod_iff (ulp_dvd_ulp n hba)]
Proof state after:
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
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 ∣ b
Theorem: a₁_lo_of_no_uflow_of_carry_of_round_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
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 ∣ b
Tactic:
exact ulp_dvd_of_trunc_eq hfb
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)
⊢ round (a + b) ≤ a + b
Tactic:
have ⟨le_size, ulp_eq⟩ :=
  le_size_and_ulp_eq_of_no_uflow_of_carry hba no_uflow carry
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
⊢ round (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
⊢ round (a + b) ≤ a + b
Tactic:
have add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a := by
  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
  rewrite [← tsub_add_cancel_of_le ulp_le]
  rewrite [Nat.add_assoc]
  rewrite [← Nat.two_mul]
  rewrite [← ulp_eq]
  apply add_lt_add_of_le_of_lt
  . exact le_size_sub_ulp_of_trunc_eq npos hfa
  . exact lt_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
⊢ round (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
⊢ round (a + b) ≤ a + b
Tactic:
have eq_pow : trunc n (a + b) = 2 ^ Nat.size a := by
  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]
  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]
  unfold trunc
  rewrite [ulp_eq]
  rewrite [← Nat.mul_assoc]
  rewrite [Nat.mul_comm 2]
  rewrite [← Nat.div_div_eq_div_mul]
  rewrite [div_ulp_eq_pow]
  rewrite [Nat.div_mul_cancel $ dvd_pow_self _ (Nat.not_eq_zero_of_lt npos)]
  exact pow_size_eq_pow_mul_ulp.symm
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
⊢ round (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
⊢ round (a + b) ≤ a + b
Tactic:
have lt_midpoint : a + b < trunc n (a + b) + ulp n (a + b) / 2 := by
  rewrite [eq_pow]
  apply Nat.lt_of_lt_of_le add_lt_pow_add_ulp
  apply Nat.add_le_add_left
  rewrite [ulp_eq]
  rw [Nat.mul_div_cancel_left _ two_pos]
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
⊢ round (a + b) ≤ a + b