Zulip Chat Archive

Stream: new members

Topic: casting between rational/real


view this post on Zulip 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?

view this post on Zulip 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?)

view this post on Zulip 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$.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 09 2020 at 01:17):

What is docs#rat.sqrt?

view this post on Zulip Mario Carneiro (Nov 09 2020 at 01:18):

rat.sqrt 2 is garbage

view this post on Zulip 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