Theorem: le_midpoint_of_round_eq_trunc (Fl/Round.lean)

State before:
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
⊢ x ≤ trunc n x + ulp n x / 2
Tactic:
cases Nat.lt_or_ge x (2 ^ n) with
| inl uflow =>
  exact ge_of_eq (trunc_add_half_ulp_eq_of_uflow uflow)
| inr no_uflow =>
  refine Nat.le_of_mul_le_mul_left ?_ two_pos
  rewrite [trunc_add_half_ulp_eq_of_no_uflow npos no_uflow]
  have h1 : x ≤ next n (trunc n x) := Nat.le_of_lt (lt_next_trunc npos x)
  have h2 : trunc n x ≤ x := trunc_le n x
  rewrite [Nat.two_mul, ← tsub_le_iff_left, add_tsub_assoc_of_le h2,
      Nat.add_comm, ← le_tsub_iff_right h1]
  exact hcorrect₀ x hlo
State after:
no goals

State before:
case inl
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
uflow : x < 2 ^ n
⊢ x ≤ trunc n x + ulp n x / 2
Tactic:
exact ge_of_eq (trunc_add_half_ulp_eq_of_uflow uflow)
State after:
no goals

State before:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
⊢ x ≤ trunc n x + ulp n x / 2
Tactic:
refine Nat.le_of_mul_le_mul_left ?_ two_pos
State after:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
⊢ 2 * x ≤ 2 * (trunc n x + ulp n x / 2)

State before:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
⊢ 2 * x ≤ 2 * (trunc n x + ulp n x / 2)
Tactic:
rewrite [trunc_add_half_ulp_eq_of_no_uflow npos no_uflow]
State after:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
⊢ 2 * x ≤ trunc n x + next n (trunc n x)

State before:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
⊢ 2 * x ≤ trunc n x + next n (trunc n x)
Tactic:
have h1 : x ≤ next n (trunc n x) := Nat.le_of_lt (lt_next_trunc npos x)
State after:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
⊢ 2 * x ≤ trunc n x + next n (trunc n x)

State before:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
⊢ 2 * x ≤ trunc n x + next n (trunc n x)
Tactic:
have h2 : trunc n x ≤ x := trunc_le n x
State after:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
h2 : trunc n x ≤ x
⊢ 2 * x ≤ trunc n x + next n (trunc n x)

State before:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
h2 : trunc n x ≤ x
⊢ 2 * x ≤ trunc n x + next n (trunc n x)
Tactic:
rewrite [Nat.two_mul, ← tsub_le_iff_left, add_tsub_assoc_of_le h2,
    Nat.add_comm, ← le_tsub_iff_right h1]
State after:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
h2 : trunc n x ≤ x
⊢ x - trunc n x ≤ next n (trunc n x) - x

State before:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
h2 : trunc n x ≤ x
⊢ x - trunc n x ≤ next n (trunc n x) - x
Tactic:
exact hcorrect₀ x hlo
State after:
no goals