internlm/Lean-Github huggingface dataset:
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
one_le_size_sub : 1 ≤ Nat.size a - n
le_size_sub_one : n ≤ Nat.size a - 1
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
lt : b < ulp n (a - b) / 2
⊢ ulp n (a - b) / 2 < ulp n (a - b) - b
Tactic:
rewrite [lt_tsub_comm]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
one_le_size_sub : 1 ≤ Nat.size a - n
le_size_sub_one : n ≤ Nat.size a - 1
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
lt : b < ulp n (a - b) / 2
⊢ b < ulp n (a - b) - ulp n (a - b) / 2
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
one_le_size_sub : 1 ≤ Nat.size a - n
le_size_sub_one : n ≤ Nat.size a - 1
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
lt : b < ulp n (a - b) / 2
⊢ b < ulp n (a - b) - ulp n (a - b) / 2
Tactic:
rewrite [sub_half_of_even ulp_even]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
one_le_size_sub : 1 ≤ Nat.size a - n
le_size_sub_one : n ≤ Nat.size a - 1
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
lt : b < ulp n (a - b) / 2
⊢ b < ulp n (a - b) / 2
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
one_le_size_sub : 1 ≤ Nat.size a - n
le_size_sub_one : n ≤ Nat.size a - 1
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
lt : b < ulp n (a - b) / 2
⊢ b < ulp n (a - b) / 2
Tactic:
exact lt
Proof state after:
no goals
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
one_le_size_sub : 1 ≤ Nat.size a - n
le_size_sub_one : n ≤ Nat.size a - 1
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
lt : b < ulp n (a - b) / 2
k₁ : ulp n (a - b) / 2 < ulp n (a - b) - b
⊢ ulp n (a - b) / 2 < a - b - trunc n (a - b)
Tactic:
rewrite [h₂]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
one_le_size_sub : 1 ≤ Nat.size a - n
le_size_sub_one : n ≤ Nat.size a - 1
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
lt : b < ulp n (a - b) / 2
k₁ : ulp n (a - b) / 2 < ulp n (a - b) - b
⊢ ulp n (a - b) / 2 < ulp n (a - b) - b
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
one_le_size_sub : 1 ≤ Nat.size a - n
le_size_sub_one : n ≤ Nat.size a - 1
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
lt : b < ulp n (a - b) / 2
k₁ : ulp n (a - b) / 2 < ulp n (a - b) - b
⊢ ulp n (a - b) / 2 < ulp n (a - b) - b
Tactic:
exact k₁
Proof state after:
no goals
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
one_le_size_sub : 1 ≤ Nat.size a - n
le_size_sub_one : n ≤ Nat.size a - 1
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
lt : b < ulp n (a - b) / 2
k₁ : ulp n (a - b) / 2 < ulp n (a - b) - b
k₂ : ulp n (a - b) / 2 < a - b - trunc n (a - b)
⊢ a - b - trunc n (a - b) ≤ ulp n (a - b) / 2
Tactic:
rewrite [tsub_le_iff_left]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
one_le_size_sub : 1 ≤ Nat.size a - n
le_size_sub_one : n ≤ Nat.size a - 1
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
lt : b < ulp n (a - b) / 2
k₁ : ulp n (a - b) / 2 < ulp n (a - b) - b
k₂ : ulp n (a - b) / 2 < a - b - trunc n (a - b)
⊢ a - b ≤ trunc n (a - b) + ulp n (a - b) / 2
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
one_le_size_sub : 1 ≤ Nat.size a - n
le_size_sub_one : n ≤ Nat.size a - 1
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
lt : b < ulp n (a - b) / 2
k₁ : ulp n (a - b) / 2 < ulp n (a - b) - b
k₂ : ulp n (a - b) / 2 < a - b - trunc n (a - b)
⊢ a - b ≤ trunc n (a - b) + ulp n (a - b) / 2
Tactic:
apply le_midpoint_of_round_eq_trunc npos hcorrect₀
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
one_le_size_sub : 1 ≤ Nat.size a - n
le_size_sub_one : n ≤ Nat.size a - 1
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
lt : b < ulp n (a - b) / 2
k₁ : ulp n (a - b) / 2 < ulp n (a - b) - b
k₂ : ulp n (a - b) / 2 < a - b - trunc n (a - b)
⊢ round (a - b) = trunc n (a - b)
Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
one_le_size_sub : 1 ≤ Nat.size a - n
le_size_sub_one : n ≤ Nat.size a - 1
h₂ : a - b - trunc n (a - b) = ulp n (a - b) - b
lt : b < ulp n (a - b) / 2
k₁ : ulp n (a - b) / 2 < ulp n (a - b) - b
k₂ : ulp n (a - b) / 2 < a - b - trunc n (a - b)
⊢ round (a - b) = trunc n (a - b)
Tactic:
exact round_eq_trunc_of_le npos hfaithful₁ round_lt.le
Proof state after:
no goals
Theorem: b₁
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
cases Nat.lt_or_ge (a - b) (2 ^ n) with
| inl uflow =>
  apply b₁_of_round_eq
  apply round_eq_of_trunc_eq npos hfaithful₀
  exact trunc_eq_self_of_uflow uflow
