internlm/Lean-Github huggingface dataset:
Theorem: trunc_next_of_carry
Proof state before:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ expt n (next n x) ≤ Nat.size x

case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ 2 ^ Nat.size x ≤ next n x

case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ next n x < 2 ^ Nat.size x + 2 ^ expt n (next n x)
Tactic:
. unfold expt
  rewrite [size_next_eq_succ_size_of_carry carry]
  rewrite [tsub_le_iff_tsub_le]
  rewrite [add_tsub_cancel_left]
  exact Nat.one_le_of_lt npos
Proof state after:
case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ 2 ^ Nat.size x ≤ next n x

case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ next n x < 2 ^ Nat.size x + 2 ^ expt n (next n x)
Theorem: trunc_next_of_carry
Proof state before:
case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ 2 ^ Nat.size x ≤ next n x

case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ next n x < 2 ^ Nat.size x + 2 ^ expt n (next n x)
Tactic:
. exact carry
Proof state after:
case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ next n x < 2 ^ Nat.size x + 2 ^ expt n (next n x)
Theorem: trunc_next_of_carry
Proof state before:
case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ next n x < 2 ^ Nat.size x + 2 ^ expt n (next n x)
Tactic:
. apply add_lt_add_of_lt_of_le
  . exact Nat.lt_size_self x
  . apply ulp_le_ulp
    exact Nat.le_add_right x (2 ^ expt n x)
Proof state after:
no goals
Theorem: trunc_next_of_carry
Proof state before:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ expt n (next n x) ≤ Nat.size x
Tactic:
unfold expt
Proof state after:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size (next n x) - n ≤ Nat.size x
Theorem: trunc_next_of_carry
Proof state before:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size (next n x) - n ≤ Nat.size x
Tactic:
rewrite [size_next_eq_succ_size_of_carry carry]
Proof state after:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 - n ≤ Nat.size x
Theorem: trunc_next_of_carry
Proof state before:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 - n ≤ Nat.size x
Tactic:
rewrite [tsub_le_iff_tsub_le]
Proof state after:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 - Nat.size x ≤ n
Theorem: trunc_next_of_carry
Proof state before:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 - Nat.size x ≤ n
Tactic:
rewrite [add_tsub_cancel_left]
Proof state after:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ 1 ≤ n
Theorem: trunc_next_of_carry
Proof state before:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ 1 ≤ n
Tactic:
exact Nat.one_le_of_lt npos
Proof state after:
no goals
Theorem: trunc_next_of_carry
Proof state before:
case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ 2 ^ Nat.size x ≤ next n x
Tactic:
exact carry
Proof state after:
no goals
Theorem: trunc_next_of_carry
Proof state before:
case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ next n x < 2 ^ Nat.size x + 2 ^ expt n (next n x)
Tactic:
apply add_lt_add_of_lt_of_le
Proof state after:
case a.h₁
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ x < 2 ^ Nat.size x

case a.h₂
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ ulp n x ≤ 2 ^ expt n (next n x)
Theorem: trunc_next_of_carry
Proof state before:
case a.h₁
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ x < 2 ^ Nat.size x

case a.h₂
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ ulp n x ≤ 2 ^ expt n (next n x)
Tactic:
. exact Nat.lt_size_self x
Proof state after:
case a.h₂
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ ulp n x ≤ 2 ^ expt n (next n x)
Theorem: trunc_next_of_carry
Proof state before:
case a.h₂
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ ulp n x ≤ 2 ^ expt n (next n x)
Tactic:
. apply ulp_le_ulp
  exact Nat.le_add_right x (2 ^ expt n x)
