internlm/Lean-Github huggingface dataset:
Theorem: next_trunc_sub_eq_ulp_sub_mod
Proof state before:
n : ℕ
npos : 0 < n
c : ℕ
⊢ trunc n c + ulp n (trunc n c) - c = ulp n c - c % ulp n c
Tactic:
rewrite [ulp_trunc npos]
Proof state after:
n : ℕ
npos : 0 < n
c : ℕ
⊢ trunc n c + ulp n c - c = ulp n c - c % ulp n c
Theorem: next_trunc_sub_eq_ulp_sub_mod
Proof state before:
n : ℕ
npos : 0 < n
c : ℕ
⊢ trunc n c + ulp n c - c = ulp n c - c % ulp n c
Tactic:
rewrite [trunc_eq_sub_mod]
Proof state after:
n : ℕ
npos : 0 < n
c : ℕ
⊢ c - c % ulp n c + ulp n c - c = ulp n c - c % ulp n c
Theorem: next_trunc_sub_eq_ulp_sub_mod
Proof state before:
n : ℕ
npos : 0 < n
c : ℕ
⊢ c - c % ulp n c + ulp n c - c = ulp n c - c % ulp n c
Tactic:
rewrite [tsub_add_eq_add_tsub (Nat.mod_le _ _)]
Proof state after:
n : ℕ
npos : 0 < n
c : ℕ
⊢ c + ulp n c - c % ulp n c - c = ulp n c - c % ulp n c
Theorem: next_trunc_sub_eq_ulp_sub_mod
Proof state before:
n : ℕ
npos : 0 < n
c : ℕ
⊢ c + ulp n c - c % ulp n c - c = ulp n c - c % ulp n c
Tactic:
rewrite [tsub_right_comm]
Proof state after:
n : ℕ
npos : 0 < n
c : ℕ
⊢ c + ulp n c - c - c % ulp n c = ulp n c - c % ulp n c
Theorem: next_trunc_sub_eq_ulp_sub_mod
Proof state before:
n : ℕ
npos : 0 < n
c : ℕ
⊢ c + ulp n c - c - c % ulp n c = ulp n c - c % ulp n c
Tactic:
rw [add_tsub_cancel_left]
Proof state after:
no goals
Theorem: next_trunc_pred_trunc_eq_self
Proof state before:
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ next n (trunc n (trunc n x - 1)) = trunc n x
Tactic:
symm
Proof state after:
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x = next n (trunc n (trunc n x - 1))
Theorem: next_trunc_pred_trunc_eq_self
Proof state before:
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x = next n (trunc n (trunc n x - 1))
Tactic:
rewrite [← trunc_next_comm npos (trunc n x - 1)]
Proof state after:
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x = trunc n (next n (trunc n x - 1))
Theorem: next_trunc_pred_trunc_eq_self
Proof state before:
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x = trunc n (next n (trunc n x - 1))
Tactic:
unfold next
Proof state after:
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x = trunc n (trunc n x - 1 + ulp n (trunc n x - 1))
Theorem: next_trunc_pred_trunc_eq_self
Proof state before:
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x = trunc n (trunc n x - 1 + ulp n (trunc n x - 1))
Tactic:
apply trunc_eq_trunc_of_le_of_lt npos
Proof state after:
case h
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x ≤ trunc n x - 1 + ulp n (trunc n x - 1)

case k
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - 1 + ulp n (trunc n x - 1) < next n (trunc n x)
Theorem: next_trunc_pred_trunc_eq_self
Proof state before:
case h
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x ≤ trunc n x - 1 + ulp n (trunc n x - 1)

case k
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - 1 + ulp n (trunc n x - 1) < next n (trunc n x)
Tactic:
. rewrite [← tsub_le_iff_right]
  apply tsub_le_tsub_left
  exact Nat.one_le_of_lt (ulp_pos _ _)
