Cases on even/oddness of a nat?

Stream: new members

[Sandy Maguire]

I'm trying to formalize the proof given here https://cs.uwaterloo.ca/~cbruni/videos/Math135SeptDec2015/Lesson01ppplusoneprime.pdf, which wants me to inspect whether a nat is even or odd. Besides writing the type of the theorem, I'm not sure how to make progress here.

[Sandy Maguire]

I've gotten as far as theorem prime_and_prime_succ : ∀ p, prime p → prime (p + 1) → p = 2 := sorry

[Alex J. Best]

You can start the proof with

begin
intro  p,
cases nat.even_or_odd p,
end

[Sandy Maguire]

just what i was looking for, thanks. i can probably get it from there

[Alex J. Best]

Ooops, I think you have to import data.nat.parity too

[Eric Wieser]

More generally you can use by_cases h : some_prop if you have an arbitrary condition you want to case on

[Eric Wieser]

But the lemma above will be more convenient for even/odd

[Alex J. Best]

And I misread your goal,

theorem prime_and_prime_succ : ∀ p, prime p → prime (p + 1) → p = 2 :=
begin
  intros p hp hp_succ,
  cases nat.even_or_odd p,
 end

would be way better!

[Sandy Maguire]

how could i have found even_or_odd for myself?

[Alex J. Best]

I just guessed the name, that requires a little experience with the naming convention though.
You can try searching on https://leanprover-community.github.io/mathlib_docs/ by typing in the top right, I put "even odd" in and it came up as the fourth result or something

[Bryan Gin-ge Chen]

#naming :smile:

[Eric Wieser]

Or if desperate, example (n : \N) : is_even n \or is_odd n := by library_search

[Sandy Maguire]

thanks all!

[Sandy Maguire]

how can i refine

hn: p = 2 * n
h: n = p

into n = 0?

[Sandy Maguire]

got it -- rw h at hn and then linarith

[Sandy Maguire]

took me two hours, but i managed to prove it. anyone mind critiquing my solution for style/ergonomics/anything?

theorem prime_and_prime_succ : ∀ p, prime p → prime (p + 1) → p = 2 :=
begin
  intros p hprime hprimesucc,
  cases even_or_odd p,
  {
    cases h with n hn,
    let hprime2 := hprime,
    cases hprime,
    specialize hprime_right n,
    have n_div_p : n ∣ p,
    {
      exact dvd.intro_left 2 (eq.symm hn)
    },

    cases hprime_right n_div_p,
    {
      linarith,
    },

    have p_zero : p = 0,
    {
      rw h at hn,
      linarith,
    },

    by_contradiction h',
    apply not_prime_zero,
    rw p_zero at hprime2,
    exact hprime2,
  },

  let h2 := h,
  cases h with n hn,
  cases hprimesucc,

  have n_div_succ_p : 2 ∣ succ p,
  {
    refine even_iff_two_dvd.mp _,
    refine even_succ.mpr _,
    exact odd_iff_not_even.mp h2,
  },

  specialize hprimesucc_right 2,
  cases hprimesucc_right n_div_succ_p,
  {
    by_contradiction h',
    linarith,
  },

  have n_zero : n = 0,
  {
    linarith,
  },

  rw n_zero at hn,
  by_contradiction,
  refine not_prime_one _,
  have p_one : p = 1,
  {
    linarith,
  },
  rw ←p_one,
  exact hprime,
end

[Sandy Maguire]

in particular i hate let hprime2 := hprime, cases hprime to work around cases destroying my term

[Eric Wieser]

An easy ergonomics thing to start: you can move your forall before the colon as {p} (hprime : prime p) (hprimesucc : prime (p + 1)) : p = 2, which removes the need for intros

[Kevin Buzzard]

Sandy Maguire said:

took me two hours, but i managed to prove it. anyone mind critiquing my solution for style/ergonomics/anything?

Can you post fully working code? (with all imports and open and etc)

[Kevin Buzzard]

oh got it:

import data.nat.parity
import tactic

open nat

[Kevin Buzzard]

I would prove this first:

lemma eq_two_of_prime_and_even (n : ℕ) (hn : even n) (hn' : prime n) : n = 2 :=
begin
  symmetry,
  rw ← prime_dvd_prime_iff_eq prime_two hn',
  exact even_iff_two_dvd.mp hn
end

[Kevin Buzzard]

let h2 := h -- you can use have here instead of let, because h is a proof.

[Bryan Gin-ge Chen]

Here's my first try:

import data.nat.parity
import data.nat.prime

open nat

theorem prime_and_prime_succ (p : ℕ) (hp : prime p) (hp' : prime (p + 1)) : p = 2 :=
begin
  cases hp.eq_two_or_odd with H H,
  { exact H, },
  { exfalso,
    cases hp'.eq_two_or_odd with H' H',
    { rw succ_inj' at H',
      exact hp.ne_one H', },
    { have : even (p + 1) := begin
        rw ← odd_iff at H,
        cases H with k hk,
        rw ← succ_inj' at hk,
        use [k + 1, hk],
      end,
      rw ← not_even_iff at H',
      exact H' this, } }
end

Undoubtedly this can be golfed further...

[Kevin Buzzard]

But the proof looks fine, you step forwards showing the stuff in the proof. Here's a shorter proof:

import data.nat.parity
import tactic

open nat

-- an even prime must be 2
lemma eq_two_of_prime_and_even {n : ℕ} (hn : even n) (hn' : prime n) : n = 2 :=
begin
  symmetry,
  -- goal now 2 = n
  rw ← prime_dvd_prime_iff_eq prime_two hn',
  -- goal now 2 ∣ n which is easy
  exact even_iff_two_dvd.mp hn
end

theorem prime_and_prime_succ (p : ℕ) (hprime : prime p) (hprimesucc : prime (p + 1)) :
  p = 2 :=
begin
  -- p is even or odd
  cases even_or_odd p with hp hp,
  { -- if it's even we're done by the previous lemma
    exact eq_two_of_prime_and_even hp hprime },
  { -- odd case can't happen so let's prove a contradiction
    exfalso,
    -- suffices to prove 1 is prime
    apply not_prime_one,
    -- so it suffices to prove p = 1
    convert hprime,
    -- so it suffices to prove p+1 = 2
    apply nat.add_right_cancel,
    -- but p+1 is prime so it suffices to prove it's even
    convert (eq_two_of_prime_and_even _ hprimesucc).symm,
    -- so it suffices to prove p is isn't even
    rw even_succ,
    -- which we can do because it's odd
    exact odd_iff_not_even.mp hp }
end

[Kevin Buzzard]

Of course I'm cheating by not formalising the proof you showed, but a shorter proof.

[Sandy Maguire]

i'll grok my way through these tomorrow. they're SIGNIFICANTLY shorter!

[Sandy Maguire]

i'd heard great things about this community but never imagined it'd be THIS helpful <3

[Bryan Gin-ge Chen]

Kevin's is nicer because he extracts a lemma that'd be reasonable to PR to mathlib.

[Sandy Maguire]

@Kevin Buzzard i just watched your talk on the future of mathematics, and it was wildly inspiring. thanks for giving it!

[Kevin Buzzard]

Great! Now go formalise a bunch more stuff :-)

[Ruben Van de Velde]

Alternative approach to Kevin's lemma:

import tactic
import data.nat.parity
import data.nat.prime

open nat

lemma eq_two_of_prime_and_even (n : ℕ) (hn : even n) (hn' : prime n) : n = 2 :=
begin
  contrapose! hn,
  rw [←odd_iff_not_even, odd_iff],
  exact hn'.eq_two_or_odd.resolve_left hn,
end