Walking through an Irrationality Proof of Square Root of 2

Stream: new members

[Husnain Raza]

Hey - I just picked up Lean a couple days ago and I'm working through a couple of classic proofs - would love some assistance as I make my way through some of them

import data.nat.basic

def coprime (p q : ℕ) : Prop :=  ( ∀ d : ℕ, ((∃ x y : ℕ, (p = d*x ∧ q = d*y)) → (d = 1)))

#eval coprime 5 6
#eval coprime 4 2

I've defined the following for determining if two numbers are coprime - however both of these return the same result; have I done something wrong?

[Eric Wieser]

The result for both is "I can't useful print this"

[Eric Wieser]

It's the same output as #eval 2 + 2 = 4 gives, right?

[Eric Wieser]

You need to ask lean to "decide" the proposition, which you can do by casting to bool

[Husnain Raza]

Im going to keep my questions in this thread as its the same proof that I am working on - I am currently trying to prove something similar to the following:

theorem test_theorem: (∃ x : ℕ, (2 * x = 10)) :=
begin
  sorry,
end

what tactic(s) would i use in order to prove this? I should just be able to provide a solution (x=5), but not sure how to translate that into lean

[David Renshaw]

use 5

[Husnain Raza]

thanks!

[Husnain Raza]

is there an easy way to search for theorems besides scrolling through the mathlib docs? i vaguely know what i want to do (need something along the lines of x+1 = y+1 \implies x = y), but I'm not sure how to find such a theorem efficiently

[David Renshaw]

tactic#library_search

[Husnain Raza]

Thanks for the help! This proof is coming together, its like an intro proof class all over again :grinning_face_with_smiling_eyes:

[Husnain Raza]

lemma all_integers_even_or_odd {n : ℕ} : (even n) ∨ (odd n) :=
begin
  induction n with j,
  {
    -- 0 is even as 0 = 2*0
    rewrite even,
    use 0,
    ring,
  },
  {
    rw odd, rw even, rw succ_eq_add_one,
    rw odd at n_ih, rw even at n_ih,
    cases n_ih, {
      -- case that j is even
      have h1 : (∃ l: ℕ, (j+1 = 2*l+1) ), by begin {
        cases n_ih with l',
        use l',
        finish,
      }
      end,
      finish,
    },
    {
      -- case that j is odd
      have h2 : (∃ l: ℕ, (j+1 = 2*l) ), by begin {
        cases n_ih with l',
        use l'+1,
        finish,
      }
      end,
      finish,
    },
  }
end

this was probably unnecessary but any feedback would be appreciated

[Eric Wieser]

A good next step would be to try to replace finish with simp, ring or some other action; that way, you can learn the steps it's taking

[Eric Wieser]

by begin { ... } end is better spelt { ... }!

[Husnain Raza]

that is better spelt

[Husnain Raza]

im almost done with implementing Euclid's proof of the irrationality of sqrt 2 - after that I'll go through and polish it up

[Kevin Buzzard]

finish really slows your code down and makes the game less fun. Too many orange bars.