Theorem: round_eq_trunc_of_lt_midpoint (Fl/Round.lean)

State before:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
⊢ round x = trunc n x
Tactic:
cases lt_or_ge n (Nat.size x) with
| inr uflow =>
  have trunc_eq : trunc n x = x := by
    unfold trunc ulp expt
    rewrite [tsub_eq_zero_of_le uflow]
    rw [Nat.pow_zero, Nat.mul_one, Nat.div_one]
  rw [round_eq_of_trunc_eq npos hfaithful₀ trunc_eq, trunc_eq]
| inl no_uflow =>
  have expt_pos : 0 < (Nat.size x) - n := lt_tsub_of_add_lt_left no_uflow
  have ulp_even : 2 ∣ ulp n x := dvd_pow_self _ (ne_zero_of_lt expt_pos)
  have h : x - trunc n x < next n (trunc n x) - x := by
    rewrite [tsub_lt_iff_left (trunc_le n x)]
    rewrite [← add_tsub_assoc_of_le (le_of_lt (lt_next_trunc npos x))]
    unfold next
    rewrite [ulp_trunc npos]
    rewrite [lt_tsub_iff_left]
    rewrite [← Nat.add_assoc]
    rewrite [← Nat.div_mul_cancel ulp_even]
    rewrite [← mul_two, ← mul_two, ← add_mul]
    exact Nat.mul_lt_mul_of_pos_right h two_pos
  cases hfaithful₁ x with
  | inl lo => exact lo
  | inr hi => exfalso ; exact Nat.lt_le_asymm h $ hcorrect₁ x hi
State after:
no goals

State before:
case inr
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
uflow : n ≥ Nat.size x
⊢ round x = trunc n x
Tactic:
have trunc_eq : trunc n x = x := by
  unfold trunc ulp expt
  rewrite [tsub_eq_zero_of_le uflow]
  rw [Nat.pow_zero, Nat.mul_one, Nat.div_one]
State after:
case inr
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
uflow : n ≥ Nat.size x
trunc_eq : trunc n x = x
⊢ round x = trunc n x

State before:
case inr
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
uflow : n ≥ Nat.size x
trunc_eq : trunc n x = x
⊢ round x = trunc n x
Tactic:
rw [round_eq_of_trunc_eq npos hfaithful₀ trunc_eq, trunc_eq]
State after:
no goals

State before:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
uflow : n ≥ Nat.size x
⊢ trunc n x = x
Tactic:
unfold trunc ulp expt
State after:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
uflow : n ≥ Nat.size x
⊢ x / 2 ^ (Nat.size x - n) * 2 ^ (Nat.size x - n) = x

State before:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
uflow : n ≥ Nat.size x
⊢ x / 2 ^ (Nat.size x - n) * 2 ^ (Nat.size x - n) = x
Tactic:
rewrite [tsub_eq_zero_of_le uflow]
State after:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
uflow : n ≥ Nat.size x
⊢ x / 2 ^ 0 * 2 ^ 0 = x

State before:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
uflow : n ≥ Nat.size x
⊢ x / 2 ^ 0 * 2 ^ 0 = x
Tactic:
rw [Nat.pow_zero, Nat.mul_one, Nat.div_one]
State after:
no goals

State before:
case inl
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
⊢ round x = trunc n x
Tactic:
have expt_pos : 0 < (Nat.size x) - n := lt_tsub_of_add_lt_left no_uflow
State after:
case inl
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
⊢ round x = trunc n x

State before:
case inl
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
⊢ round x = trunc n x
Tactic:
have ulp_even : 2 ∣ ulp n x := dvd_pow_self _ (ne_zero_of_lt expt_pos)
State after:
case inl
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
⊢ round x = trunc n x

