Stream: new members

Topic: casting between rational/real

Meyer Zinn (Nov 08 2020 at 23:52):

I'm trying to show that irrational_sqrt_two -> rat.sqrt(2) * rat.sqrt(2) \ne 2. mathlib comes with a proof that the sqrt of 2 : R is irrational, but the irrational_sqrt_rat_iff theorem takes a proof that the sqrt of 2 : Q is irrational. How should I approach this? Do I need a lemma that the sqrt of 2 : Q is irrational using the fact that sqrt 2 : R is irrational?

Meyer Zinn (Nov 08 2020 at 23:53):

Actually, I just realized this approach doesn't make sense, since rat.sqrt is not related to real.sqrt (I think?)

Meyer Zinn (Nov 08 2020 at 23:54):

Will need to find a different proof approach. My ultimate goal is to show that there is no integer $n$ such that $n^2=2$.

Yakov Pechersky (Nov 09 2020 at 00:24):

For all n : Z, n <= n * n. So if n * n = 2, then n <= 2. Split on -2 and below, 2, then finish on case bash on -1, 0, 1?

Bryan Gin-ge Chen (Nov 09 2020 at 00:34):

This is a little slow, but it works:

import tactic
example : ¬ (∃ (n : ℤ), n * n = 2) :=
begin
push_neg,
intros n hn,
by_cases h : 2 ≤ abs n,
{ have : 4 ≤ (abs n)*(abs n) := calc
4 = 2*2 : dec_trivial
... ≤ (abs n) * (abs n) : mul_le_mul h h dec_trivial (le_trans dec_trivial h),
rw [←abs_mul_abs_self] at hn,
linarith },
{ simp only [abs_lt, not_le] at h,
obtain ⟨h₁, h₂⟩ := h,
interval_cases n,
all_goals { linarith } }
end


Bryan Gin-ge Chen (Nov 09 2020 at 00:57):

Here's a similar proof using Yakov's idea:

import tactic

-- this seems to be missing from mathlib?
lemma int.le_mul_self (n : ℤ) : n ≤ n * n :=
begin
rw [←int.nat_abs_mul_self'],
calc n ≤ (n.nat_abs : ℤ) : int.le_nat_abs
... ≤ _ : by exact_mod_cast nat.le_mul_self _,
end

example : ¬ (∃ (n : ℤ), n * n = 2) :=
begin
push_neg,
intros n hn,
by_cases h : 2 < abs n,
{ rw [←abs_mul_abs_self] at hn,
have : abs n ≤ 2 := by { rw ←hn, exact int.le_mul_self _ },
linarith },
{ simp only [abs_le, not_lt] at h,
obtain ⟨h₁, h₂⟩ := h,
interval_cases n,
all_goals { linarith } }
end


Mario Carneiro (Nov 09 2020 at 01:17):

What is docs#rat.sqrt?

Mario Carneiro (Nov 09 2020 at 01:18):

rat.sqrt 2 is garbage

Mario Carneiro (Nov 09 2020 at 01:28):

Here's a proof that actually uses irrational_sqrt_two instead of reproving it:

import data.rat.sqrt data.real.irrational

example : ¬ ∃ (n : ℤ), n * n = 2 :=
begin
rintro ⟨n, e⟩,
apply (irrational_iff_ne_rational _).1 irrational_sqrt_two (abs n) 1,
simp,
rw [real.sqrt_eq_iff_mul_self_eq _ (abs_nonneg _), ← abs_mul, abs_mul_self],
{exact_mod_cast e}, {norm_num},
end


Last updated: May 14 2021 at 06:16 UTC