working with symbolic real numbers

Stream: new members

[Luca Seemungal]

How do I solve the following goal :

ε : ℝ,
H : ε > 0,
n : ℕ,
H_1 : nat_ceil (1 / ε) < n
⊢ abs (↑n)⁻¹ < ε

What sort of tactics would be useful here?

[Kevin Buzzard]

This is a nice question. The result is trivial mathematically, but I suspect it's still a bit of work in Lean. We have tactics which help with this sort of thing. My first instinct is to turn H_1 into an inequality about reals (there should be a tactic which does this now but I'm not up to speed with how it's done nowadays, I just remember sweating 2 years ago). Then there will be theorems in the library saying 1/e<=(nat_ceil (1/e) : real) and 0<x<y -> 1/y<1/x which I would be tempted to apply manually. Then you should be reduced to abs (\u n)\-1 = 1/n which should hopefully be less of a pain. I would love it if someone could use tactics to make this less painful.

[Floris van Doorn]

exact_mod_cast is a very useful tactic to write a term explicitly, but not worry about the casts in the expression. Here is how I would do it:

lemma lt_of_lt_nat_ceil {α} [linear_ordered_ring α] [floor_ring α] {x : α} {n}
  (h : nat_ceil x < n) : x < n :=
by { refine lt_of_le_of_lt (le_nat_ceil x) _, exact_mod_cast h }

example (ε : ℝ) (H : ε > 0) (n : ℕ) (H_1 : nat_ceil (1 / ε) < n) : abs (↑n)⁻¹ < ε :=
begin
  rw [abs_inv, abs_of_nonneg, inv_lt _ H, ← one_div_eq_inv],
  { exact lt_of_lt_nat_ceil H_1 },
  { exact_mod_cast lt_of_le_of_lt (zero_le _) H_1 },
  { exact_mod_cast zero_le n }
end

[Patrick Massot]

Mixing inverse and one div looks strange. After https://github.com/leanprover-community/mathlib/blob/master/src/algebra/ordered_field.lean#L81, shouldn't we have

lemma one_div_lt (ha : 0 < a) (hb : 0 < b) : 1/a < b ↔ 1/b < a :=
(one_div_eq_inv a).symm ▸ (one_div_eq_inv b).symm ▸ inv_lt ha hb

[Patrick Massot]

Do you intend to PR that

lemma lt_of_lt_nat_ceil {α} [linear_ordered_ring α] [floor_ring α] {x : α} {n}
  (h : nat_ceil x < n) : x < n :=
lt_of_le_of_lt (le_nat_ceil x) (by exact_mod_cast h)

[Patrick Massot]

(slightly golfed from your post)

[Patrick Massot]

https://github.com/leanprover-community/mathlib/pull/1522