internlm/Lean-Github huggingface dataset:
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 + x < trunc n x + (trunc n x + ulp n x)
Tactic:
rewrite [← Nat.add_assoc]
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
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 + x < trunc n x + trunc n x + ulp n x
Tactic:
rewrite [← Nat.div_mul_cancel ulp_even]
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 / 2 * 2
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 + x < trunc n x + trunc n x + ulp n x / 2 * 2
Tactic:
rewrite [← mul_two, ← mul_two, ← add_mul]
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 * 2 < (trunc n x + ulp n x / 2) * 2
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 * 2 < (trunc n x + ulp n x / 2) * 2
Tactic:
exact Nat.mul_lt_mul_of_pos_right h two_pos
Proof state after:
no goals
Theorem: round_eq_trunc_of_lt_midpoint
Proof state before:
case inl.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
lo : round x = trunc n x
⊢ round x = trunc n x
Tactic:
exact lo
Proof state after:
no goals
Theorem: round_eq_trunc_of_lt_midpoint
Proof state before:
case inl.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
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
hi : round x = next n (trunc n x)
⊢ round x = trunc n x
Tactic:
exfalso
Proof state after:
case inl.inr.h
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
hi : round x = next n (trunc n x)
⊢ False
Theorem: round_eq_trunc_of_lt_midpoint
Proof state before:
case inl.inr.h
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
hi : round x = next n (trunc n x)
⊢ False
Tactic:
exact Nat.lt_le_asymm h $ hcorrect₁ x hi
Proof state after:
no goals
Theorem: midpoint_le_of_round_eq_next_trunc
Proof state before:
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₁ : correct₁ n round
hhi : round x = next n (trunc n x)
⊢ trunc n x + ulp n x / 2 ≤ x
Tactic:
cases Nat.lt_or_ge x (2 ^ n) with
| inl uflow =>
  exact le_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 h1,
           Nat.add_comm, ← le_tsub_iff_right h2]
  exact hcorrect₁ x hhi
Proof state after:
no goals
Theorem: midpoint_le_of_round_eq_next_trunc
Proof state before:
case inl
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₁ : correct₁ n round
hhi : round x = next n (trunc n x)
uflow : x < 2 ^ n
⊢ trunc n x + ulp n x / 2 ≤ x
Tactic:
exact le_of_eq (trunc_add_half_ulp_eq_of_uflow uflow)
Proof state after:
no goals
Theorem: midpoint_le_of_round_eq_next_trunc
Proof state before:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₁ : correct₁ n round
hhi : round x = next n (trunc n x)
no_uflow : x ≥ 2 ^ n
⊢ trunc n x + ulp n x / 2 ≤ x
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
hhi : round x = next n (trunc n x)
no_uflow : x ≥ 2 ^ n
⊢ 2 * (trunc n x + ulp n x / 2) ≤ 2 * x
Theorem: midpoint_le_of_round_eq_next_trunc
Proof state before:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₁ : correct₁ n round
hhi : round x = next n (trunc n x)
no_uflow : x ≥ 2 ^ n
⊢ 2 * (trunc n x + ulp n x / 2) ≤ 2 * x
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
hhi : round x = next n (trunc n x)
no_uflow : x ≥ 2 ^ n
⊢ trunc n x + next n (trunc n x) ≤ 2 * x
Theorem: midpoint_le_of_round_eq_next_trunc
Proof state before:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₁ : correct₁ n round
hhi : round x = next n (trunc n x)
no_uflow : x ≥ 2 ^ n
⊢ trunc n x + next n (trunc n x) ≤ 2 * 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
hhi : round x = next n (trunc n x)
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
⊢ trunc n x + next n (trunc n x) ≤ 2 * x
Theorem: midpoint_le_of_round_eq_next_trunc
Proof state before:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₁ : correct₁ n round
hhi : round x = next n (trunc n x)
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
⊢ trunc n x + next n (trunc n x) ≤ 2 * 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
hhi : round x = next n (trunc n x)
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
h2 : trunc n x ≤ x
⊢ trunc n x + next n (trunc n x) ≤ 2 * x
Theorem: midpoint_le_of_round_eq_next_trunc
Proof state before:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₁ : correct₁ n round
hhi : round x = next n (trunc n x)
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
h2 : trunc n x ≤ x
⊢ trunc n x + next n (trunc n x) ≤ 2 * x
Tactic:
rewrite [Nat.two_mul, ← tsub_le_iff_left, add_tsub_assoc_of_le h1,
         Nat.add_comm, ← le_tsub_iff_right h2]