Proof state after:
no goals
Theorem: trunc_next_of_carry
Proof state before:
case a.h₁
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ x < 2 ^ Nat.size x
Tactic:
exact Nat.lt_size_self x
Proof state after:
no goals
Theorem: trunc_next_of_carry
Proof state before:
case a.h₂
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ ulp n x ≤ 2 ^ expt n (next n x)
Tactic:
apply ulp_le_ulp
Proof state after:
case a.h₂.h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ x ≤ next n x
Theorem: trunc_next_of_carry
Proof state before:
case a.h₂.h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ x ≤ next n x
Tactic:
exact Nat.le_add_right x (2 ^ expt n x)
Proof state after:
no goals
Theorem: next_trunc_of_carry
Proof state before:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ next n (trunc n x) = 2 ^ Nat.size x
Tactic:
unfold next
Proof state after:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ trunc n x + ulp n (trunc n x) = 2 ^ Nat.size x
Theorem: next_trunc_of_carry
Proof state before:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ trunc n x + ulp n (trunc n x) = 2 ^ Nat.size x
Tactic:
rewrite [ulp_trunc npos]
Proof state after:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ trunc n x + ulp n x = 2 ^ Nat.size x
Theorem: next_trunc_of_carry
Proof state before:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ trunc n x + ulp n x = 2 ^ Nat.size x
Tactic:
unfold trunc ulp
Proof state after:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ x / 2 ^ expt n x * 2 ^ expt n x + 2 ^ expt n x = 2 ^ Nat.size x
Theorem: next_trunc_of_carry
Proof state before:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ x / 2 ^ expt n x * 2 ^ expt n x + 2 ^ expt n x = 2 ^ Nat.size x
Tactic:
rewrite [← Nat.succ_mul]
Proof state after:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.succ (x / 2 ^ expt n x) * 2 ^ expt n x = 2 ^ Nat.size x
Theorem: next_trunc_of_carry
Proof state before:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.succ (x / 2 ^ expt n x) * 2 ^ expt n x = 2 ^ Nat.size x
Tactic:
rewrite [← Nat.add_div_right x two_pow_pos]
Proof state after:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ (x + 2 ^ expt n x) / 2 ^ expt n x * 2 ^ expt n x = 2 ^ Nat.size x
Theorem: next_trunc_of_carry
Proof state before:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ (x + 2 ^ expt n x) / 2 ^ expt n x * 2 ^ expt n x = 2 ^ Nat.size x
Tactic:
have h₁ : expt n x ≤ Nat.size x := tsub_le_self
Proof state after:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
h₁ : expt n x ≤ Nat.size x
⊢ (x + 2 ^ expt n x) / 2 ^ expt n x * 2 ^ expt n x = 2 ^ Nat.size x
Theorem: next_trunc_of_carry
Proof state before:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
h₁ : expt n x ≤ Nat.size x
⊢ (x + 2 ^ expt n x) / 2 ^ expt n x * 2 ^ expt n x = 2 ^ Nat.size x
Tactic:
have h₃ : next n x < 2 ^ Nat.size x + 2 ^ expt n x :=
  Nat.add_lt_add_right (Nat.lt_size_self x) _
