Theorem: midpoint_le_of_round_eq_next_trunc (Fl/Round.lean)

State before:
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₁ : correct₁ n round
hhi : round x = next n (trunc n x)
⊢ trunc n x + ulp n x / 2 ≤ x
Tactic:
cases Nat.lt_or_ge x (2 ^ n) with
| inl uflow =>
  exact le_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 h1,
           Nat.add_comm, ← le_tsub_iff_right h2]
  exact hcorrect₁ x hhi
State after:
no goals

State before:
case inl
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₁ : correct₁ n round
hhi : round x = next n (trunc n x)
uflow : x < 2 ^ n
⊢ trunc n x + ulp n x / 2 ≤ x
Tactic:
exact le_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
hhi : round x = next n (trunc n x)
no_uflow : x ≥ 2 ^ n
⊢ trunc n x + ulp n x / 2 ≤ x
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
hhi : round x = next n (trunc n x)
no_uflow : x ≥ 2 ^ n
⊢ 2 * (trunc n x + ulp n x / 2) ≤ 2 * x

State before:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₁ : correct₁ n round
hhi : round x = next n (trunc n x)
no_uflow : x ≥ 2 ^ n
⊢ 2 * (trunc n x + ulp n x / 2) ≤ 2 * x
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
hhi : round x = next n (trunc n x)
no_uflow : x ≥ 2 ^ n
⊢ trunc n x + next n (trunc n x) ≤ 2 * x

State before:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₁ : correct₁ n round
hhi : round x = next n (trunc n x)
no_uflow : x ≥ 2 ^ n
⊢ trunc n x + next n (trunc n x) ≤ 2 * 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
hhi : round x = next n (trunc n x)
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
⊢ trunc n x + next n (trunc n x) ≤ 2 * x

State before:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₁ : correct₁ n round
hhi : round x = next n (trunc n x)
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
⊢ trunc n x + next n (trunc n x) ≤ 2 * 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
hhi : round x = next n (trunc n x)
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
h2 : trunc n x ≤ x
⊢ trunc n x + next n (trunc n x) ≤ 2 * x

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

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