Proof state after:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₁ : correct₁ n round
hhi : round x = next n (trunc n x)
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
h2 : trunc n x ≤ x
⊢ next n (trunc n x) - x ≤ x - trunc n x
Theorem: midpoint_le_of_round_eq_next_trunc
Proof state before:
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₁ : correct₁ n round
hhi : round x = next n (trunc n x)
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
h2 : trunc n x ≤ x
⊢ next n (trunc n x) - x ≤ x - trunc n x
Tactic:
exact hcorrect₁ x hhi
Proof state after:
no goals
Theorem: round_le_trunc_of_le_trunc
Proof state before:
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
⊢ round y ≤ trunc n x
Tactic:
cases Nat.lt_or_eq_of_le h with
| inl lt => have pos := Nat.zero_lt_of_lt lt
  rewrite [← next_trunc_pred_trunc_eq_self npos pos]
  apply Nat.le_trans
  . exact round_le_next_trunc hfaithful₁ y
  . apply next_le_next
    apply trunc_le_trunc npos
    apply Nat.le_pred_of_lt
    exact lt
| inr eq => rw [eq, round_trunc npos x hfaithful₀]
Proof state after:
no goals
Theorem: round_le_trunc_of_le_trunc
Proof state before:
case inl
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
⊢ round y ≤ trunc n x
Tactic:
have pos := Nat.zero_lt_of_lt lt
Proof state after:
case inl
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ round y ≤ trunc n x
Theorem: round_le_trunc_of_le_trunc
Proof state before:
case inl
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ round y ≤ trunc n x
Tactic:
rewrite [← next_trunc_pred_trunc_eq_self npos pos]
Proof state after:
case inl
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ round y ≤ next n (trunc n (trunc n x - 1))
Theorem: round_le_trunc_of_le_trunc
Proof state before:
case inl
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ round y ≤ next n (trunc n (trunc n x - 1))
Tactic:
apply Nat.le_trans
Proof state after:
case inl.a
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ round y ≤ ?inl.m

case inl.a
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ ?inl.m ≤ next n (trunc n (trunc n x - 1))

case inl.m
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ ℕ
Theorem: round_le_trunc_of_le_trunc
Proof state before:
case inl.a
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ round y ≤ ?inl.m

case inl.a
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ ?inl.m ≤ next n (trunc n (trunc n x - 1))

case inl.m
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ ℕ
Tactic:
. exact round_le_next_trunc hfaithful₁ y
Proof state after:
case inl.a
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ next n (trunc n y) ≤ next n (trunc n (trunc n x - 1))
Theorem: round_le_trunc_of_le_trunc
Proof state before:
case inl.a
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ next n (trunc n y) ≤ next n (trunc n (trunc n x - 1))
Tactic:
. apply next_le_next
  apply trunc_le_trunc npos
  apply Nat.le_pred_of_lt
  exact lt
Proof state after:
no goals
Theorem: round_le_trunc_of_le_trunc
Proof state before:
case inl.a
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ round y ≤ ?inl.m
Tactic:
exact round_le_next_trunc hfaithful₁ y
Proof state after:
no goals
Theorem: round_le_trunc_of_le_trunc
Proof state before:
case inl.a
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ next n (trunc n y) ≤ next n (trunc n (trunc n x - 1))
Tactic:
apply next_le_next
Proof state after:
case inl.a.h
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ trunc n y ≤ trunc n (trunc n x - 1)
Theorem: round_le_trunc_of_le_trunc
Proof state before:
case inl.a.h
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ trunc n y ≤ trunc n (trunc n x - 1)
Tactic:
apply trunc_le_trunc npos
Proof state after:
case inl.a.h
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ y ≤ trunc n x - 1
Theorem: round_le_trunc_of_le_trunc
Proof state before:
case inl.a.h
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ y ≤ trunc n x - 1
Tactic:
apply Nat.le_pred_of_lt
Proof state after:
case inl.a.h.h
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ y < Nat.sub (trunc n x) 0
Theorem: round_le_trunc_of_le_trunc
Proof state before:
case inl.a.h.h
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ y < Nat.sub (trunc n x) 0
Tactic:
exact lt
Proof state after:
no goals
Theorem: round_le_trunc_of_le_trunc
Proof state before:
case inr
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
eq : y = trunc n x
⊢ round y ≤ trunc n x
Tactic:
rw [eq, round_trunc npos x hfaithful₀]
Proof state after:
no goals
Theorem: round_sub_le
Proof state before:
a n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
b : ℕ
hfa : trunc n a = a
⊢ round (a - b) ≤ a
Tactic:
trans trunc n a
Proof state after:
a n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
b : ℕ
hfa : trunc n a = a
⊢ round (a - b) ≤ trunc n a

a n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
b : ℕ
hfa : trunc n a = a
⊢ trunc n a ≤ a
Theorem: round_sub_le
Proof state before:
a n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
b : ℕ
hfa : trunc n a = a
⊢ round (a - b) ≤ trunc n a