Proof state after:
case k
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - 1 + ulp n (trunc n x - 1) < next n (trunc n x)
Theorem: next_trunc_pred_trunc_eq_self
Proof state before:
case k
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - 1 + ulp n (trunc n x - 1) < next n (trunc n x)
Tactic:
. apply add_lt_add_of_lt_of_le
  . exact tsub_lt_self xpos zero_lt_one
  . exact ulp_le_ulp n tsub_le_self
Proof state after:
no goals
Theorem: next_trunc_pred_trunc_eq_self
Proof state before:
case h
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x ≤ trunc n x - 1 + ulp n (trunc n x - 1)
Tactic:
rewrite [← tsub_le_iff_right]
Proof state after:
case h
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - ulp n (trunc n x - 1) ≤ trunc n x - 1
Theorem: next_trunc_pred_trunc_eq_self
Proof state before:
case h
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - ulp n (trunc n x - 1) ≤ trunc n x - 1
Tactic:
apply tsub_le_tsub_left
Proof state after:
case h.h
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ 1 ≤ ulp n (trunc n x - 1)
Theorem: next_trunc_pred_trunc_eq_self
Proof state before:
case h.h
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ 1 ≤ ulp n (trunc n x - 1)
Tactic:
exact Nat.one_le_of_lt (ulp_pos _ _)
Proof state after:
no goals
Theorem: next_trunc_pred_trunc_eq_self
Proof state before:
case k
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - 1 + ulp n (trunc n x - 1) < next n (trunc n x)
Tactic:
apply add_lt_add_of_lt_of_le
Proof state after:
case k.h₁
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - 1 < trunc n x

case k.h₂
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ ulp n (trunc n x - 1) ≤ ulp n (trunc n x)
Theorem: next_trunc_pred_trunc_eq_self
Proof state before:
case k.h₁
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - 1 < trunc n x

case k.h₂
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ ulp n (trunc n x - 1) ≤ ulp n (trunc n x)
Tactic:
. exact tsub_lt_self xpos zero_lt_one
Proof state after:
case k.h₂
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ ulp n (trunc n x - 1) ≤ ulp n (trunc n x)
Theorem: next_trunc_pred_trunc_eq_self
Proof state before:
case k.h₂
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ ulp n (trunc n x - 1) ≤ ulp n (trunc n x)
Tactic:
. exact ulp_le_ulp n tsub_le_self
Proof state after:
no goals
Theorem: next_trunc_pred_trunc_eq_self
Proof state before:
case k.h₁
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - 1 < trunc n x
Tactic:
exact tsub_lt_self xpos zero_lt_one
Proof state after:
no goals
Theorem: next_trunc_pred_trunc_eq_self
Proof state before:
case k.h₂
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ ulp n (trunc n x - 1) ≤ ulp n (trunc n x)
Tactic:
exact ulp_le_ulp n tsub_le_self
Proof state after:
no goals
Theorem: round_eq_next_trunc_of_gt
Proof state before:
n x : ℕ
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x > x
⊢ round x = next n (trunc n x)
Tactic:
cases hfaithful₁ x with
| inl hlo =>
  exfalso
  apply Nat.lt_le_asymm h
  exact hlo ▸ (trunc_le n x)