Proof state after:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
h₁ : expt n x ≤ Nat.size x
h₃ : next n x < 2 ^ Nat.size x + 2 ^ expt n x
⊢ (x + 2 ^ expt n x) / 2 ^ expt n x * 2 ^ expt n x = 2 ^ Nat.size x
Theorem: next_trunc_of_carry
Proof state before:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
h₁ : expt n x ≤ Nat.size x
h₃ : next n x < 2 ^ Nat.size x + 2 ^ expt n x
⊢ (x + 2 ^ expt n x) / 2 ^ expt n x * 2 ^ expt n x = 2 ^ Nat.size x
Tactic:
exact div_mul_eq_of_le_of_lt h₁ carry h₃
Proof state after:
no goals
Theorem: trunc_next_comm
Proof state before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ trunc n (next n x) = next n (trunc n x)
Tactic:
cases Nat.lt_or_ge (next n x) (2 ^ Nat.size x) with
| inl next_lt => exact trunc_next_comm_of_no_carry npos next_lt
| inr next_ge => rw [next_trunc_of_carry npos next_ge, trunc_next_of_carry npos next_ge]
Proof state after:
no goals
Theorem: trunc_next_comm
Proof state before:
case inl
n : ℕ
npos : 0 < n
x : ℕ
next_lt : next n x < 2 ^ Nat.size x
⊢ trunc n (next n x) = next n (trunc n x)
Tactic:
exact trunc_next_comm_of_no_carry npos next_lt
Proof state after:
no goals
Theorem: trunc_next_comm
Proof state before:
case inr
n : ℕ
npos : 0 < n
x : ℕ
next_ge : next n x ≥ 2 ^ Nat.size x
⊢ trunc n (next n x) = next n (trunc n x)
Tactic:
rw [next_trunc_of_carry npos next_ge, trunc_next_of_carry npos next_ge]
Proof state after:
no goals
Theorem: lt_next_trunc
Proof state before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ x < next n (trunc n x)
Tactic:
unfold next
Proof state after:
n : ℕ
npos : 0 < n
x : ℕ
⊢ x < trunc n x + ulp n (trunc n x)
Theorem: lt_next_trunc
Proof state before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ x < trunc n x + ulp n (trunc n x)
Tactic:
rewrite [ulp_trunc npos]
Proof state after:
n : ℕ
npos : 0 < n
x : ℕ
⊢ x < trunc n x + ulp n x
Theorem: lt_next_trunc
Proof state before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ x < trunc n x + ulp n x
Tactic:
unfold trunc
Proof state after:
n : ℕ
npos : 0 < n
x : ℕ
⊢ x < x / ulp n x * ulp n x + ulp n x
Theorem: lt_next_trunc
Proof state before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ x < x / ulp n x * ulp n x + ulp n x
Tactic:
rewrite [← Nat.succ_mul, mul_comm]
Proof state after:
n : ℕ
npos : 0 < n
x : ℕ
⊢ x < ulp n x * Nat.succ (x / ulp n x)
Theorem: lt_next_trunc
Proof state before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ x < ulp n x * Nat.succ (x / ulp n x)
Tactic:
exact Nat.lt_mul_div_succ x (ulp_pos n x)
Proof state after:
no goals
Theorem: trunc_next_le
Proof state before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ trunc n (next n x) ≤ 2 ^ Nat.size x
Tactic:
cases Nat.le_total (next n x) (2 ^ Nat.size x) with
| inl le => exact Nat.le_trans (trunc_le n (next n x)) le
| inr ge => exact Nat.le_of_eq (trunc_next_of_carry npos ge)
Proof state after:
no goals
Theorem: trunc_next_le
Proof state before:
case inl
n : ℕ
npos : 0 < n
x : ℕ
le : next n x ≤ 2 ^ Nat.size x
⊢ trunc n (next n x) ≤ 2 ^ Nat.size x
Tactic:
exact Nat.le_trans (trunc_le n (next n x)) le
Proof state after:
no goals
Theorem: trunc_next_le
Proof state before:
case inr
n : ℕ
npos : 0 < n
x : ℕ
ge : 2 ^ Nat.size x ≤ next n x
⊢ trunc n (next n x) ≤ 2 ^ Nat.size x
Tactic:
exact Nat.le_of_eq (trunc_next_of_carry npos ge)
Proof state after:
no goals
Theorem: next_trunc_le
Proof state before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ next n (trunc n x) ≤ 2 ^ Nat.size x
Tactic:
rewrite [← trunc_next_comm npos]
Proof state after:
n : ℕ
npos : 0 < n
x : ℕ
⊢ trunc n (next n x) ≤ 2 ^ Nat.size x
Theorem: next_trunc_le
Proof state before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ trunc n (next n x) ≤ 2 ^ Nat.size x
Tactic:
exact trunc_next_le npos x
Proof state after:
no goals
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ trunc n x = trunc n y
Tactic:
have ulp_eq : ulp n x = ulp n y := by
  rewrite [← ulp_trunc npos]
  apply le_antisymm
  . apply ulp_le_ulp
    exact h
  . rewrite [ulp_trunc npos]
    unfold ulp expt
    apply Nat.pow_le_pow_of_le_right two_pos
    apply tsub_le_tsub_right
    rewrite [Nat.size_le]
    apply Nat.lt_of_lt_of_le k
    exact next_trunc_le npos x
Proof state after:
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ trunc n x = trunc n y
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ trunc n x = trunc n y
Tactic:
unfold trunc
Proof state after:
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ x / ulp n x * ulp n x = y / ulp n y * ulp n y
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ x / ulp n x * ulp n x = y / ulp n y * ulp n y
Tactic:
rewrite [← ulp_eq]
Proof state after:
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ x / ulp n x * ulp n x = y / ulp n x * ulp n x
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ x / ulp n x * ulp n x = y / ulp n x * ulp n x
Tactic:
apply Eq.symm
Proof state after:
case h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y / ulp n x * ulp n x = x / ulp n x * ulp n x
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
case h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y / ulp n x * ulp n x = x / ulp n x * ulp n x
Tactic:
apply congr_arg (fun w => w * ulp n x)
Proof state after:
case h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y / ulp n x = x / ulp n x
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
case h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y / ulp n x = x / ulp n x
Tactic:
apply Nat.eq_of_le_of_lt_succ
Proof state after:
case h.h₁
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ x / ulp n x ≤ y / ulp n x

case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y / ulp n x < x / ulp n x + 1
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
case h.h₁
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ x / ulp n x ≤ y / ulp n x

case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y / ulp n x < x / ulp n x + 1
Tactic:
. rewrite [← Nat.mul_div_cancel (x / ulp n x) (ulp_pos n x)]
  exact Nat.div_le_div_right h
