Zulip Chat Archive

Stream: new members

Topic: Cases on even/oddness of a nat?


Sandy Maguire (Jan 07 2021 at 20:22):

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 (Jan 07 2021 at 20:22):

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

Alex J. Best (Jan 07 2021 at 20:24):

You can start the proof with

begin
intro  p,
cases nat.even_or_odd p,
end

Sandy Maguire (Jan 07 2021 at 20:24):

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

Alex J. Best (Jan 07 2021 at 20:25):

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

Eric Wieser (Jan 07 2021 at 20:26):

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

Eric Wieser (Jan 07 2021 at 20:26):

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

Alex J. Best (Jan 07 2021 at 20:28):

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 (Jan 07 2021 at 20:29):

how could i have found even_or_odd for myself?

Alex J. Best (Jan 07 2021 at 20:31):

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 (Jan 07 2021 at 20:31):

#naming :smile:

Eric Wieser (Jan 07 2021 at 20:31):

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

Sandy Maguire (Jan 07 2021 at 20:32):

thanks all!

Sandy Maguire (Jan 07 2021 at 20:46):

how can i refine

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

into n = 0?

Sandy Maguire (Jan 07 2021 at 20:52):

got it -- rw h at hn and then linarith

Sandy Maguire (Jan 07 2021 at 21:13):

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 (Jan 07 2021 at 21:15):

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

Eric Wieser (Jan 07 2021 at 21:23):

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 (Jan 07 2021 at 21:36):

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 (Jan 07 2021 at 21:37):

oh got it:

import data.nat.parity
import tactic

open nat

Kevin Buzzard (Jan 07 2021 at 21:42):

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 (Jan 07 2021 at 21:46):

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

Bryan Gin-ge Chen (Jan 07 2021 at 21:55):

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 (Jan 07 2021 at 21:57):

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 (Jan 07 2021 at 21:58):

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

Sandy Maguire (Jan 07 2021 at 21:59):

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

Sandy Maguire (Jan 07 2021 at 22:00):

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

Bryan Gin-ge Chen (Jan 07 2021 at 22:00):

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

Sandy Maguire (Jan 07 2021 at 22:03):

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

Kevin Buzzard (Jan 07 2021 at 22:03):

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

Ruben Van de Velde (Jan 08 2021 at 09:44):

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

Last updated: Dec 20 2023 at 11:08 UTC