Inequalities with Reals

Stream: new members

[ROCKY KAMEN-RUBIO]

I'm trying to prove ¬ real.sqrt 5 = 0. I know that for nats we would just do cc, but tactics like ring don't seem to be working for me here. I'm also having trouble finding theorems in mathlib that relate to inequalities with reals, or theorems from other typeclasses that are inherited by the reals. I'm could transform this into expressions like ¬ 5 = 0 using (0:ℝ) ≤ (5:ℝ) and real.sqrt_eq_zero, but then I run into the same issue. Could someone point me in the right direction?

[Reid Barton]

The norm_num tactic will prove ¬ 5 = 0, at least.

[Shing Tak Lam]

In fact norm_num could prove your initial goal.

import tactic data.real.basic

example : ¬ real.sqrt 5 = 0 := by norm_num

[Mario Carneiro]

this is almost certainly one of those times when it's not norm_num doing the work

[Reid Barton]

@[simp] theorem sqrt_eq_zero (h : 0 ≤ x) : sqrt x = 0 ↔ x = 0

[Mario Carneiro]

aha:

example : ¬ real.sqrt 5 = 0 := by simp [
  show 0 ≤ (5:ℝ), by norm_num, show (5:ℝ) ≠ 0, by norm_num]

[Mario Carneiro]

it's because norm_num calls simp with norm_num as discharger

[ROCKY KAMEN-RUBIO]

Somewhat related inequality question: I'm trying to do this pretty simple limit proof. I get this far, and I know conceptually I need to use he and the inverse of hn to finesse my goal state into something trivial, but I can't seem to get there with the theorems I know (especially with the type casting). Could someone point me in the right direction?

import data.real.basic
import data.nat.basic
import algebra.archimedean
def lim_to_inf (x : ℕ → ℝ) (l : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, abs (x n - l) < ε

example : lim_to_inf (λ n, 1/n) 0 :=
begin
rw lim_to_inf,
intro ε,
intro hε,
have he := exists_nat_gt ε,
cases he with N he,
use N,
intro n,
intro hn,
simp,
end

[Kevin Buzzard]

What if epsilon=0.1, N=1, and n=1? Then the goal is false.

[Chris Hughes]

You want a nat greater than 1/epsilon I think.

[Kevin Buzzard]

I would write down a careful paper proof first, and then think about how to get each line into Lean.