| inr hhi => exact hhi
Proof state after:
no goals
Theorem: round_eq_next_trunc_of_gt
Proof state before:
case inl
n x : ℕ
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x > x
hlo : round x = trunc n x
⊢ round x = next n (trunc n x)
Tactic:
exfalso
Proof state after:
case inl.h
n x : ℕ
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x > x
hlo : round x = trunc n x
⊢ False
Theorem: round_eq_next_trunc_of_gt
Proof state before:
case inl.h
n x : ℕ
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x > x
hlo : round x = trunc n x
⊢ False
Tactic:
apply Nat.lt_le_asymm h
Proof state after:
case inl.h
n x : ℕ
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x > x
hlo : round x = trunc n x
⊢ round x ≤ x
Theorem: round_eq_next_trunc_of_gt
Proof state before:
case inl.h
n x : ℕ
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x > x
hlo : round x = trunc n x
⊢ round x ≤ x
Tactic:
exact hlo ▸ (trunc_le n x)
Proof state after:
no goals
Theorem: round_eq_next_trunc_of_gt
Proof state before:
case inr
n x : ℕ
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x > x
hhi : round x = next n (trunc n x)
⊢ round x = next n (trunc n x)
Tactic:
exact hhi
Proof state after:
no goals
Theorem: trunc_round
Proof state before:
n : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
x : ℕ
⊢ trunc n (round x) = round x
Tactic:
cases hfaithful₁ x with
| inl lo => rw [lo, trunc_idempotent npos]
| inr hi => rw [hi, trunc_next_comm npos, trunc_idempotent npos]
Proof state after:
no goals
Theorem: trunc_round
Proof state before:
case inl
n : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
x : ℕ
lo : round x = trunc n x
⊢ trunc n (round x) = round x
Tactic:
rw [lo, trunc_idempotent npos]
Proof state after:
no goals
Theorem: trunc_round
Proof state before:
case inr
n : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
x : ℕ
hi : round x = next n (trunc n x)
⊢ trunc n (round x) = round x
Tactic:
rw [hi, trunc_next_comm npos, trunc_idempotent npos]
Proof state after:
no goals
Theorem: trunc_eq_of_round_eq
Proof state before:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
round_eq : round x = x
⊢ trunc n x = x
Tactic:
rw [← round_eq, trunc_round npos hfaithful₁ x]
Proof state after:
no goals
Theorem: round_eq_of_trunc_eq
Proof state before:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
trunc_eq : trunc n x = x
⊢ round x = x
Tactic:
rw [← trunc_eq, round_trunc npos x hfaithful₀]
Proof state after:
no goals
Theorem: round_eq_trunc_of_le
Proof state before:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x ≤ x
⊢ round x = trunc n x
Tactic:
cases hfaithful₁ x with
| inl hlo => exact hlo
| inr hhi =>
  exfalso
  apply Nat.lt_le_asymm (lt_next_trunc npos x)
  exact hhi ▸ h
Proof state after:
no goals
Theorem: round_eq_trunc_of_le
Proof state before:
case inl
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x ≤ x
hlo : round x = trunc n x
⊢ round x = trunc n x
Tactic:
exact hlo
Proof state after:
no goals
Theorem: round_eq_trunc_of_le
Proof state before:
case inr
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x ≤ x
hhi : round x = next n (trunc n x)
⊢ round x = trunc n x
Tactic:
exfalso
Proof state after:
case inr.h
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x ≤ x
hhi : round x = next n (trunc n x)
⊢ False
Theorem: round_eq_trunc_of_le
Proof state before:
case inr.h
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x ≤ x
hhi : round x = next n (trunc n x)
⊢ False
Tactic:
apply Nat.lt_le_asymm (lt_next_trunc npos x)
Proof state after:
case inr.h
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x ≤ x
hhi : round x = next n (trunc n x)
⊢ next n (trunc n x) ≤ x
Theorem: round_eq_trunc_of_le
Proof state before:
case inr.h
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x ≤ x
hhi : round x = next n (trunc n x)
⊢ next n (trunc n x) ≤ x
Tactic:
exact hhi ▸ h
Proof state after:
no goals
Theorem: le_midpoint_of_round_eq_trunc
Proof state before:
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
⊢ x ≤ trunc n x + ulp n x / 2
Tactic:
cases Nat.lt_or_ge x (2 ^ n) with
| inl uflow =>
  exact ge_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 h2,
      Nat.add_comm, ← le_tsub_iff_right h1]
  exact hcorrect₀ x hlo