Proof state after:
case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y / ulp n x < x / ulp n x + 1
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y / ulp n x < x / ulp n x + 1
Tactic:
. rewrite [Nat.div_lt_iff_lt_mul (ulp_pos n x)]
  rewrite [Nat.mul_comm, Nat.mul_succ, Nat.mul_comm]
  rewrite [← trunc, ← ulp_trunc npos, ← next]
  exact k
Proof state after:
no goals
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n x = ulp n y
Tactic:
rewrite [← ulp_trunc npos]
Proof state after:
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n (trunc n x) = ulp n y
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n (trunc n x) = ulp n y
Tactic:
apply le_antisymm
Proof state after:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n (trunc n x) ≤ ulp n y

case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n y ≤ ulp n (trunc n x)
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n (trunc n x) ≤ ulp n y

case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n y ≤ ulp n (trunc n x)
Tactic:
. apply ulp_le_ulp
  exact h
Proof state after:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n y ≤ ulp n (trunc n x)
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n y ≤ ulp n (trunc n x)
Tactic:
. rewrite [ulp_trunc npos]
  unfold ulp expt
  apply Nat.pow_le_pow_of_le_right two_pos
  apply tsub_le_tsub_right
  rewrite [Nat.size_le]
  apply Nat.lt_of_lt_of_le k
  exact next_trunc_le npos x
Proof state after:
no goals
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n (trunc n x) ≤ ulp n y
Tactic:
apply ulp_le_ulp
Proof state after:
case a.h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ trunc n x ≤ y
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
case a.h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ trunc n x ≤ y
Tactic:
exact h
Proof state after:
no goals
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n y ≤ ulp n (trunc n x)
Tactic:
rewrite [ulp_trunc npos]
Proof state after:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n y ≤ ulp n x
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n y ≤ ulp n x
Tactic:
unfold ulp expt
Proof state after:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ 2 ^ (Nat.size y - n) ≤ 2 ^ (Nat.size x - n)
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ 2 ^ (Nat.size y - n) ≤ 2 ^ (Nat.size x - n)
Tactic:
apply Nat.pow_le_pow_of_le_right two_pos
Proof state after:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ Nat.size y - n ≤ Nat.size x - n
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ Nat.size y - n ≤ Nat.size x - n
Tactic:
apply tsub_le_tsub_right
Proof state after:
case a.h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ Nat.size y ≤ Nat.size x
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
case a.h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ Nat.size y ≤ Nat.size x
Tactic:
rewrite [Nat.size_le]
Proof state after:
case a.h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ y < 2 ^ Nat.size x
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
case a.h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ y < 2 ^ Nat.size x
Tactic:
apply Nat.lt_of_lt_of_le k
Proof state after:
case a.h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ next n (trunc n x) ≤ 2 ^ Nat.size x
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
case a.h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ next n (trunc n x) ≤ 2 ^ Nat.size x
Tactic:
exact next_trunc_le npos x
Proof state after:
no goals
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
case h.h₁
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ x / ulp n x ≤ y / ulp n x
Tactic:
rewrite [← Nat.mul_div_cancel (x / ulp n x) (ulp_pos n x)]
Proof state after:
case h.h₁
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ x / ulp n x * ulp n x / ulp n x ≤ y / ulp n x
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
case h.h₁
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ x / ulp n x * ulp n x / ulp n x ≤ y / ulp n x
Tactic:
exact Nat.div_le_div_right h
Proof state after:
no goals
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y / ulp n x < x / ulp n x + 1
Tactic:
rewrite [Nat.div_lt_iff_lt_mul (ulp_pos n x)]
Proof state after:
case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y < (x / ulp n x + 1) * ulp n x
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y < (x / ulp n x + 1) * ulp n x
Tactic:
rewrite [Nat.mul_comm, Nat.mul_succ, Nat.mul_comm]
Proof state after:
case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y < x / ulp n x * ulp n x + ulp n x
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y < x / ulp n x * ulp n x + ulp n x
Tactic:
rewrite [← trunc, ← ulp_trunc npos, ← next]
Proof state after:
case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y < next n (trunc n x)
Theorem: trunc_eq_trunc_of_le_of_lt
Proof state before:
case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y < next n (trunc n x)
Tactic:
exact k
Proof state after:
no goals
Theorem: trunc_pred_eq_trunc_of_trunc_ne_self
Proof state before:
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ trunc n (a - 1) = trunc n a
Tactic:
symm
Proof state after:
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ trunc n a = trunc n (a - 1)
Theorem: trunc_pred_eq_trunc_of_trunc_ne_self
Proof state before:
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ trunc n a = trunc n (a - 1)
Tactic:
apply trunc_eq_trunc_of_le_of_lt npos
Proof state after:
case h
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ trunc n a ≤ a - 1

