Theorem: ulp_sub_le_of_no_uflow_of_no_carry_of_lt_round (Fl.lean)

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)
⊢ ulp n (a + b) - (a + b) % ulp n (a + b) ≤ 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 _ _)
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 n (a + b) - (a + b) % ulp n (a + b) ≤ b

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 n (a + b) - (a + b) % ulp n (a + b) ≤ b
Tactic:
have ulp_eq : ulp n (a + b) = ulp n a := by
  unfold ulp expt
  rw [size_eq]
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
⊢ ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b

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
⊢ ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
Tactic:
have ulp_le : ulp n a ≤ 2 * b := by
  have ⟨d, hd⟩ := two_dvd_ulp_of_no_uflow no_uflow
  rewrite [← ulp_eq, hd]
  apply Nat.mul_le_mul_left
  apply Nat.le_of_add_le_add_left (a := a)
  trans trunc n (a + b) + ulp n (a + b) / 2
  . rewrite [hd, Nat.mul_div_cancel_left _ two_pos]
    apply Nat.add_le_add_right
    trans trunc n a
    . exact hfa.ge
    . apply trunc_le_trunc npos
      exact Nat.le_add_right _ _
  . apply midpoint_le_of_round_eq_next_trunc npos hcorrect₁
    exact round_eq_next_trunc_of_gt hfaithful₁ lt_round
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
ulp_le : ulp n a ≤ 2 * b
⊢ ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b

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
ulp_le : ulp n a ≤ 2 * b
⊢ ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
Tactic:
rewrite [ulp_eq, ← Nat.mod_add_mod,
    Nat.mod_eq_zero_of_dvd (ulp_dvd_of_trunc_eq hfa), Nat.zero_add]
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
ulp_le : ulp n a ≤ 2 * b
⊢ ulp n a - b % ulp n a ≤ b

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
ulp_le : ulp n a ≤ 2 * b
⊢ ulp n a - b % ulp n a ≤ b
Tactic:
cases Nat.lt_or_ge b (ulp n a) with
| inl lt_ulp' =>
  rewrite [tsub_le_iff_right, Nat.mod_eq_of_lt lt_ulp', ← Nat.two_mul]
  exact ulp_le
| inr ulp_le' => exact Nat.le_trans tsub_le_self ulp_le'
State after:
no goals

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)
⊢ Nat.size (a + b) = Nat.size a
Tactic:
apply Nat.le_antisymm
State after:
case h₁
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)
⊢ Nat.size (a + b) ≤ Nat.size a

case h₂
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)
⊢ Nat.size a ≤ Nat.size (a + b)

State before:
case h₁
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)
⊢ Nat.size (a + b) ≤ Nat.size a

case h₂
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)
⊢ Nat.size a ≤ Nat.size (a + b)
Tactic:
. exact Nat.size_le.mpr no_carry
State after:
case h₂
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)
⊢ Nat.size a ≤ Nat.size (a + b)

State before:
case h₂
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)
⊢ Nat.size a ≤ Nat.size (a + b)
Tactic:
. exact Nat.size_le_size (Nat.le_add_right _ _)
State after:
no goals

State before:
case h₁
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)
⊢ Nat.size (a + b) ≤ Nat.size a
Tactic:
exact Nat.size_le.mpr no_carry
State after:
no goals

State before:
case h₂
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)
⊢ Nat.size a ≤ Nat.size (a + b)
Tactic:
exact Nat.size_le_size (Nat.le_add_right _ _)
State after:
no goals

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 n (a + b) = ulp n a
Tactic:
unfold ulp expt
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
⊢ 2 ^ (Nat.size (a + b) - n) = 2 ^ (Nat.size a - n)

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
⊢ 2 ^ (Nat.size (a + b) - n) = 2 ^ (Nat.size a - n)
Tactic:
rw [size_eq]
State after:
no goals

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
⊢ ulp n a ≤ 2 * b
Tactic:
have ⟨d, hd⟩ := two_dvd_ulp_of_no_uflow no_uflow
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
⊢ ulp n a ≤ 2 * b

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
⊢ ulp n a ≤ 2 * b
Tactic:
rewrite [← ulp_eq, hd]
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
⊢ 2 * d ≤ 2 * b

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
⊢ 2 * d ≤ 2 * b
Tactic:
apply Nat.mul_le_mul_left
State after:
case h
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
⊢ d ≤ b

State before:
case h
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
⊢ d ≤ b
Tactic:
apply Nat.le_of_add_le_add_left (a := a)
State after:
case h
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 + d ≤ a + b

State before:
case h
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 + d ≤ a + b
Tactic:
trans trunc n (a + b) + ulp n (a + b) / 2
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 + d ≤ trunc n (a + b) + ulp n (a + b) / 2

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

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 + d ≤ trunc n (a + b) + ulp n (a + b) / 2

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:
. rewrite [hd, Nat.mul_div_cancel_left _ two_pos]
  apply Nat.add_le_add_right
  trans trunc n a
  . exact hfa.ge
  . apply trunc_le_trunc npos
    exact Nat.le_add_right _ _
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
⊢ trunc n (a + b) + ulp n (a + b) / 2 ≤ a + b

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₁
  exact round_eq_next_trunc_of_gt hfaithful₁ lt_round
State after:
no goals

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 + d ≤ trunc n (a + b) + ulp n (a + b) / 2
Tactic:
rewrite [hd, Nat.mul_div_cancel_left _ two_pos]
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 + d ≤ trunc n (a + b) + d

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 + d ≤ trunc n (a + b) + d
Tactic:
apply Nat.add_le_add_right
State after:
case h
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 + b)

State before:
case h
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 + b)
Tactic:
trans trunc n a
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 ≤ trunc n a

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)

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

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:
. exact hfa.ge
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
⊢ trunc n a ≤ trunc n (a + b)

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
  exact Nat.le_add_right _ _
State after:
no goals

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
State after:
no goals

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

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 _ _
State after:
no goals

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

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
State after:
no goals

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

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
State after:
no goals

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'
State after:
no goals