a n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
b : ℕ
hfa : trunc n a = a
⊢ trunc n a ≤ a
Tactic:
. apply round_le_trunc_of_le_trunc npos hfaithful₀ hfaithful₁
  exact Nat.le_trans tsub_le_self hfa.ge
Proof state after:
a n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
b : ℕ
hfa : trunc n a = a
⊢ trunc n a ≤ a
Theorem: round_sub_le
Proof state before:
a n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
b : ℕ
hfa : trunc n a = a
⊢ trunc n a ≤ a
Tactic:
. exact trunc_le _ _
Proof state after:
no goals
Theorem: round_sub_le
Proof state before:
a n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
b : ℕ
hfa : trunc n a = a
⊢ round (a - b) ≤ trunc n a
Tactic:
apply round_le_trunc_of_le_trunc npos hfaithful₀ hfaithful₁
Proof state after:
a n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
b : ℕ
hfa : trunc n a = a
⊢ a - b ≤ trunc n a
Theorem: round_sub_le
Proof state before:
a n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
b : ℕ
hfa : trunc n a = a
⊢ a - b ≤ trunc n a
Tactic:
exact Nat.le_trans tsub_le_self hfa.ge
Proof state after:
no goals
Theorem: round_sub_le
Proof state before:
a n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
b : ℕ
hfa : trunc n a = a
⊢ trunc n a ≤ a
Tactic:
exact trunc_le _ _
Proof state after:
no goals
Theorem: round_add_le
Proof state before:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : b ≤ a
⊢ round (a + b) ≤ 2 * a
Tactic:
rewrite [← add_tsub_tsub_cancel hba]
Proof state after:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : b ≤ a
⊢ round (a + a - (a - b)) ≤ 2 * a
Theorem: round_add_le
Proof state before:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : b ≤ a
⊢ round (a + a - (a - b)) ≤ 2 * a
Tactic:
rewrite [← two_mul, ← pow_one 2]
Proof state after:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : b ≤ a
⊢ round (2 ^ 1 * a - (a - b)) ≤ 2 ^ 1 * a
Theorem: round_add_le
Proof state before:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : b ≤ a
⊢ round (2 ^ 1 * a - (a - b)) ≤ 2 ^ 1 * a
Tactic:
apply round_sub_le npos hfaithful₀ hfaithful₁
Proof state after:
case hfa
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : b ≤ a
⊢ trunc n (2 ^ 1 * a) = 2 ^ 1 * a
Theorem: round_add_le
Proof state before:
case hfa
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : b ≤ a
⊢ trunc n (2 ^ 1 * a) = 2 ^ 1 * a
Tactic:
rw [trunc_pow_mul npos, hfa]
Proof state after:
no goals
Theorem: round_le_round
Proof state before:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
⊢ round b ≤ round a
Tactic:
have lolo : trunc n b ≤ trunc n a := trunc_le_trunc npos hba
Proof state after:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
⊢ round b ≤ round a
Theorem: round_le_round
Proof state before:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
⊢ round b ≤ round a
Tactic:
have lohi : trunc n b ≤ next n (trunc n a) :=
  Nat.le_trans lolo (Nat.le_add_right _ _)
Proof state after:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
⊢ round b ≤ round a
Theorem: round_le_round
Proof state before:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
⊢ round b ≤ round a
Tactic:
have hihi : next n (trunc n b) ≤ next n (trunc n a) :=
  Nat.add_le_add lolo (ulp_le_ulp n lolo)
Proof state after:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
⊢ round b ≤ round a
Theorem: round_le_round
Proof state before:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
⊢ round b ≤ round a
Tactic:
rcases hfaithful₁ b, (hfaithful₁ a).symm with ⟨blo | bhi, ahi | alo⟩
Proof state after:
case inl.inl
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
blo : round b = trunc n b
ahi : round a = next n (trunc n a)
⊢ round b ≤ round a

case inl.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
blo : round b = trunc n b
alo : round a = trunc n a
⊢ round b ≤ round a

case inr.inl
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
ahi : round a = next n (trunc n a)
⊢ round b ≤ round a

case inr.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
⊢ round b ≤ round a
Theorem: round_le_round
Proof state before:
case inl.inl
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
blo : round b = trunc n b
ahi : round a = next n (trunc n a)
⊢ round b ≤ round a

case inl.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
blo : round b = trunc n b
alo : round a = trunc n a
⊢ round b ≤ round a

case inr.inl
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
ahi : round a = next n (trunc n a)
⊢ round b ≤ round a

case inr.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
⊢ round b ≤ round a
Tactic:
. rwa [blo, ahi]
Proof state after:
case inl.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
blo : round b = trunc n b
alo : round a = trunc n a
⊢ round b ≤ round a

case inr.inl
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
ahi : round a = next n (trunc n a)
⊢ round b ≤ round a

case inr.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
⊢ round b ≤ round a