Proof state after:
no goals
Theorem: le_midpoint_of_round_eq_trunc
Proof state before:
case inl
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
uflow : x < 2 ^ n
⊢ x ≤ trunc n x + ulp n x / 2
Tactic:
exact ge_of_eq (trunc_add_half_ulp_eq_of_uflow uflow)
Proof state after:
no goals
Theorem: le_midpoint_of_round_eq_trunc
Proof state before:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
⊢ x ≤ trunc n x + ulp n x / 2
Tactic:
refine Nat.le_of_mul_le_mul_left ?_ two_pos
Proof state after:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
⊢ 2 * x ≤ 2 * (trunc n x + ulp n x / 2)
Theorem: le_midpoint_of_round_eq_trunc
Proof state before:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
⊢ 2 * x ≤ 2 * (trunc n x + ulp n x / 2)
Tactic:
rewrite [trunc_add_half_ulp_eq_of_no_uflow npos no_uflow]
Proof state after:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
⊢ 2 * x ≤ trunc n x + next n (trunc n x)
Theorem: le_midpoint_of_round_eq_trunc
Proof state before:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
⊢ 2 * x ≤ trunc n x + next n (trunc n x)
Tactic:
have h1 : x ≤ next n (trunc n x) := Nat.le_of_lt (lt_next_trunc npos x)
Proof state after:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
⊢ 2 * x ≤ trunc n x + next n (trunc n x)
Theorem: le_midpoint_of_round_eq_trunc
Proof state before:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
⊢ 2 * x ≤ trunc n x + next n (trunc n x)
Tactic:
have h2 : trunc n x ≤ x := trunc_le n x
Proof state after:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
h2 : trunc n x ≤ x
⊢ 2 * x ≤ trunc n x + next n (trunc n x)
Theorem: le_midpoint_of_round_eq_trunc
Proof state before:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
h2 : trunc n x ≤ x
⊢ 2 * x ≤ trunc n x + next n (trunc n x)
Tactic:
rewrite [Nat.two_mul, ← tsub_le_iff_left, add_tsub_assoc_of_le h2,
    Nat.add_comm, ← le_tsub_iff_right h1]
Proof state after:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
h2 : trunc n x ≤ x
⊢ x - trunc n x ≤ next n (trunc n x) - x
Theorem: le_midpoint_of_round_eq_trunc
Proof state before:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₀ : correct₀ n round
hlo : round x = trunc n x
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
h2 : trunc n x ≤ x
⊢ x - trunc n x ≤ next n (trunc n x) - x
Tactic:
exact hcorrect₀ x hlo
Proof state after:
no goals
Theorem: round_eq_trunc_of_lt_midpoint
Proof 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
Proof state after:
no goals
Theorem: round_eq_trunc_of_lt_midpoint
Proof 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]
Proof 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
Theorem: round_eq_trunc_of_lt_midpoint
Proof 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]
Proof state after:
no goals
Theorem: round_eq_trunc_of_lt_midpoint
Proof 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
Proof 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
Theorem: round_eq_trunc_of_lt_midpoint
Proof 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]
Proof 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
Theorem: round_eq_trunc_of_lt_midpoint
Proof 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]
Proof state after:
no goals
Theorem: round_eq_trunc_of_lt_midpoint
Proof 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
Proof 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
Theorem: round_eq_trunc_of_lt_midpoint
Proof 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)
Proof 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
Theorem: round_eq_trunc_of_lt_midpoint
Proof 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
Proof 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
Theorem: round_eq_trunc_of_lt_midpoint
Proof 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
Proof state after:
no goals
Theorem: round_eq_trunc_of_lt_midpoint
Proof 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)]
Proof 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)
Theorem: round_eq_trunc_of_lt_midpoint
Proof 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))]
Proof 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
Theorem: round_eq_trunc_of_lt_midpoint
Proof 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
Proof 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
Theorem: round_eq_trunc_of_lt_midpoint
Proof 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]
Proof 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
Theorem: round_eq_trunc_of_lt_midpoint
Proof 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]
Proof 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)