| inr no_uflow =>
  cases Nat.eq_zero_or_pos b with
  | inl bzero =>
    apply b₁_of_round_eq
    rewrite [bzero, tsub_zero]
    exact round_eq_of_trunc_eq npos hfaithful₀ hfa
  | inr bpos =>
    cases Nat.lt_or_ge (2 * b) a with
    | inr le_two_mul =>
      apply b₁_of_round_eq
      apply round_eq_of_trunc_eq npos hfaithful₀
      exact sterbenz hfa hfb hba le_two_mul
    | inl two_mul_lt =>
      rcases Nat.lt_trichotomy (a - b) (round (a - b)) with (lt_round | eq_round | round_lt)
      . constructor
        . exact b₁_lo_of_lt_round npos hfaithful₁ lt_round
        . exact b₁_hi_of_two_mul_le_of_lt_round npos hfaithful₀ hfaithful₁
            hfa hfb two_mul_lt.le lt_round
      . exact b₁_of_round_eq eq_round.symm
      . constructor
        . cases Nat.lt_or_ge b (ulp n (a - b)) with
          | inl lt_ulp =>
            cases Nat.eq_or_lt_of_le (ulp_le_ulp n tsub_le_self) with
            | inl ulp_eq_ulp =>
              exact b₁_lo_of_round_lt_of_no_uflow_of_ulp_eq_ulp_of_two_mul_lt_of_pos_of_le_ulp
                npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
                round_lt no_uflow ulp_eq_ulp bpos (ulp_eq_ulp ▸ lt_ulp.le)
            | inr ulp_lt_ulp =>
              exact b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
                npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
                round_lt no_uflow ulp_lt_ulp two_mul_lt bpos lt_ulp.le
          | inr ulp_le =>
            exact b₁_lo_of_round_le_of_two_mul_le_of_ulp_le npos hfaithful₁
              hfa hfb round_lt.le two_mul_lt.le ulp_le
        . exact b₁_hi_of_round_le npos hfaithful₁ round_lt.le
Proof state after:
no goals
Theorem: b₁
Proof state before:
case inl
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
uflow : a - b < 2 ^ n
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
apply b₁_of_round_eq
Proof state after:
case inl.round_eq
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
uflow : a - b < 2 ^ n
⊢ round (a - b) = a - b
Theorem: b₁
Proof state before:
case inl.round_eq
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
uflow : a - b < 2 ^ n
⊢ round (a - b) = a - b
Tactic:
apply round_eq_of_trunc_eq npos hfaithful₀
Proof state after:
case inl.round_eq
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
uflow : a - b < 2 ^ n
⊢ trunc n (a - b) = a - b
Theorem: b₁
Proof state before:
case inl.round_eq
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
uflow : a - b < 2 ^ n
⊢ trunc n (a - b) = a - b
Tactic:
exact trunc_eq_self_of_uflow uflow
Proof state after:
no goals
Theorem: b₁
Proof state before:
case inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
cases Nat.eq_zero_or_pos b with
| inl bzero =>
  apply b₁_of_round_eq
  rewrite [bzero, tsub_zero]
  exact round_eq_of_trunc_eq npos hfaithful₀ hfa
