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
⊢ b % ulp n a = (a % ulp n a + b) % ulp n a
Tactic:
rewrite [Nat.mod_eq_zero_of_dvd (ulp_dvd_of_trunc_eq 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 : ulp n a ≤ b
⊢ b % ulp n a = (0 + 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
⊢ b % ulp n a = (0 + b) % ulp n a
Tactic:
rw [Nat.zero_add]
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)
⊢ a + b - trunc n (a + b) = (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
Tactic:
unfold trunc
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)
⊢ a + b - (a + b) / ulp n (a + b) * ulp n (a + 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:
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)
⊢ a + b - (a + b) / ulp n (a + b) * ulp n (a + b) = (a + b) / ulp n a * ulp n a % ulp n (a + b) + b % ulp n a
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)
⊢ a + b - (a + b) / ulp n (a + b) * ulp n (a + b) = (a + b) / ulp n a * ulp n a % ulp n (a + b) + (a + 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)
⊢ a + b - (a + b) / ulp n (a + b) * ulp n (a + b) = (a + b) / ulp n a * ulp n a % ulp n (a + b) + (a + b) % ulp n a
Tactic:
rewrite [mod_eq_sub_div_mul]
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)
⊢ a + b - (a + b) / ulp n (a + b) * ulp n (a + b) =
    (a + b) / ulp n a * ulp n a - (a + b) / ulp n a * ulp n a / ulp n (a + b) * ulp n (a + b) + (a + 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)
⊢ a + b - (a + b) / ulp n (a + b) * ulp n (a + b) =
    (a + b) / ulp n a * ulp n a - (a + b) / ulp n a * ulp n a / ulp n (a + b) * ulp n (a + b) + (a + b) % ulp n a
Tactic:
rewrite [tsub_add_eq_add_tsub (Nat.div_mul_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 : ulp n a ≤ b
h₀ : b % ulp n a = (a + b) % ulp n a
h₁ : ulp n a ∣ ulp n (a + b)
⊢ a + b - (a + b) / ulp n (a + b) * ulp n (a + b) =
    (a + b) / ulp n a * ulp n a + (a + b) % ulp n a - (a + b) / ulp n a * ulp n a / ulp n (a + b) * 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)
⊢ a + b - (a + b) / ulp n (a + b) * ulp n (a + b) =
    (a + b) / ulp n a * ulp n a + (a + b) % ulp n a - (a + b) / ulp n a * ulp n a / ulp n (a + b) * ulp n (a + b)
Tactic:
rewrite [div_mul_div_cancel_of_dvd 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)
⊢ a + b - (a + b) / ulp n (a + b) * ulp n (a + b) =
    (a + b) / ulp n a * ulp n a + (a + b) % ulp n a - (a + b) / ulp n (a + b) * 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)
⊢ a + b - (a + b) / ulp n (a + b) * ulp n (a + b) =
    (a + b) / ulp n a * ulp n a + (a + b) % ulp n a - (a + b) / ulp n (a + b) * ulp n (a + b)
Tactic:
rw [Nat.div_add_mod' _ _]
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
⊢ (a + b) / ulp n a * ulp n a % ulp n (a + b) ≤ b / ulp n a * ulp n a
Tactic:
trans ulp n (a + b) - 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
⊢ (a + b) / ulp n a * ulp n a % ulp n (a + b) ≤ ulp n (a + 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
⊢ ulp n (a + b) - 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
⊢ (a + b) / ulp n a * ulp n a % ulp n (a + b) ≤ ulp n (a + 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
⊢ ulp n (a + b) - ulp n a ≤ b / ulp n a * ulp n a
Tactic:
. 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 _)
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
⊢ ulp n (a + b) - 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
⊢ ulp n (a + b) - ulp n a ≤ b / ulp n a * ulp n a
Tactic:
. 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:
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
⊢ (a + b) / ulp n a * ulp n a % ulp n (a + b) ≤ ulp n (a + b) - ulp n a
Tactic:
apply le_sub_of_dvd_of_dvd_of_lt
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 ∣ (a + b) / ulp n a * ulp n a % ulp n (a + b)

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 ∣ ulp n (a + b)

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
⊢ (a + b) / ulp n a * ulp n a % ulp n (a + b) < 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 ∣ (a + b) / ulp n a * ulp n a % ulp n (a + b)

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 ∣ ulp n (a + b)

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
⊢ (a + b) / ulp n a * ulp n a % ulp n (a + b) < ulp n (a + b)
Tactic:
. rewrite [Nat.dvd_mod_iff h₁]
  exact Nat.dvd_mul_left _ _
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 ∣ ulp n (a + b)

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
⊢ (a + b) / ulp n a * ulp n a % ulp n (a + b) < 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 ∣ ulp n (a + b)

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
⊢ (a + b) / ulp n a * ulp n a % ulp n (a + b) < ulp n (a + b)
Tactic:
. exact h₁
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
⊢ (a + b) / ulp n a * ulp n a % ulp n (a + b) < 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
⊢ (a + b) / ulp n a * ulp n a % ulp n (a + b) < ulp n (a + b)
Tactic:
. exact Nat.mod_lt _ (ulp_pos n _)
Proof state after:
no goals
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 ∣ (a + b) / ulp n a * ulp n a % ulp n (a + b)
Tactic:
rewrite [Nat.dvd_mod_iff h₁]
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 ∣ (a + b) / ulp n a * 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
⊢ 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 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 ∣ ulp n (a + b)
Tactic:
exact h₁
Proof state after:
no goals
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
⊢ (a + b) / ulp n a * ulp n a % ulp n (a + b) < ulp n (a + b)
Tactic:
exact Nat.mod_lt _ (ulp_pos n _)
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
⊢ ulp n (a + b) - ulp n a ≤ b / ulp n a * ulp n a
Tactic:
rewrite [ulp_add_eq_two_mul_ulp]
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
⊢ 2 * ulp n a - 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
⊢ 2 * ulp n a - ulp n a ≤ b / ulp n a * ulp n a
Tactic:
rewrite [← Nat.mul_pred_left]
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
⊢ Nat.pred 2 * ulp n a ≤ b / ulp n a * ulp n a