internlm/Lean-Github huggingface dataset:
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ a ≤ trunc n a
Tactic:
exact hfa.ge
Proof state after:
no goals
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ trunc n a ≤ trunc n (a + b)
Tactic:
apply trunc_le_trunc npos
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ a ≤ a + b
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ a ≤ a + b
Tactic:
exact Nat.le_add_right _ _
Proof state after:
no goals
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ trunc n (a + b) + ulp n (a + b) / 2 ≤ a + b
Tactic:
apply midpoint_le_of_round_eq_next_trunc npos hcorrect₁
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ round (a + b) = next n (trunc n (a + b))
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
d : ℕ
hd : ulp n (a + b) = 2 * d
⊢ round (a + b) = next n (trunc n (a + b))
Tactic:
exact round_eq_next_trunc_of_gt hfaithful₁ lt_round
Proof state after:
no goals
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
case inl
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
ulp_le : ulp n a ≤ 2 * b
lt_ulp' : b < ulp n a
⊢ ulp n a - b % ulp n a ≤ b
Tactic:
rewrite [tsub_le_iff_right, Nat.mod_eq_of_lt lt_ulp', ← Nat.two_mul]
Proof state after:
case inl
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
ulp_le : ulp n a ≤ 2 * b
lt_ulp' : b < ulp n a
⊢ ulp n a ≤ 2 * b
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
case inl
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
ulp_le : ulp n a ≤ 2 * b
lt_ulp' : b < ulp n a
⊢ ulp n a ≤ 2 * b
Tactic:
exact ulp_le
Proof state after:
no goals
Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
case inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
ulp_le : ulp n a ≤ 2 * b
ulp_le' : b ≥ ulp n a
⊢ ulp n a - b % ulp n a ≤ b
Tactic:
exact Nat.le_trans tsub_le_self ulp_le'
Proof state after:
no goals
Theorem: a₁_hi_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
n a b : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
⊢ trunc n (round (a + b) - (a + b)) = round (a + b) - (a + b)
Tactic:
apply a₁_hi_of_lt_round_of_ulp_sub_le npos hfaithful₁ hfa hfb hba lt_round
Proof state after:
n a b : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
⊢ ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
Theorem: a₁_hi_of_no_uflow_of_no_carry_of_lt_round
Proof state before:
n a b : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
⊢ ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
Tactic:
exact ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round npos hfaithful₁ hcorrect₁
  hfa no_uflow no_carry lt_round
Proof state after:
no goals
Theorem: a₁_hi_of_ulp_le_of_lt_round
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
ulp_le : ulp n (a + b) ≤ b
lt_round : a + b < round (a + b)
⊢ trunc n (round (a + b) - (a + b)) = round (a + b) - (a + b)
Tactic:
apply a₁_hi_of_lt_round_of_ulp_sub_le npos hfaithful₁ hfa hfb hba lt_round
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
ulp_le : ulp n (a + b) ≤ b
lt_round : a + b < round (a + b)
⊢ ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
Theorem: a₁_hi_of_ulp_le_of_lt_round
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
ulp_le : ulp n (a + b) ≤ b
lt_round : a + b < round (a + b)
⊢ ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
Tactic:
exact Nat.le_trans tsub_le_self ulp_le
Proof state after:
no goals
Theorem: a₁_lo_of_no_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_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Tactic:
have size_eq : Nat.size (a + b) = Nat.size a := by
  apply Nat.le_antisymm
  . exact Nat.size_le.mpr no_carry
  . exact Nat.size_le_size (Nat.le_add_right _ _)
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
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
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Theorem: a₁_lo_of_no_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_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Tactic:
have ulp_eq : ulp n (a + b) = ulp n a := by
  unfold ulp expt
  rw [size_eq]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
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
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Theorem: a₁_lo_of_no_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_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
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Tactic:
have mod_ulp₁ : a % ulp n a = 0 := by
  apply Nat.mod_eq_zero_of_dvd
  exact 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_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
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Theorem: a₁_lo_of_no_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_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
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Tactic:
have mod_ulp₂ : (a + b) % ulp n a = b % ulp n a := by
  rw [Nat.add_mod, mod_ulp₁, Nat.zero_add, Nat.mod_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_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
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Theorem: a₁_lo_of_no_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_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
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Tactic:
have error_eq : a + b - trunc n (a + b) = b % ulp n a := by
  rewrite [tsub_eq_iff_eq_add_of_le (trunc_le _ _), Nat.add_comm (b % ulp n a)]
  rewrite [← mod_ulp₂, ← ulp_eq]
  unfold trunc
  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_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
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Theorem: a₁_lo_of_no_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_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
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Tactic:
rewrite [round_eq_trunc_of_le npos hfaithful₁ round_le, error_eq]
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_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
⊢ trunc n (b % ulp n a) = b % ulp n a
Theorem: a₁_lo_of_no_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_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
⊢ trunc n (b % ulp n a) = 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_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

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
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

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:
. exact Nat.mod_le _ _
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 % ulp n a
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)]
  exact ulp_dvd_of_trunc_eq hfb
