Zulip Chat Archive

Stream: maths

Topic: Sqrt of 2 is irrational


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

Sayantan Majumdar (May 05 2020 at 11:26):

has anyone done this proof in a better way?

Sayantan Majumdar (May 05 2020 at 11:26):

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

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

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

Sayantan Majumdar (May 05 2020 at 11:57):

thanks, will try to continue from there

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.

Patrick Massot (May 05 2020 at 12:04):

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

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: Dec 20 2023 at 11:08 UTC