Theorem: le_size_and_ulp_eq_of_no_uflow_of_carry (Fl/Trunc.lean)

State before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ n ≤ Nat.size a ∧ ulp n (a + b) = 2 * ulp n a
Tactic:
have size_eq : Nat.size (a + b) = Nat.size a + 1 := by
  apply Nat.le_antisymm
  . rewrite [Nat.size_le, pow_succ, Nat.two_mul]
    apply Nat.add_lt_add
    . exact Nat.lt_size_self _
    . exact Nat.lt_of_le_of_lt hba (Nat.lt_size_self _)
  . rewrite [Nat.succ_le, Nat.lt_size]
    exact carry
State after:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
⊢ n ≤ Nat.size a ∧ ulp n (a + b) = 2 * ulp n a

State before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
⊢ n ≤ Nat.size a ∧ ulp n (a + b) = 2 * ulp n a
Tactic:
have le_size : n ≤ Nat.size a := by
  rewrite [← Nat.lt_succ, Nat.succ_eq_add_one]
  calc
    n < Nat.size (a + b) := by rwa [Nat.lt_size]
    _ = Nat.size a + 1   := size_eq
State after:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
le_size : n ≤ Nat.size a
⊢ n ≤ Nat.size a ∧ ulp n (a + b) = 2 * ulp n a

State before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
le_size : n ≤ Nat.size a
⊢ n ≤ Nat.size a ∧ ulp n (a + b) = 2 * ulp n a
Tactic:
have ulp_eq : ulp n (a + b) = 2 * ulp n a := by
  calc
    ulp n (a + b)
      = 2 ^ (Nat.size (a + b) - n) := rfl
    _ = 2 ^ (Nat.size a + 1 - n)   := by rw [size_eq]
    _ = 2 ^ (Nat.size a - n + 1)   := by rw [← tsub_add_eq_add_tsub le_size]
    _ = 2 * 2 ^ (Nat.size a - n)   := by rw [pow_succ]
    _ = 2 * ulp n a                := rfl
State after:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
⊢ n ≤ Nat.size a ∧ ulp n (a + b) = 2 * ulp n a

State before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
⊢ n ≤ Nat.size a ∧ ulp n (a + b) = 2 * ulp n a
Tactic:
exact ⟨le_size, ulp_eq⟩
State after:
no goals

State before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ Nat.size (a + b) = Nat.size a + 1
Tactic:
apply Nat.le_antisymm
State after:
case h₁
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ Nat.size (a + b) ≤ Nat.size a + 1

case h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ Nat.size a + 1 ≤ Nat.size (a + b)

State before:
case h₁
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ Nat.size (a + b) ≤ Nat.size a + 1

case h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ Nat.size a + 1 ≤ Nat.size (a + b)
Tactic:
. rewrite [Nat.size_le, pow_succ, Nat.two_mul]
  apply Nat.add_lt_add
  . exact Nat.lt_size_self _
  . exact Nat.lt_of_le_of_lt hba (Nat.lt_size_self _)
State after:
case h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ Nat.size a + 1 ≤ Nat.size (a + b)

State before:
case h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ Nat.size a + 1 ≤ Nat.size (a + b)
Tactic:
. rewrite [Nat.succ_le, Nat.lt_size]
  exact carry
State after:
no goals

State before:
case h₁
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ Nat.size (a + b) ≤ Nat.size a + 1
Tactic:
rewrite [Nat.size_le, pow_succ, Nat.two_mul]
State after:
case h₁
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ a + b < 2 ^ Nat.size a + 2 ^ Nat.size a

State before:
case h₁
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ a + b < 2 ^ Nat.size a + 2 ^ Nat.size a
Tactic:
apply Nat.add_lt_add
State after:
case h₁.h₁
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ a < 2 ^ Nat.size a

case h₁.h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ b < 2 ^ Nat.size a

State before:
case h₁.h₁
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ a < 2 ^ Nat.size a

case h₁.h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ b < 2 ^ Nat.size a
Tactic:
. exact Nat.lt_size_self _
State after:
case h₁.h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ b < 2 ^ Nat.size a

State before:
case h₁.h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ b < 2 ^ Nat.size a
Tactic:
. exact Nat.lt_of_le_of_lt hba (Nat.lt_size_self _)
State after:
no goals

State before:
case h₁.h₁
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ a < 2 ^ Nat.size a
Tactic:
exact Nat.lt_size_self _
State after:
no goals

State before:
case h₁.h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ b < 2 ^ Nat.size a
Tactic:
exact Nat.lt_of_le_of_lt hba (Nat.lt_size_self _)
State after:
no goals

State before:
case h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ Nat.size a + 1 ≤ Nat.size (a + b)
Tactic:
rewrite [Nat.succ_le, Nat.lt_size]
State after:
case h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ 2 ^ Nat.size a ≤ a + b

State before:
case h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ 2 ^ Nat.size a ≤ a + b
Tactic:
exact carry
State after:
no goals

State before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
⊢ n ≤ Nat.size a
Tactic:
rewrite [← Nat.lt_succ, Nat.succ_eq_add_one]
State after:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
⊢ n < Nat.size a + 1

State before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
⊢ n < Nat.size a + 1
Tactic:
calc
  n < Nat.size (a + b) := by rwa [Nat.lt_size]
  _ = Nat.size a + 1   := size_eq
State after:
no goals

State before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
⊢ n < Nat.size (a + b)
Tactic:
rwa [Nat.lt_size]
State after:
no goals

State before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
le_size : n ≤ Nat.size a
⊢ ulp n (a + b) = 2 * ulp n a
Tactic:
calc
  ulp n (a + b)
    = 2 ^ (Nat.size (a + b) - n) := rfl
  _ = 2 ^ (Nat.size a + 1 - n)   := by rw [size_eq]
  _ = 2 ^ (Nat.size a - n + 1)   := by rw [← tsub_add_eq_add_tsub le_size]
  _ = 2 * 2 ^ (Nat.size a - n)   := by rw [pow_succ]
  _ = 2 * ulp n a                := rfl
State after:
no goals

State before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
le_size : n ≤ Nat.size a
⊢ 2 ^ (Nat.size (a + b) - n) = 2 ^ (Nat.size a + 1 - n)
Tactic:
rw [size_eq]
State after:
no goals

State before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
le_size : n ≤ Nat.size a
⊢ 2 ^ (Nat.size a + 1 - n) = 2 ^ (Nat.size a - n + 1)
Tactic:
rw [← tsub_add_eq_add_tsub le_size]
State after:
no goals

State before:
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
le_size : n ≤ Nat.size a
⊢ 2 ^ (Nat.size a - n + 1) = 2 * 2 ^ (Nat.size a - n)
Tactic:
rw [pow_succ]
State after:
no goals