case k
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ a - 1 < next n (trunc n a)
Theorem: trunc_pred_eq_trunc_of_trunc_ne_self
Proof state before:
case h
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ trunc n a ≤ a - 1

case k
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ a - 1 < next n (trunc n a)
Tactic:
. apply Nat.le_pred_of_lt
  exact Nat.lt_of_le_of_ne (trunc_le n a) h
Proof state after:
case k
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ a - 1 < next n (trunc n a)
Theorem: trunc_pred_eq_trunc_of_trunc_ne_self
Proof state before:
case k
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ a - 1 < next n (trunc n a)
Tactic:
. exact Nat.lt_of_le_of_lt tsub_le_self (lt_next_trunc npos a)
Proof state after:
no goals
Theorem: trunc_pred_eq_trunc_of_trunc_ne_self
Proof state before:
case h
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ trunc n a ≤ a - 1
Tactic:
apply Nat.le_pred_of_lt
Proof state after:
case h.h
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ trunc n a < Nat.sub a 0
Theorem: trunc_pred_eq_trunc_of_trunc_ne_self
Proof state before:
case h.h
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ trunc n a < Nat.sub a 0
Tactic:
exact Nat.lt_of_le_of_ne (trunc_le n a) h
Proof state after:
no goals
Theorem: trunc_pred_eq_trunc_of_trunc_ne_self
Proof state before:
case k
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ a - 1 < next n (trunc n a)
Tactic:
exact Nat.lt_of_le_of_lt tsub_le_self (lt_next_trunc npos a)
Proof state after:
no goals
Theorem: trunc_add_half_ulp_eq_of_no_uflow
Proof state before:
n x : ℕ
npos : 0 < n
no_uflow : 2 ^ n ≤ x
⊢ 2 * (trunc n x + ulp n x / 2) = trunc n x + next n (trunc n x)
Tactic:
have ulp_even := two_dvd_ulp_of_no_uflow no_uflow
Proof state after:
n x : ℕ
npos : 0 < n
no_uflow : 2 ^ n ≤ x
ulp_even : 2 ∣ ulp n x
⊢ 2 * (trunc n x + ulp n x / 2) = trunc n x + next n (trunc n x)
Theorem: trunc_add_half_ulp_eq_of_no_uflow
Proof state before:
n x : ℕ
npos : 0 < n
no_uflow : 2 ^ n ≤ x
ulp_even : 2 ∣ ulp n x
⊢ 2 * (trunc n x + ulp n x / 2) = trunc n x + next n (trunc n x)
Tactic:
rw [Nat.left_distrib, Nat.two_mul, Nat.add_assoc,
    Nat.mul_div_cancel' ulp_even, ← ulp_trunc npos, next]
Proof state after:
no goals
Theorem: trunc_le_trunc_of_lt_next_trunc
Proof state before:
n x y : ℕ
npos : 0 < n
h : x < next n (trunc n y)
⊢ trunc n x ≤ trunc n y
Tactic:
cases Nat.le_total x (trunc n y) with
| inl hxy => exact trunc_le_trunc npos (Nat.le_trans hxy (trunc_le n y))
| inr hyx => exact ge_of_eq (trunc_eq_trunc_of_le_of_lt npos hyx h)
Proof state after:
no goals
Theorem: trunc_le_trunc_of_lt_next_trunc
Proof state before:
case inl
n x y : ℕ
npos : 0 < n
h : x < next n (trunc n y)
hxy : x ≤ trunc n y
⊢ trunc n x ≤ trunc n y
Tactic:
exact trunc_le_trunc npos (Nat.le_trans hxy (trunc_le n y))
Proof state after:
no goals
Theorem: trunc_le_trunc_of_lt_next_trunc
Proof state before:
case inr
n x y : ℕ
npos : 0 < n
h : x < next n (trunc n y)
hyx : trunc n y ≤ x
⊢ trunc n x ≤ trunc n y
Tactic:
exact ge_of_eq (trunc_eq_trunc_of_le_of_lt npos hyx h)
Proof state after:
no goals
Theorem: next_trunc_sub_eq_ulp_sub_mod
Proof state before:
n : ℕ
npos : 0 < n
c : ℕ
⊢ next n (trunc n c) - c = ulp n c - c % ulp n c
Tactic:
unfold next
Proof state after:
n : ℕ
npos : 0 < n
c : ℕ
⊢ trunc n c + ulp n (trunc n c) - c = ulp n c - c % ulp n c