Zulip Chat Archive

Stream: maths

Topic: Sqrt of 2 is irrational


view this post on Zulip Sayantan Majumdar (May 05 2020 at 11:25):

I am trying to prove ¬(∃ p : ℚ, p * p = 2). I have reached to a somewhat good place but there is a coercion issue

example : ¬( p : , p * p = 2) :=
begin
    intro h,
    apply exists.elim h,
    assume p,
    assume h₀,
    have h₁, from @rat.eq_iff_mul_eq_mul (p * p) (2 : ),
    have h₂, from (iff.elim_left h₁),
    have h₃, from eq.symm (h₂ h₀),
    have h₄, from (rat.coe_nat_denom 2),
    -- have h₅, from @eq.subst ℤ (λ x, (2 : ℚ).num * ↑((p * p).denom) = (p * p).num * x) ↑((2 : ℚ).denom) 1 h₄ h₃,
    have h₅, from rat.coe_nat_num 2,
    have h₆, from rat.coe_int_denom 2,
    have h₇, from rat.coe_int_num 2,
    have h₈, from rat.coe_int_eq_of_int 2,
    sorry,
end

view this post on Zulip Sayantan Majumdar (May 05 2020 at 11:26):

has anyone done this proof in a better way?

view this post on Zulip Sayantan Majumdar (May 05 2020 at 11:26):

I am having trouble getting rid of the 2.denom part

view this post on Zulip Patrick Massot (May 05 2020 at 11:44):

I have zero experience using rational numbers in Lean but I would start with:

import tactic
example : ¬( p : , p * p = 2) :=
begin
  suffices : ¬  a b : , a*a = 2*b*b,
  { rintro p, h₀,
    apply this,
    rw rat.eq_iff_mul_eq_mul at h₀,
    use [p.num, p.denom],
    norm_cast at h₀,
    simpa [mul_assoc, rat.mul_self_num, rat.mul_self_denom] using h₀ },

    sorry,
end

view this post on Zulip Patrick Massot (May 05 2020 at 11:45):

Of course you'll find much more by reading https://leanprover-community.github.io/mathlib_docs/data/real/irrational.html

view this post on Zulip Sayantan Majumdar (May 05 2020 at 11:57):

thanks, will try to continue from there

view this post on Zulip Patrick Massot (May 05 2020 at 12:03):

You should also study the use of rintros and rw here (and simpa). It will make your code much more efficient.

view this post on Zulip Patrick Massot (May 05 2020 at 12:04):

Your handling of negation also strongly suggests you would benefit from going through the tutorials project.

view this post on Zulip Sayantan Majumdar (May 05 2020 at 12:09):

thanks, will do. was trying to write everything out to understand where thing have gone wrong


Last updated: May 06 2021 at 18:20 UTC