Theorem: ulp_le_ulp_of_le_ulp_of_size_lt (Fl.lean)

State before:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ ulp n a ≤ ulp n (a - b)
Tactic:
unfold ulp expt
State after:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - n) ≤ 2 ^ (Nat.size (a - b) - n)

State before:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - n) ≤ 2 ^ (Nat.size (a - b) - n)
Tactic:
apply Nat.pow_le_pow_of_le_right two_pos
State after:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ Nat.size a - n ≤ Nat.size (a - b) - n

State before:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ Nat.size a - n ≤ Nat.size (a - b) - n
Tactic:
apply tsub_le_tsub_right
State after:
case h
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ Nat.size a ≤ Nat.size (a - b)

State before:
case h
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ Nat.size a ≤ Nat.size (a - b)
Tactic:
apply Nat.le_of_pred_lt
State after:
case h.a
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ Nat.pred (Nat.size a) < Nat.size (a - b)

State before:
case h.a
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ Nat.pred (Nat.size a) < Nat.size (a - b)
Tactic:
rewrite [← Nat.sub_one]
State after:
case h.a
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ Nat.size a - 1 < Nat.size (a - b)

State before:
case h.a
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ Nat.size a - 1 < Nat.size (a - b)
Tactic:
rewrite [Nat.lt_size]
State after:
case h.a
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) ≤ a - b

State before:
case h.a
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) ≤ a - b
Tactic:
trans 2 ^ (Nat.size a - 1) + (ulp n a - b)
State after:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) ≤ 2 ^ (Nat.size a - 1) + (ulp n a - b)

n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) + (ulp n a - b) ≤ a - b

State before:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) ≤ 2 ^ (Nat.size a - 1) + (ulp n a - b)

n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) + (ulp n a - b) ≤ a - b
Tactic:
. exact Nat.le_add_right _ _
State after:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) + (ulp n a - b) ≤ a - b

State before:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) + (ulp n a - b) ≤ a - b
Tactic:
. rewrite [← add_tsub_assoc_of_le le_ulp]
  apply tsub_le_tsub_right
  apply add_le_of_dvd_of_dvd_of_lt
  . exact ulp_dvd_of_trunc_eq hfa
  . unfold ulp expt
    rewrite [Nat.pow_dvd_pow_iff_le_right one_lt_two]
    apply tsub_le_tsub_left
    exact Nat.one_le_of_lt npos
  . exact size_lt
State after:
no goals

State before:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) ≤ 2 ^ (Nat.size a - 1) + (ulp n a - b)
Tactic:
exact Nat.le_add_right _ _
State after:
no goals

State before:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) + (ulp n a - b) ≤ a - b
Tactic:
rewrite [← add_tsub_assoc_of_le le_ulp]
State after:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) + ulp n a - b ≤ a - b

State before:
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) + ulp n a - b ≤ a - b
Tactic:
apply tsub_le_tsub_right
State after:
case h
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) + ulp n a ≤ a

State before:
case h
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) + ulp n a ≤ a
Tactic:
apply add_le_of_dvd_of_dvd_of_lt
State after:
case h.h₁
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ ulp n a ∣ a

case h.h₂
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ ulp n a ∣ 2 ^ (Nat.size a - 1)

case h.h₃
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) < a

State before:
case h.h₁
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ ulp n a ∣ a

case h.h₂
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ ulp n a ∣ 2 ^ (Nat.size a - 1)

case h.h₃
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) < a
Tactic:
. exact ulp_dvd_of_trunc_eq hfa
State after:
case h.h₂
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ ulp n a ∣ 2 ^ (Nat.size a - 1)

case h.h₃
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) < a

State before:
case h.h₂
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ ulp n a ∣ 2 ^ (Nat.size a - 1)

case h.h₃
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) < a
Tactic:
. unfold ulp expt
  rewrite [Nat.pow_dvd_pow_iff_le_right one_lt_two]
  apply tsub_le_tsub_left
  exact Nat.one_le_of_lt npos
State after:
case h.h₃
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) < a

State before:
case h.h₃
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) < a
Tactic:
. exact size_lt
State after:
no goals

State before:
case h.h₁
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ ulp n a ∣ a
Tactic:
exact ulp_dvd_of_trunc_eq hfa
State after:
no goals

State before:
case h.h₂
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ ulp n a ∣ 2 ^ (Nat.size a - 1)
Tactic:
unfold ulp expt
State after:
case h.h₂
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - n) ∣ 2 ^ (Nat.size a - 1)

State before:
case h.h₂
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - n) ∣ 2 ^ (Nat.size a - 1)
Tactic:
rewrite [Nat.pow_dvd_pow_iff_le_right one_lt_two]
State after:
case h.h₂
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ Nat.size a - n ≤ Nat.size a - 1

State before:
case h.h₂
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ Nat.size a - n ≤ Nat.size a - 1
Tactic:
apply tsub_le_tsub_left
State after:
case h.h₂.h
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 1 ≤ n

State before:
case h.h₂.h
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 1 ≤ n
Tactic:
exact Nat.one_le_of_lt npos
State after:
no goals

State before:
case h.h₃
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) < a
Tactic:
exact size_lt
State after:
no goals