Proof state after:
no goals
Theorem: a₁_lo_of_no_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_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
⊢ Nat.size (a + b) = Nat.size a
Tactic:
apply Nat.le_antisymm
Proof state after:
case h₁
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
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
⊢ Nat.size (a + b) ≤ Nat.size a

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_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
⊢ Nat.size a ≤ Nat.size (a + b)
Theorem: a₁_lo_of_no_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_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
⊢ Nat.size (a + b) ≤ Nat.size a

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_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
⊢ Nat.size a ≤ Nat.size (a + b)
Tactic:
. exact Nat.size_le.mpr no_carry
Proof state after:
case h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
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
⊢ Nat.size a ≤ Nat.size (a + b)
Theorem: a₁_lo_of_no_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_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
⊢ Nat.size a ≤ Nat.size (a + b)
Tactic:
. exact Nat.size_le_size (Nat.le_add_right _ _)
Proof state after:
no goals
Theorem: a₁_lo_of_no_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_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
⊢ Nat.size (a + b) ≤ Nat.size a
Tactic:
exact Nat.size_le.mpr no_carry
Proof state after:
no goals
Theorem: a₁_lo_of_no_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_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
⊢ Nat.size a ≤ Nat.size (a + b)
Tactic:
exact Nat.size_le_size (Nat.le_add_right _ _)
Proof state after:
no goals
Theorem: a₁_lo_of_no_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_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
⊢ ulp n (a + b) = ulp n a
Tactic:
unfold ulp expt
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
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
⊢ 2 ^ (Nat.size (a + b) - n) = 2 ^ (Nat.size a - n)
Theorem: a₁_lo_of_no_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_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
⊢ 2 ^ (Nat.size (a + b) - n) = 2 ^ (Nat.size a - n)
Tactic:
rw [size_eq]
Proof state after:
no goals
Theorem: a₁_lo_of_no_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_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
⊢ a % ulp n a = 0
Tactic:
apply Nat.mod_eq_zero_of_dvd
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_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
⊢ ulp n a ∣ a
Theorem: a₁_lo_of_no_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_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
⊢ ulp n a ∣ a
Tactic:
exact ulp_dvd_of_trunc_eq hfa
Proof state after:
no goals
Theorem: a₁_lo_of_no_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_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
⊢ (a + b) % ulp n a = b % ulp n a
Tactic:
rw [Nat.add_mod, mod_ulp₁, Nat.zero_add, Nat.mod_mod]
Proof state after:
no goals
Theorem: a₁_lo_of_no_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_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
⊢ a + b - trunc n (a + b) = b % ulp n a
Tactic:
rewrite [tsub_eq_iff_eq_add_of_le (trunc_le _ _), Nat.add_comm (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_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
⊢ a + b = trunc n (a + b) + b % ulp n a
Theorem: a₁_lo_of_no_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_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
⊢ a + b = trunc n (a + b) + b % ulp n a
Tactic:
rewrite [← mod_ulp₂, ← ulp_eq]
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_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
⊢ a + b = trunc n (a + b) + (a + b) % ulp n (a + b)
Theorem: a₁_lo_of_no_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_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
⊢ a + b = trunc n (a + b) + (a + b) % ulp n (a + b)
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_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
⊢ a + b = (a + b) / ulp n (a + b) * ulp n (a + b) + (a + b) % ulp n (a + b)
Theorem: a₁_lo_of_no_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_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
⊢ a + b = (a + b) / ulp n (a + b) * ulp n (a + b) + (a + b) % ulp n (a + b)
Tactic:
rw [Nat.div_add_mod']
Proof state after:
no goals