| inr bpos =>
  cases Nat.lt_or_ge (2 * b) a with
  | inr le_two_mul =>
    apply b₁_of_round_eq
    apply round_eq_of_trunc_eq npos hfaithful₀
    exact sterbenz hfa hfb hba le_two_mul
  | inl two_mul_lt =>
    rcases Nat.lt_trichotomy (a - b) (round (a - b)) with (lt_round | eq_round | round_lt)
    . constructor
      . exact b₁_lo_of_lt_round npos hfaithful₁ lt_round
      . exact b₁_hi_of_two_mul_le_of_lt_round npos hfaithful₀ hfaithful₁
          hfa hfb two_mul_lt.le lt_round
    . exact b₁_of_round_eq eq_round.symm
    . constructor
      . cases Nat.lt_or_ge b (ulp n (a - b)) with
        | inl lt_ulp =>
          cases Nat.eq_or_lt_of_le (ulp_le_ulp n tsub_le_self) with
          | inl ulp_eq_ulp =>
            exact b₁_lo_of_round_lt_of_no_uflow_of_ulp_eq_ulp_of_two_mul_lt_of_pos_of_le_ulp
              npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
              round_lt no_uflow ulp_eq_ulp bpos (ulp_eq_ulp ▸ lt_ulp.le)
          | inr ulp_lt_ulp =>
            exact b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
              npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
              round_lt no_uflow ulp_lt_ulp two_mul_lt bpos lt_ulp.le
        | inr ulp_le =>
          exact b₁_lo_of_round_le_of_two_mul_le_of_ulp_le npos hfaithful₁
            hfa hfb round_lt.le two_mul_lt.le ulp_le
      . exact b₁_hi_of_round_le npos hfaithful₁ round_lt.le
Proof state after:
no goals
Theorem: b₁
Proof state before:
case inr.inl
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bzero : b = 0
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
apply b₁_of_round_eq
Proof state after:
case inr.inl.round_eq
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bzero : b = 0
⊢ round (a - b) = a - b
Theorem: b₁
Proof state before:
case inr.inl.round_eq
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bzero : b = 0
⊢ round (a - b) = a - b
Tactic:
rewrite [bzero, tsub_zero]
Proof state after:
case inr.inl.round_eq
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bzero : b = 0
⊢ round a = a
Theorem: b₁
Proof state before:
case inr.inl.round_eq
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bzero : b = 0
⊢ round a = a
Tactic:
exact round_eq_of_trunc_eq npos hfaithful₀ hfa
Proof state after:
no goals
Theorem: b₁
Proof state before:
case inr.inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
cases Nat.lt_or_ge (2 * b) a with
| inr le_two_mul =>
  apply b₁_of_round_eq
  apply round_eq_of_trunc_eq npos hfaithful₀
  exact sterbenz hfa hfb hba le_two_mul
| inl two_mul_lt =>
  rcases Nat.lt_trichotomy (a - b) (round (a - b)) with (lt_round | eq_round | round_lt)
  . constructor
    . exact b₁_lo_of_lt_round npos hfaithful₁ lt_round
    . exact b₁_hi_of_two_mul_le_of_lt_round npos hfaithful₀ hfaithful₁
        hfa hfb two_mul_lt.le lt_round
  . exact b₁_of_round_eq eq_round.symm
  . constructor
    . cases Nat.lt_or_ge b (ulp n (a - b)) with
      | inl lt_ulp =>
        cases Nat.eq_or_lt_of_le (ulp_le_ulp n tsub_le_self) with
        | inl ulp_eq_ulp =>
          exact b₁_lo_of_round_lt_of_no_uflow_of_ulp_eq_ulp_of_two_mul_lt_of_pos_of_le_ulp
            npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
            round_lt no_uflow ulp_eq_ulp bpos (ulp_eq_ulp ▸ lt_ulp.le)
        | inr ulp_lt_ulp =>
          exact b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
            npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
            round_lt no_uflow ulp_lt_ulp two_mul_lt bpos lt_ulp.le
      | inr ulp_le =>
        exact b₁_lo_of_round_le_of_two_mul_le_of_ulp_le npos hfaithful₁
          hfa hfb round_lt.le two_mul_lt.le ulp_le
    . exact b₁_hi_of_round_le npos hfaithful₁ round_lt.le
Proof state after:
no goals
Theorem: b₁
Proof state before:
case inr.inr.inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
le_two_mul : 2 * b ≥ a
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
apply b₁_of_round_eq
Proof state after:
case inr.inr.inr.round_eq
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
le_two_mul : 2 * b ≥ a
⊢ round (a - b) = a - b
Theorem: b₁
Proof state before:
case inr.inr.inr.round_eq
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
le_two_mul : 2 * b ≥ a
⊢ round (a - b) = a - b
Tactic:
apply round_eq_of_trunc_eq npos hfaithful₀
Proof state after:
case inr.inr.inr.round_eq
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
le_two_mul : 2 * b ≥ a
⊢ trunc n (a - b) = a - b
Theorem: b₁
Proof state before:
case inr.inr.inr.round_eq
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
le_two_mul : 2 * b ≥ a
⊢ trunc n (a - b) = a - b
Tactic:
exact sterbenz hfa hfb hba le_two_mul
Proof state after:
no goals