State before:
case inl
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
⊢ round x = trunc n x
Tactic:
have h : x - trunc n x < next n (trunc n x) - x := by
  rewrite [tsub_lt_iff_left (trunc_le n x)]
  rewrite [← add_tsub_assoc_of_le (le_of_lt (lt_next_trunc npos x))]
  unfold next
  rewrite [ulp_trunc npos]
  rewrite [lt_tsub_iff_left]
  rewrite [← Nat.add_assoc]
  rewrite [← Nat.div_mul_cancel ulp_even]
  rewrite [← mul_two, ← mul_two, ← add_mul]
  exact Nat.mul_lt_mul_of_pos_right h two_pos
State after:
case inl
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h✝ : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
h : x - trunc n x < next n (trunc n x) - x
⊢ round x = trunc n x

State before:
case inl
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h✝ : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
h : x - trunc n x < next n (trunc n x) - x
⊢ round x = trunc n x
Tactic:
cases hfaithful₁ x with
| inl lo => exact lo
| inr hi => exfalso ; exact Nat.lt_le_asymm h $ hcorrect₁ x hi
State after:
no goals

State before:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
⊢ x - trunc n x < next n (trunc n x) - x
Tactic:
rewrite [tsub_lt_iff_left (trunc_le n x)]
State after:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
⊢ x < trunc n x + (next n (trunc n x) - x)

State before:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
⊢ x < trunc n x + (next n (trunc n x) - x)
Tactic:
rewrite [← add_tsub_assoc_of_le (le_of_lt (lt_next_trunc npos x))]
State after:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
⊢ x < trunc n x + next n (trunc n x) - x

State before:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
⊢ x < trunc n x + next n (trunc n x) - x
Tactic:
unfold next
State after:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
⊢ x < trunc n x + (trunc n x + ulp n (trunc n x)) - x

State before:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
⊢ x < trunc n x + (trunc n x + ulp n (trunc n x)) - x
Tactic:
rewrite [ulp_trunc npos]
State after:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
⊢ x < trunc n x + (trunc n x + ulp n x) - x

State before:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
⊢ x < trunc n x + (trunc n x + ulp n x) - x
Tactic:
rewrite [lt_tsub_iff_left]
State after:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
⊢ x + x < trunc n x + (trunc n x + ulp n x)

State before:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
⊢ x + x < trunc n x + (trunc n x + ulp n x)
Tactic:
rewrite [← Nat.add_assoc]
State after:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
⊢ x + x < trunc n x + trunc n x + ulp n x

State before:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
⊢ x + x < trunc n x + trunc n x + ulp n x
Tactic:
rewrite [← Nat.div_mul_cancel ulp_even]
State after:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
⊢ x + x < trunc n x + trunc n x + ulp n x / 2 * 2

State before:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
⊢ x + x < trunc n x + trunc n x + ulp n x / 2 * 2
Tactic:
rewrite [← mul_two, ← mul_two, ← add_mul]
State after:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
⊢ x * 2 < (trunc n x + ulp n x / 2) * 2

State before:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
⊢ x * 2 < (trunc n x + ulp n x / 2) * 2
Tactic:
exact Nat.mul_lt_mul_of_pos_right h two_pos
State after:
no goals

State before:
case inl.inl
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h✝ : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
h : x - trunc n x < next n (trunc n x) - x
lo : round x = trunc n x
⊢ round x = trunc n x
Tactic:
exact lo
State after:
no goals

State before:
case inl.inr
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h✝ : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
h : x - trunc n x < next n (trunc n x) - x
hi : round x = next n (trunc n x)
⊢ round x = trunc n x
Tactic:
exfalso
State after:
case inl.inr.h
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h✝ : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
h : x - trunc n x < next n (trunc n x) - x
hi : round x = next n (trunc n x)
⊢ False

State before:
case inl.inr.h
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h✝ : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
h : x - trunc n x < next n (trunc n x) - x
hi : round x = next n (trunc n x)
⊢ False
Tactic:
exact Nat.lt_le_asymm h $ hcorrect₁ x hi
State after:
no goals